POPL 2014 logo

POPL 2014: 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

San Diego, USA
January 22-24, 2014


19 Jan
20 Jan
21 Jan
22 Jan
23 Jan
24 Jan
25 Jan
 Tutorials PLPV PPREW
  PLMW Posters

Hotel floor plans (PDF)

WEDNESDAY 22 January (DAY 1)

7:00 - 8:20 Breakfast

8:20 - 8:30 Welcoming Remarks: Suresh Jagannathan and Peter Sewell

8:30 - 9:30 Milner Award

Modular Reasoning about Concurrent Higher-Order Imperative Programs

Lars Birkedal (Aarhus University)

9:30 - 10:00 SIGPLAN Achievement Award

A Galois Connection Calculus for Abstract Interpretation

Patrick Cousot (New York University),
Radhia Cousot (École normale supérieure)

10:00 - 10:45 Break

10:45 - 12:15 Session 1a/1b

Session 1a Type System Design. Chair: Nate Foster

Polymorphic Functions with Set-Theoretic Types. Part 1: Syntax, Semantics, and Evaluation

Giuseppe Castagna (CNRS. Université Paris Diderot),
Kim Nguyen (Université Paris-Sud),
Zhiwu Xu (Université Paris Diderot),
Hyeonseung Im (Université Paris-Sud),
Sergueï Lenglet (Université de Lorraine),
Luca Padovani (Università di Torino)

Backpack: Retrofitting Haskell with Interfaces

Scott Kilpatrick (MPI-SWS),
Derek Dreyer (MPI-SWS),
Simon Peyton Jones (Microsoft Research),
Simon Marlow (Facebook)

Combining Proofs and Programs in a Dependently Typed Language

Chris Casinghino, Vilhelm Sjöberg, Stephanie Weirich (University of Pennsylvania)

Session 1b Program Analysis 1. Chair: Xavier Rival

Tracing Compilation by Abstract Interpretation

Stefano Dissegna (University of Padova),
Francesco Logozzo (Microsoft Research),
Francesco Ranzato (University of Padova)

A Type-Directed Abstraction Refinement Approach to Higher-Order Model Checking

Steven J Ramsay, Robin P Neatherway, C.-H. Luke Ong (University of Oxford)

Fissile Type Analysis: Modular Checking of Almost Everywhere Invariants

Devin Coughlin, Bor-Yuh Evan Chang (University of Colorado Boulder)

12:15 - 14:15 Lunch (Celestial Ballroom and Grant Hall)

14:15 - 15:45 Session 2a/2b

Session 2a Semantics of Systems. Chair: James Cheney

A Trusted Mechanised JavaScript Specification

Martin Bodin (Inria & ENS Lyon),
Arthur Chargueraud (Inria & LRI, Universite Paris Sud, CNRS),
Daniele Filaretti (Imperial College London),
Philippa Gardner (Imperial College London),
Sergio Maffeis (Imperial College London),
Daiva Naudziuniene (Imperial College London),
Alan Schmitt (Inria),
Gareth Smith (Imperial College London)

An Operational and Axiomatic Semantics for Non-determinism and Sequence Points in C

Robbert Krebbers (ICIS, Radboud University Nijmegen)

NetKAT: Semantic Foundations for Networks

Carolyn Jane Anderson (Swarthmore College),
Nate Foster (Cornell University),
Arjun Guha (University of Massachusetts Amherst),
Jean-Baptiste Jeannin (Carnegie Mellon University),
Dexter Kozen (Cornell University),
Cole Schlesinger (Princeton University),
David Walker (Princeton University)

Session 2b Program Analysis 2. Chair: Thomas Wies

Bias-Variance Tradeoffs in Program Analysis

Rahul Sharma (Stanford University),
Aditya V. Nori (Microsoft Research),
Alex Aiken (Stanford University)

Abstract Satisfaction

Vijay D'Silva (University of California),
Leopold Haller (University of Oxford),
Daniel Kroening (University of Oxford)

