POPL 2013 Program
8:00-8:50 Breakfast
8:50-9:00 Welcome: Roberto Giacobazzi and Radhia Cousot
9:00-10:00 Invited speaker: Georges Gonthier (Microsoft Research)
Engineering mathematics: the odd order theorem proof

Chair: Manuel Hermenegildo
10:00-10:30 Break
Chair: Peter O'Hearn
Verification & Static Analysis
Chair: Laurent Mauborgne
10:30-11:00 Full abstraction for nominal Scott domains.
S. Lösch, A. Pitts
Cache and I/O efficient functional algorithms.
G. Blelloch, R. Harper
11:00-11:30 The sequential semantics of producer effect systems.
R. Tate
On the linear ranking problem for integer linear-constraint loops.
A. Ben-Amram, S. Genaim
11:30-12:00 Copatterns: programming infinite structures by observations.
A. Abel, B. Pientka, D. Thibodeau, A. Setzer
Advanced automata minimization.
R. Mayr, L. Clemente
12:30-14:00 Lunch
14:00-14:30 Judith Bishop and Natarajan Shankar present the 2012
Microsoft Research Verified Software Milestone Award to Xavier Leroy
Chair: Benjamin Pierce
Abstract Interpretation
Chair: Francesco Ranzato
14:30-15:00 Automating relatively complete verification of higher-order functional programs.
H. Unno, T. Terauchi, N. Kobayashi
Quantitative abstraction refinement.
P. Cerny, T. Henzinger, A. Radhakrishna
15:00-15:30 Abstraction and invariance for algebraically indexed types.
R. Atkey, P. Johann, A. Kennedy
Inductive data flow graphs.
A. Farzan, Z. Kincaid, A. Podelski
15:30-16:00 Static and dynamic semantics of NoSQL languages.
V. Benzaken, G. Castagna, K. Nguyễn, J. Siméon
Abstract conflict driven learning.
V. D'Silva, L. Haller, D. Kroening
16:00-16:30 Break
Chair: Eijiro Sumii
Proofs & Verification
Chair: Xavier Leroy
16:30-17:00 The lambda lambda-bar calculus: a dual calculus for unconstrained strategies.
A. Goyet
The power of parameterization in coinductive proof.
C. Hur, G. Neis, D. Dreyer, V. Vafeiadis
17:00-17:30 The geometry of types.
U. Lago, B. Petit
Meta-theory a la carte.
B. Delaware, B. Oliveira, T. Schrijvers
17:30-18:00 Universal properties of impure programming languages.
S. Staton, P. Levy
A theorem prover for Boolean BI.
J. Park, J. Seo, S. Park
18:00-19:00 Student session
8:00-8:50 Breakfast
8:50-9:00 Most influential POPL paper award
9:00-10:00 Invited speaker: Shriram Krishnamurthi (Brown) - SIGPLAN Robin Milner young researcher award
From principles to programming languages (and back)

Chair: Derek Dreyer
10:00-10:30 Break
Concurrency & Design
Chair: Andreas Rossberg
Separation Logic
Chair: David Walker
10:30-11:00 Library abstraction for C/C++ concurrency.
M. Batty, M. Dodds, A. Gotsman
The type discipline of behavioral separation.
L. Caires, J. Seco
11:00-11:30 Fault tolerance via idempotence.
G. Ramalingam, K. Vaswani
Views: compositional reasoning for concurrent programs.
T. Dinsdale-Young, L. Birkedal, P. Gardner, M. Parkinson, H. Yang
11:30-12:00 Deadlock-freedom-by-design: multiparty asynchronous global programming.
M. Carbone, F. Montesi
High-level separation Logic for low-level code.
J. Jensen, N. Benton, A. Kennedy
12:30-14:00 Lunch
14:15-14:30 In memoriam of Kohei
14:30-15:30 Invited speaker: Andrew Myers (Cornell)
How languages can save distributed computing

Chair: Francesco Logozzo
15:30-16:00 Break
Chair: Peter Sewell
Chair: Kwang Yi
16:00-16:30 Quantitative relaxation of concurrent data structures.
T. Henzinger, C. Kirsch, H. Payer, A. Sezgin, A. Sokolova
Linear dependent types for differential privacy.
M. Gaboardi, A. Haeberlen, J. Hsu, A. Narayan, B. Pierce
16:30-17:00 Plan B: a buffered memory model for Java.
D. Demange, V. Laporte, L. Zhao, S. Jagannathan, D. Pichardie, J. Vitek
Fully abstract compilation to JavaScript.
C. Fournet, N. Swamy, J. Chen, P. Dagand, P. Strub, B. Livshits
17:00-17:30 Logical relations for fine-grained concurrency.
A. Turon, J. Thamsborg, A. Ahmed, L. Birkedal, D. Dreyer
Towards fully automatic placement of security sanitizers and declassifiers,
B. Livshits, S. Chong
18:00-18:15 Conference chairs report
18:15-19:00 Business meeting
20:00-23:00 Social dinner
8:00-8:50 Breakfast
8:50-9:00 POPL 2014 Preview: Suresh Jagannathan and Peter Sewell
9:00-10:00 Invited speaker: Noah Goodman (Stanford)
The principles and practice of probabilistic programming

Chair: Andy Gordon
10:00-10:30 Break
  Models & Semantics
Chair: Tobias Wrigstad
Synthesis & Verification
Chair: Josh Berdine
10:30-11:00 A model-learner pattern for Bayesian reasoning.
A. Gordon, M. Aizatulin, J. Borgstroem, G. Claret, T. Graepel, A. Nori, S. Rajamani, C. Russo
Sigma*: Symbolic Learning of Stream Filters.
M. Botincan, D. Babic
11:00-11:30 Hyperstream processing systems: nonstandard modeling of continuous-time signals.
K. Suenaga, H. Sekine, I. Hasuo
Checking NFA equivalence with bisimulations up to congruence.
F. Bonchi, D. Pous
11:30-12:00 HALO: From Haskell to first-order logic through denotational semantics.
D. Vytiniotis, S. Peyton Jones, K. Claessen, D. Rosén
Synthesis of biological models from mutation experiments.
A. Köksal, Y. Pu, S. Srivastava, R. Bodík, J. Fisher, N. Piterman
12:30-14:00 Lunch
14:00-14:30 Invited Speaker: Doug Mcllroy (Dartmouth College)
POPL in 1973, an idea whose time had come. An amarcord of POPL 1973

Chair: Roberto Giacobazzi
14:30-15:00 The 90th of Corrado Böhm by EATCS and SIGPLAN
Mariangiola Dezani (U. Torino)
Chair: Manuel Fahndich
Analysis & Logics
Chair: Eric Koskinen
15:00-15:30 Sub-polyhedral scheduling using (unit-)two-variable-per-inequality polyhedra.
R. Upadrasta, A. Cohen
The ramifications of sharing in data structures.
A. Hobor, J. Villard
15:30-16:00 Optimizing data structures in high-level programs: new directions for extensible compilers based on staging.
T. Rompf, A. Sujeeth, N. Amin, K. Brown, V. Jovanovic, H. Lee, M. Jonalagedda, K. Olukotun, M. Odersky
Complete instantiation-based interpolation.
N. Totla, T. Wies
16:00-16:30 Principled parsing for indentation-sensitive languages.
M. Adams
Automatic detection of floating-point exceptions.
E. Barr, T. Vo, V. Le, Z. Su
16:30-17:00   Subjective auxiliary state for coarse-grained concurrency.
R. Ley-Wild, A. Nanevski
17:00-17:30 Closing & Break
17:30-19:00 Student session