| POPL 2013 Program | ||
| 23-Jan-2013 | ||
| 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 | |
| Semantics 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 |
|
| Types 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 | |
| Semantics 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 | |
| 24-Jan-2013 | ||
| 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 | |
| Concurrency Chair: Peter Sewell |
Security 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 | |
| 25-Jan-2013 | ||
| 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) |
| Compilation 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 | |