Proofs That Count

Azadeh Farzan (University of Toronto),
Zachary Kincaid (University of Toronto),
Andreas Podelski (University of Freiburg)

15:45 - 16:30 Break

16:30 - 18:00 Session 3a/3b

Session 3a Verified Systems. Chair: Aaron Turon

A Verified Information-Flow Architecture

Arthur Azevedo de Amorim (University of Pennsylvania),
Nathan Collins (Portland State University),
André DeHon (University of Pennsylvania),
Delphine Demange (University of Pennsylvania),
Catalin Hritcu (University of Pennsylvania and INRIA),
David Pichardie (Harvard University and INRIA),
Benjamin C. Pierce (University of Pennsylvania),
Randy Pollack (Harvard University),
Andrew Tolmach (Portland State University)

CakeML: A Verified Implementation of ML

Ramana Kumar (University of Cambridge),
Magnus O. Myreen (University of Cambridge),
Michael Norrish (NICTA),
Scott Owens (University of Kent)

Probabilistic Relational Verification for Cryptographic Implementations

Gilles Barthe (IMDEA Software Institute),
Cédric Fournet (Microsoft Research),
Benjamin Grégoire (Inria Sophia Antipolis - Méditerranée),
Pierre-Yves Strub (IMDEA Software Institute),
Nikhil Swamy (Microsoft Research),
Santiago Zanella-Béguelin (Microsoft Research)

Session 3b Synthesis. Chair: Xavier Rival

Bridging Boolean and Quantitative Synthesis Using Smoothed Proof Search

Swarat Chaudhuri (Rice University),
Martin Clochard (ENS Paris and Université Paris-Sud (LRI and Inria Saclay)),
Armando Solar-Lezama (Massachusetts Institute of Technology)

A Constraint-Based Approach to Solving Games on Infinite Graphs

Tewodros Beyene (TU München),
Swarat Chaudhuri (Rice University),
Corneliu Popeea (TU München),
Andrey Rybalchenko (Microsoft Research Cambridge and TU München)

Sound Compilation of Reals

Eva Darulova, Viktor Kuncak (EPFL)

18:30 - 21:30 Reception and poster session (Crystal Ballroom)

THURSDAY 23 January (DAY 2)

7:00 - 8:10 Breakfast

8:10 - 8:20 Microsoft Research Verified Software Milestone Award

The Intel Core i7 Verification Project

Roope Kaivola (Intel Corporation)

8:20 - 8:30 POPL'04 Most Influential Paper Award

8:30 - 9:00 SIGPLAN Software Systems Award

30 Years of Research and Development around Coq

Gérard Huet, Hugo Herbelin (INRIA Paris - Rocquencourt)

9:00 - 10:00 The Essence of Reynolds

The Essence of Reynolds

Stephen Brookes (Carnegie Mellon University),
Peter W O'Hearn (Facebook),
Uday Reddy (University of Birmingham)

10:00 - 10:45 Break

10:45 - 12:15 Session 4a/4b

Session 4a Concurrent Programming Models. Chair: Viktor Vafeiadis

Freeze After Writing. Quasi-Deterministic Parallel Programming with LVars

Lindsey Kuper (Indiana University),
Aaron Turon (MPI-SWS),
Neelakantan R. Krishnaswami (University of Birmingham),
Ryan R. Newton (Indiana University)

Replicated Data Types: Specification, Verification, Optimality

Sebastian Burckhardt (Microsoft Research),
Alexey Gotsman (IMDEA Software Institute),
Hongseok Yang (University of Oxford),
Marek Zawirski (INRIA & UPMC-LIP6)

Verifying Eventual Consistency of Optimistic Replication Systems

Ahmed Bouajjani, Constantin Enea, Jad Hamza (LIAFA, Univ Paris Diderot, Sorbonne Paris Cite)

Session 4b Probability. Chair: Nikhil Swamy

