.

Wednesday, Jan 25

.

8:30-9:20Breakfast

.

9:20-9:30Welcome

.

John Field (General Chair) and Michael Hicks (Program Chair)

.

9:30-10:30SIGPLAN Distinguished Achievement Award Presentation and Interview

.

Tony Hoare, Microsoft Research and Hon. Mem. Cambridge University Computer Laboratory

.

Session chairs: Andrew P. Black, Peter O'Hearn

.

10:30-11:00Refreshments

.

11:00-12:301.A: Verification1.B: Semantics

.

Session chair: Ranjit JhalaSession chair: Patricia Johann

.

Freefinement (Stephan van Staden, Cristiano Calcagno, and Bertrand Meyer)Higher-Order Functional Reactive Programming in Bounded Space (Neelakantan R. Krishnaswami, Nick Benton and Jan Hoffmann)

.

Underspecified harnesses and interleaved bugs (Saurabh Joshi, Shuvendu K. Lahiri, and Akash Lal)The Marriage of Bisimulations and Kripke Logical Relations (Chung-Kil Hur, Derek Dreyer, Georg Neis, and Viktor Vafeiadis)

.

Towards a Program Logic for JavaScript (Philippa Gardner, Sergio Maffeis, and Gareth Smith)Information Effects (Roshan P. James and Amr Sabry)

.

12:30-14:00Lunch

.

14:00-15:30 2.A: Privacy and Access Control2.B: Decision Procedures

.

Session chair: Nikhil SwamySession chair: Swarat Chaudhuri

.

A Language for Automatically Enforcing Privacy Policies (Jean Yang, Kuat Yessenov, and Armando Solar-Lezama)Recursive Proofs for Inductive Tree Data-Structures (Parthasarathy Madhusudan, Xiaokang Qiu, and Andrei Stefanescu)

.

Probabilistic Relational Reasoning for Differential Privacy (Gilles Barthe, Boris Köpf, Federico Olmedo, and Santiago Zanella Bėguelin)Symbolic Finite State Transducers: Algorithms and Applications (Margus Veanes, Pieter Hooimeijer, Benjamin Livshits, David Molnar, and Nikolaj Bjørner)

.

Access Permission Contracts for Scripting Languages (Phillip Heidegger, Annette Bieniusa, and Peter Thiemann)Constraints as Control (Ali Sinan Köksal, Viktor Kuncak, and Philippe Suter)

.

15:30-16:15Refreshments

.

16:15-17:153.A: Security3.B: Complexity for Concurrency

.

Session chair: Neelakantan KrishnaswamiSession chair: P. Madhusudan

.

Multiple Facets for Dynamic Information Flow (Thomas H. Austin and Cormac Flanagan)Deciding Choreography Realizability (Samik Basu, Tevfik Bultan, and Meriem Ouederni)

.

Defining Code-Injection Attacks (Donald Ray and Jay Ligatti)Analysis of Recursively Parallel Programs (Ahmed Bouajjani and Michael Emmi)

.

.

17:30-18:30Reception

.

