.

Wednesday, Jan 25

.

8:30-9:20Breakfast

.

9:20-9:30Welcome

.

9:30-10:30Presentation of SIGPLAN Distinguished Achievement Award and Interview [Session Chairs: Andrew P. Black, Peter O'Hearn]
Tony Hoare

.

10:30-11:00

.

11:00-12:30Verification [Session chair: Ranjit Jhala]Semantics [Session chair: Patricia Johann]

.

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

.

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

.

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

.

12:30-2:00Lunch

.

2:00-3:30 Privacy and Access Control [Session chair: Nikhil Swamy]Decision Procedures [Session 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 (P Madhusudan, Xiaokang Qiu, and Andrei Stefanescu)

.

Probabilistic Relational Reasoning for Differential Privacy (Gilles Barthe, Boris Köpf, Federico Olmedo, and Santiago Zanella Beguelin)Symbolic Finite State Transducers, Algorithms and Applications (Nikolaj Bjorner, Pieter Hooimeijer, and Benjamin Livshits, David Molnar, and Margus Veanes)

.

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)

.

3:30-4:15Coffee Break

.

4:15-5:15 Security [Session chair: Neelakantan Krishnaswami]Complexity for Concurrency [Session chair: P. Madhusudan]

.

Multiple Facets for Dynamic Information Flow (Thomas 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)

.

5:15-6:00Break

.

6:00-8:00Student Session [Session chair: Tobias Wrigstad]

.

.

Thursday, Jan 26

.

8:30-9:20Breakfast

.

9:20-9:30Announcements

.

9:30-10:30Invited talk [Session Chair: Michael Hicks]
Jen Rexford

.

10:30-11:00Coffee Break

.

11:00-12:30Medley [Session chair: Suresh Jagannathan]Mechanized Proofs [Session 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 (Krystof 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, and Matthias Felleisen, Matthew Flatt, Jay McCarthy, Jon Rafkind, Sam Tobin-Hochstadt, and Robert Bruce Findler)

.

12:30-2:00Lunch

.

2:00-3:30 Concurrency [Session chair: Matt Parkinson]Type Theory [Session 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 Botincan and Mike Dodds and Suresh Jagannathan )Algebraic Foundations for Effect-Dependent Optimisations (Ohad Kammar and Gordon Plotkin )

.

Syntactic Control of Interference for Separation Logic (Uday S Reddy and John C Reynolds )Extending System F-eta with Abstraction over Erasable Coercions (Didier Remy and Julien Cretin)

.

3:30-4:15Coffee Break

.

4:15-5:15Dynamic Analysis [Session chair: Aarti Gupta]Names & Binders [Session chair: Zhong Shao]

.

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

.

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

.

5:15-5:45Business Meeting

.

7:00Banquet

.

.

Friday Jan 27

.

8:30-9:20Breakfast

.

9:20-9:30POPL'13 preview

.

9:30-10:30Invited talk [Session Chair: John Field]
J Strother Moore

.

10:30-11:00Coffee Break

.

11:00-12:30Verified Transformations [Session chair: Chris Hawblitzel]Functional Programming [Session chair: Dimitrios Vytiniotis]

.

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

.

Optimal Randomized Transformation of Approximate Computations (Zeyuan Allen Zhu, Sasa Misailovic, Jonathan Kelner, and Martin Rinard)The Ins and Outs of Gradual Type Inference (Aseem Rastogi and 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 and Benjamin C Pierce and Daniel Wagner)

.

12:30-2:00Lunch

.

2:00-3:30C/C++ Semantics [Session chair: Andreas Podelski]Type Systems [Session chair: Norman Ramsey]

.

Clarifying and compiling C/C++ concurrency: from C++0x to POWER (Mark Batty, Kayvan Memarian, and Scott Owens, Susmit Sarkar, and Peter Sewell)A Type Theory for Probability Density Functions (Sooraj Bhat, Ashish Agarwal, and 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 Without Fractions (Karl Naden, Robert L Bocchino Jr, and Jonathan Aldrich )

.

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 and Nikhil Swamy, Cedric Fournet, and Juan Chen )

.

3:30-4:00Closing and Raffle