| 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 | |