On Coinductive Equivalences for Higher-Order Probabilistic Functional Programs

Ugo Dal Lago (Università di Bologna & INRIA),
Davide Sangiorgi (Università di Bologna & INRIA),
Michele Alberti (CNRS & Université d'Aix-Marseille)

Probabilistic Coherence Spaces are Fully Abstract for Probabilistic PCF.

Thomas Ehrhard (Laboratoire PPS - CNRS - Université Paris Diderot),
Michele Pagani (Laboratoire LIPN - CNRS - Université Paris 13),
Christine Tasson (Laboratoire PPS - CNRS - Université Paris Diderot)

Tabular: A Schema-Driven Probabilistic Programming Language

Andrew D Gordon (Microsoft Research and University of Edinburgh),
Thore Graepel (Microsoft Research),
Nicolas Rolland (Microsoft Research),
Claudio Russo (Microsoft Research),
Johannes Borgstrom (Uppsala University),
John Guiver (Microsoft Research)

12:15 - 14:15 Lunch (Celestial Ballroom and Grant Hall)

14:15 - 15:45 Session 5a/5b

Session 5a Functional Programming 1. Chair: Alan Jeffrey

Modular, Higher-Order Cardinality Analysis in Theory and Practice

Ilya Sergey (IMDEA Software Institute),
Dimitrios Vytiniotis (Microsoft Research),
Simon Peyton Jones (Microsoft Research)

Profiling For Laziness

Stephen Chang, Matthias Felleisen (Northeastern University)

Fair Reactive Programming

Andrew Cave, Francisco Ferreira, Prakash Panangaden, Brigitte Pientka (McGill University)

Session 5b Reasoning. Chair: Andrey Rybalchenko

Optimal Dynamic Partial Order Reduction

Parosh Abdulla, Stavros Aronis, Bengt Jonsson, Konstantinos Sagonas (Uppsala University)

Modular Reasoning about Heap Paths via Effectively Propositional Formulas

Shachar Itzhaky (Tel Aviv University),
Anindya Banerjee (IMDEA Software Institute),
Neil Immerman (UMASS Amherst),
Ori Lahav (Tel Aviv University),
Aleksandar Nanevski (IMDEA Software Institute),
Mooly Sagiv (Tel Aviv University)

A Sound and Complete Abstraction for Reasoning about Parallel Prefix Sums

Nathan Chong, Alastair F. Donaldson, Jeroen Ketema (Imperial College London)

15:45 - 16:30 Break

16:30 - 18:00 Session 6a/6b

Session 6a Security. Chair: Ross Tate

Authenticated Data Structures, Generically

Andrew Miller, Michael Hicks, Jonathan Katz, Elaine Shi (University of Maryland)

Gradual Typing Embedded Securely in JavaScript

Nikhil Swamy (Microsoft Research),
Cedric Fournet (Microsoft Research),
Aseem Rastogi (University of Maryland),
Karthikeyan Bhargavan (INRIA),
Juan Chen (Microsoft Research),
Pierre-Yves Strub (IMDEA Software Institute),
Gavin Bierman (Microsoft Research)

Sound Input Filter Generation for Integer Overflow Errors

Fan Long, Stelios Sidiroglou-Douskos, Deokhwan Kim, Martin Rinard (Massachusetts Institute of Technology)

Session 6b Separation Logic. Chair: Andrew W. Appel

Parametric Completeness for Separation Theories

James Brotherston, Jules Villard (University College London)

Proof Search for Propositional Abstract Separation Logics via Labelled Sequents

Zhe Hou (The Australian National University),
Ranald Clouston (The Australian National University),
Rajeev Gore (The Australian National University),
Alwen Tiu (Nanyang Technological University)

A Proof System for Separation Logic with Magic Wand

Wonyeol Lee, Sungwoo Park (Pohang University of Science and Technology (POSTECH))

18:00 - 19:00 SIGPLAN meeting (Crystal Ballroom)

20:00 - 23:00 Banquet (USS Midway)

FRIDAY 24 January (DAY 3)

7:00 - 8:20 Breakfast

8:20 - 8:30 POPL'15 preview (Sriram Rajamani and David Walker)

8:30 - 9:00 Conference Report (Peter Sewell and Suresh Jagannathan)

9:00 - 10:00 Invited Talk. Chair: Suresh Jagannathan

From the Trenches: Static Analysis in Industry

Andy Chou

10:00 - 10:45 Break

10:45 - 12:15 Session 7a/7b

Session 7a Semantic Models 1. Chair: Nick Benton

From Parametricity to Conservation Laws, via Noether's Theorem

Robert Atkey

A Relationally Parametric Model of Dependent Type Theory

Robert Atkey,
Neil Ghani (University of Strathclyde),
Patricia Johann (Appalachian State University)

Game Semantics for Interface Middleweight Java

Andrzej S Murawski (University of Warwick ),
Nikos Tzevelekos (Queen Mary University of London)

Session 7b Program Analysis 3. Chair: Ahmed Bouajjani

Abstract Acceleration of General Linear Loops

Bertrand Jeannet (INRIA),
Peter Schrammel (University of Oxford),
Sriram Sankaranarayanan (University of Colorado)

Minimization of Symbolic Automata

Loris D'Antoni (University of Pennsylvania),
Margus Veanes (Microsoft Research)

Consistency Analysis of Decision-Making Programs

Swarat Chaudhuri (Rice University),
Azadeh Farzan (University of Toronto),
Zachary Kincaid (University of Toronto)

12:15 - 14:15 Lunch (Celestial Ballroom and Grant Hall)

14:15 - 15:15 Session 8a/8b

Session 8a Static Errors. Chair: Stephanie Weirich

Toward General Diagnosis of Static Errors

Danfeng Zhang, Andrew C. Myers (Cornell University)

Counter-Factual Typing for Debugging Type Errors

Sheng Chen, Martin Erwig (Oregon State University)

Session 8b Model Checking and SMT. Chair: Andreas Podelski

Battery Transition Systems

Udi Boker (The Interdisciplinary Center, Herzliya),
Thomas A. Henzinger (IST Austria),
Arjun Radhakrishna (IST Austria)

Symbolic Optimization with SMT Solvers

Yi Li (University of Toronto),
Aws Albarghouthi (University of Toronto),
Zachary Kincaid (University of Toronto),
Arie Gurfinkel (Carnegie Mellon University),
Marsha Chechik (University of Toronto)

15:15 - 16:00 Break

16:00 - 17:30 Session 9a/9b

Session 9a Semantic Models 2. Chair: Lars Birkedal

Abstract Effects and Proof-Relevant Logical Relations

Nick Benton (Microsoft Research),
Martin Hofmann (LMU),
Vivek Nigam (UFPB)

Parametric Effect Monads and Semantics of Effect Systems

Shin-ya Katsumata (Kyoto Univeristy)

Applying Quantitative Semantics to Higher-Order Quantum Computing

Michele Pagani (Université Paris 13, Sorbonne Paris Cité),
Peter Selinger (Dalhousie University),
Benoît Valiron (University of Pennsylvania)

Session 9b Functional Programming 2. Chair: Neelakantan R. Krishnaswami

A Nonstandard Standardization Theorem

Beniamino Accattoli (Carnegie Mellon University),
Eduardo Bonelli (Univ. Nac. de Quilmes and CONICET),
Delia Kesner (Univ. Paris-Diderot, SPC, PPS, CNRS),
Carlos Lombardi (Univ. Nac. de Quilmes and Univ. de Buenos Aires)

Closed Type Families with Overlapping Equations

Richard A. Eisenberg (University of Pennsylvania),
Dimitrios Vytiniotis (Microsoft Research Cambridge),
Simon Peyton Jones (Microsoft Research Cambridge),
Stephanie Weirich (University of Pennsylvania)