 |
POPL 2014: 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming LanguagesSan Diego, USA
|
Overview
| Sun 19 Jan |
Mon 20 Jan |
Tue 21 Jan |
Wed 22 Jan |
Thu 23 Jan |
Fri 24 Jan |
Sat 25 Jan |
| VMCAI | POPL | DCP | ||||
| PADL | OBT | |||||
| PEPM | PiP | |||||
| Tutorials | PLPV | PPREW | ||||
| PLMW | Posters | |||||
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)