(Hors d'oeuvres and drinks will be served. Music by the Principle of Jazz. Sponsored by ARM.)

.

18:30-20:00Student Lighting Talks

.

Session chair: Tobias Wrigstad

.

(Best lightning talk award sponsored by Google)

.

.

Thursday, Jan 26

.

8:30-9:20Breakfast

.

9:20-9:30Most Influential POPL Paper Award

.

.

9:30-10:30Invited Talk: Programming Languages for Programmable Networks

.

Jennifer Rexford, Princeton University

.

Session chair: Michael Hicks

.

10:30-11:00Refreshments

.

11:00-12:304.A: Medley4.B: Mechanized Proofs

.

Session chair: Suresh JagannathanSession chair: Adam Chlipala

.

A Compiler and Run-time System for Network Programming Languages (Christopher Monsanto, Nate Foster, Rob Harrison, and David Walker)Playing in the Grey Area of Proofs (Kryštof Hoder, Laura Kovacs, and Andrei Voronkov)

.

Nested Refinements: A Logic For Duck Typing (Ravi Chugh, Patrick M. Rondon, and Ranjit Jhala)Static and User-Extensible Proof Checking (Antonis Stampoulis and Zhong Shao)

.

An Abstract Interpretation Framework for Termination (Patrick Cousot and Radhia Cousot)Run Your Research: On the Effectiveness of Lightweight Mechanization (Casey Klein, John Clements, Christos Dimoulas, Carl Eastlund, Matthias Felleisen, Matthew Flatt, Jay McCarthy, Jon Rafkind, Sam Tobin-Hochstadt, and Robert Bruce Findler)

.

12:30-14:00Lunch

.

14:00-15:305.A: Concurrency5.B: Type Theory

.

Session chair: Matthew ParkinsonSession chair: Stephanie Weirich

.

Verification of Parameterized Concurrent Programs By Modular Reasoning about Data and Control (Azadeh Farzan and Zachary Kincaid)Canonicity for 2-Dimensional Type Theory (Daniel R. Licata and Robert Harper)

.

Resource-Sensitive Synchronization Inference by Abduction (Matko Botinčan, Mike Dodds, and Suresh Jagannathan)Algebraic Foundations for Effect-Dependent Optimisations (Ohad Kammar and Gordon D. Plotkin)

.

Syntactic Control of Interference for Separation Logic (Uday S. Reddy and John C. Reynolds)On the Power of Coercion Abstraction (Julien Cretin and Didier Rémy)

.

15:30-16:15Refreshments

.

16:15-17:156.A: Dynamic Analysis6.B: Names and Binders

.

Session chair: Aarti GuptaSession chair: Zhong Shao

.

Abstractions From Tests (Mayur Naik, Hongseok Yang, Ghila Castelnuovo, and Mooly Sagiv)Towards Nominal Computation (Mikolaj Bojańczyk, Laurent Braud, Bartek Klin, and Slawomir Lasota)

.

Sound Predictive Race Detection in Polynomial Time (Yannis Smaragdakis, Jacob M. Evans, Caitlin Sadowski, Jaeheon Yi, and Cormac Flanagan)Programming with Binders and Indexed Data-Types (Andrew Cave and Brigitte Pientka)

.

17:15-17:30Program Committee chair report

.

Michael Hicks

.

17:30-18:15Business Meeting: The future of POPL

.

Philip Wadler, SIGPLAN Chair

.

.

19:00-22:00Banquet

.

Philadelphia Academy of Fine Arts

.

(Buses depart hotel starting 18:30; see master conference schedule for details.)

.

.

Friday Jan 27

.

8:30-9:20Breakfast

.

9:20-9:30POPL'13 Preview

.

Roberto Giacobazzi (POPL '13 General Chair) and Radhia Cousot (POPL '13 Program Chair)

.

9:30-10:30Invited talk: Meta-level Features in an Industrial-Strength Theorem Prover

.

J Strother Moore, University of Texas

.

Session Chair: John Field

.

10:30-11:00Refreshments

.

11:00-12:307.A: Verified Transformations7.B: Functional Programming

.

Session chair: Chris HawblitzelSession chair: Dimitrios Vytiniotis

.

Formalizing the LLVM Intermediate Representation for Verified Program Transformation (Jianzhou Zhao, Santosh Nagarakatte, Milo M.K. Martin, and Steve Zdancewic)A Unified Approach to Fully Lazy Sharing (Thibaut Balabonski)

.

Randomized Accuracy-Aware Program Transformations For Efficient Approximate Computations (Zeyuan Allen Zhu, Sasa Misailovic, Jonathan Kelner, and Martin Rinard)The Ins and Outs of Gradual Type Inference (Aseem Rastogi, Avik Chaudhuri, and Basil Hosmer)

.

A Rely-Guarantee-Based Simulation for Verifying Concurrent Program Transformations (Hongjin Liang, Xinyu Feng, and Ming Fu)Edit Lenses (Martin Hofmann, Benjamin Pierce, and Daniel Wagner)

.

12:30-14:00Lunch

.

14:00-15:308.A: C/C++ Semantics8.B: Type Systems

.

Session chair: Andreas PodelskiSession chair: Norman Ramsey

.

Clarifying and Compiling C/C++ Concurrency: from C++11 to POWER (Mark Batty, Kayvan Memarian, Scott Owens, Susmit Sarkar, and Peter Sewell)A Type Theory for Probability Density Functions (Sooraj Bhat, Ashish Agarwal, Richard Vuduc, and Alexander Gray)

.

A mechanized semantics for C++ object construction and destruction, with applications to resource management (Tahina Ramananandro, Gabriel Dos Reis, and Xavier Leroy)A Type System for Borrowing Permissions (Karl Naden, Robert Bocchino Jr., Jonathan Aldrich, and Kevin Bierhoff)

.

An Executable Formal Semantics of C with Applications (Chucky Ellison and Grigore Rosu)Self-Certification: Bootstrapping Certified Typecheckers in F* with Coq (Pierre-Yves Strub, Nikhil Swamy, Cédric Fournet, and Juan Chen)

.

15:30-16:00Closing and Raffle

.

(raffle prize sponsored by Google)

.

16:15Refreshments