POPL 2015 logo

POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Tata Institute of Fundamental Research, Mumbai, India
January 12-18, 2015

POPL 2015 Accepted Papers

The following 52 papers were accepted out of the 226 submissions to POPL'15. Papers with a checkmark badge have associated artifacts accepted by the artifact evaluation committee.

  1. A Scalable, Correct Time-Stamped Stack
    Mike Dodds (University of York)
    Andreas Haas (University of Salzburg)
    Christoph M. Kirsch (University of Salzburg)
  2. From Communicating Machines to Graphical Choreographies
    Julien Lange (Imperial Colllege London)
    Emilio Tuosto (University of Leicester)
    Nobuko Yoshida (Imperial Colllege London)
  3. Equations, contractions, and unique solutions
    Davide Sangiorgi (University of Bologna and INRIA)
  4. Formal verification of a C static analyzer
    Jacques-Henri Jourdan (Inria Paris-Rocquencourt)
    Vincent Laporte (IRISA and U. Rennes 1)
    Sandrine Blazy (IRISA and U. Rennes 1)
    Xavier Leroy (Inria Paris-Rocquencourt)
    David Pichardie (IRISA and ENS Rennes)
  5. Space-Efficient Manifest Contracts
    Michael Greenberg (Princeton University)
  6. Quantitative Interprocedural Analysis
    Krishnendu Chatterjee (IST Austria)
    Andreas Pavlogiannis (IST Austria)
    Yaron Velner (Tel Aviv University)
  7. Integrating Linear and Dependent Types
    Neel Krishnaswami (University of Birmingham)
    Pierre Pradic (ENS Lyon)
    Nick Benton (Microsoft Research)
  8. Functors are type refinement systems
    Paul-André Melliès (CNRS, Université Paris Diderot)
    Noam Zeilberger (MSR-Inria)
  9. Safe and Efficient Gradual Typing for TypeScript
    Aseem Rastogi (University of Maryland, College Park)
    Nikhil Swamy (Microsoft Research)
    Cedric Fournet (Microsoft Research)
    Gavin Bierman (Oracle Labs)
    Panagiotis Vekris (University of California, San Diego)
  10. Sound Modular Verification of C Code Executing in an Unverified Context
    Pieter Agten (iMinds-DistriNet, KU Leuven)
    Bart Jacobs (iMinds-DistriNet, KU Leuven)
    Frank Piessens (iMinds-DistriNet, KU Leuven)
  11. Program Boosting: Program Synthesis via Crowd-Sourcing
    Robert A Cochran (University of North Carolina at Chapel Hill)
    Loris D'Antoni (University of Pennsylvania)
    Benjamin Livshits (Microsoft Research)
    David Molnar (Microsoft Research)
    Margus Veanes (Microsoft Research)
  12. Programming up to Congruence
    Vilhelm Sjöberg (University of Pennsylvania)
    Stephanie Weirich (University of Pennsylvania)
  13. Deep Specifications and Certified Abstraction Layers
    Ronghui Gu (Yale University)
    Jeremie Koenig (Yale University)
    Tahina Ramananandro (Yale University)
    Zhong Shao (Yale University)
    Newman Wu (Yale University)
    Shu-chun Weng (Yale University)
    Haozhong Zhang (University of Science and Technology of China)
    Yu Guo (University of Science and Technology of China)
  14. A Meta Lambda Calculus with Cross-Level Computation
    Kazunori Tobisawa (Graduate School of Mathematical Sciences, The University of Tokyo)
  15. Specification Inference Using Context-Free Language Reachability
    Osbert Bastani (Stanford University)
    Saswat Anand (Stanford University)
    Alex Aiken (Stanford Univeristy)
  16. Runtime enforcement of security policies on black box reactive programs
    Minh Ngo (University of Trento)
    Fabio Massacci (University of Trento)
    Dimiter Milushev (KU Leuven)
    Frank Piessens (KU Leuven)
  17. Faster Algorithms for Algebraic Path Properties in RSMs with Constant Treewidth
    Krishnendu Chatterjee (IST Austria)
    Prateesh Goyal (IIT Bombay)
    Rasmus Ibsen-Jensen (IST Austria)
    Andreas Pavlogiannis (IST Austria)
  18. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning
    Ralf Jung (MPI-SWS, Germany)
    David Swasey (MPI-SWS, Germany)
    Filip Sieczkowski (Aarhus University)
    Kasper Svendsen (Aarhus University)
    Aaron Turon (Mozilla Research)
    Lars Birkedal (Aarhus University)
    Derek Dreyer (MPI-SWS, Germany)
  19. DReX: A Declarative Language for Efficiently Computable Regular String Transformations
    Rajeev Alur (University of Pennsylvania)
    Loris D'Antoni (University of Pennsylvania)
    Mukund Raghothaman (University of Pennsylvania)
  20. K-Java: A Complete Semantics of Java
    Denis Bogdanas (Alexandru Ioan Cuza University Iasi, Romania)
    Grigore Rosu (University of Illinois at Urbana-Champaign)
  21. Higher Inductive Types as Homotopy-Initial Algebras
    Kristina Sojakova (Carnegie Mellon University)
  22. A Calculus for Relaxed Memory
    Karl Crary (Carnegie Mellon University)
    Michael Sullivan (Carnegie Mellon University)
  23. Compositional CompCert
    Gordon Stewart (Princeton University)
    Lennart Beringer (Princeton University)
    Santiago Cuellar (Princeton University)
    Andrew W. Appel (Princeton University)
  24. Abstract Symbolic Automata
    Mila Dalla Preda (University of Verona)
    Roberto Giacobazzi (University of Verona)
    Arun Lakhotia (University of Louisiana)
    Isabella Mastroeni (University of Verona)
  25. Analyzing Program Analyses
    Roberto Giacobazzi (University of Verona)
    Francesco Logozzo (Microsoft Research)
    Francesco Ranzato (University of Padova)
  26. Self-Representation in Girard's System U
    Matt Brown (UCLA)
    Jens Palsberg (UCLA)
  27. Conjugate Hylomorphisms: The Mother of All Structured Recursion Schemes
    Ralf Hinze (University of Oxford)
    Nicolas Wu (University of Oxford)
    Jeremy Gibbons (University of Oxford)
  28. Decentralizing SDN Policies
    Oded Padon (Tel Aviv University)
    Neil Immerman (University of Massachusetts, Amherst)
    Aleksandr Karbyshev (Tel Aviv University)
    Ori Lahav (Tel Aviv University)
    Mooly Sagiv (Tel Aviv University)
    Sharon Shoham (The Academic College of Tel Aviv Yaffo)
  29. Polymorphic Functions with Set-Theoretic Types. Part 2: Local Type Inference and Type Reconstruction
    Giuseppe Castagna (CNRS - Université Paris Diderot)
    Kim Nguyen (LRI - Université Paris Sud)
    Zhiwu Xu
    Pietro Abate (Université Paris Diderot)
  30. Principal Type Schemes for Gradual Programs
    Ronald Garcia (University of British Columbia)
    Matteo Cimini (Indiana University)
  31. Full Abstraction for Signal Flow Graphs
    Filippo Bonchi (Ecole Normale Supérieure yon; France)
    Pawel Sobocinski (University of Southampton, UK)
    Fabio Zanasi (Ecole Normale Supérieure Lyn,; France
  32. Dependent Information Flow Types
    Luísa Lourenço (CITI and NOVA-LINCS / Universidade Nova de Lisboa)
    Luís Caires (CITI and NOVA-LINCS / Universidade Nova de Lisboa)
  33. Common compiler optimisations are invalid in the C11 memory model and what we can do about it
    Viktor Vafeiadis (MPI-SWS)
    Thibaut Balabonski (INRIA)
    Soham Chakraborty (MPI-SWS)
    Robin Morisset (INRIA)
    Francesco Zappa Nardelli (INRIA)
  34. Manifest Contracts for Datatypes
    Taro Sekiyama (Kyoto University)
    Yuki Nishida (Kyoto University)
    Atsushi Igarashi (Kyoto University)
  35. Summary-Based Context-Sensitive Data-Dependence Analysis in Presence of Callbacks
    Hao Tang (Peking University, China)
    Xiaoyin Wang (University of Texas at San Antonio)
    Lingming Zhang (University of Texas at Dallas)
    Bing Xie (Peking University, China)
    Lu Zhang (Peking University, China)
    Hong Mei (Peking University, China)
  36. Leveraging Weighted Automata to Compositional Reasoning of Probabilistic Programs
    Fei He (Tsinghua University)
    Xiaowei Gao (Tsinghua University)
    Bow-Yaw Wang (Academia Sinica)
    Lijun Zhang (Institute of Software, Chinese Academy of Sciences)
  37. Algebraic effects linearity and quantum programming languages
    Sam Staton (Radboud University Nijmegen)
  38. Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy
    Gilles Barthe (IMDEA Software Institute)
    Marco Gaboardi (University of Dundee)
    Emilio Gallego Arias (University of Pennsylvania)
    Justin Hsu (University of Pennsylvania)
    Aaron Roth (University of Pennsylvania)
    Pierre-Yves Strub (IMDEA Software Institute)
  39. Probabilistic Termination
    Luis Maria Ferrer Fioriti (Saarland University)
    Holger Hermanns (Saarland University)
  40. Tractable Refinement Checking for Concurrent Objects
    Ahmed Bouajjani (LIAFA Université Paris Diderot; France)
    Michael Emmi (IMDEA Software Institute, Spain)
    Constantin Enea (LIAFA Université Paris Diderot; France)
    Jad Hamza (LIAFA Université Paris Diderot; France)
  41. From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification
    Adam Chlipala (MIT CSAIL)
  42. Ur/Web: A Simple Model for Programming the Web
    Adam Chlipala (MIT CSAIL)
  43. Differential Privacy: Now it's Getting Personal
    Hamid Ebadi (Chalmers University of Technology)
    David Sands (Chalmers University of Technology)
    Gerardo Schneider (Chalmers University of Technology)
  44. Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant
    Benjamin Delaware (MIT CSAIL)
    Clément Pit-Claudel (MIT CSAIL)
    Jason Gross (MIT CSAIL)
    Adam Chlipala (MIT CSAIL)
  45. Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests
    Damien Pous (CNRS, France)
  46. Succinct Representation of Concurrent Trace Sets
    Ashutosh Gupta (IST Austria)
    Thomas A. Henzinger (IST Austria)
    Arjun Radhakrishna (IST Austria)
    Roopsha Samanta (IST Austria)
    Thorsten Tarrach (IST Austria)
  47. Predicting Program Properties from Big Code
    Veselin Raychev (ETH Zurich)
    Martin Vechev (ETH Zurich)
    Andreas Krause (ETH Zurich)
  48. On Characterizing the Data Access Complexity of Programs
    Venmugil Elango (The Ohio State University)
    Fabrice Rastello (Inria)
    Louis-Noel Pouchet (University of California Los Angeles)
    J. Ramanujam (Louisiana State University)
    P. Sadayappan (The Ohio State University)
  49. A Coalgebraic Decision Procedure for NetKAT
    Nate Foster (Cornell University)
    Dexter Kozen (Cornell University)
    Matthew Milano (Cornell University)
    Alexandra Silva (Raboud University Nijmegen)
    Laure Thompson (Cornell University)
  50. Proof Spaces for Unbounded Parallelism
    Azadeh Farzan (University of Toronto)
    Zachary Kincaid (University of Toronto)
    Andreas Podelski (University of Freiburg)
  51. Towards the Essence of Hygiene
    Michael D. Adams (University of Utah, University of Illinois at Urbana/Champaign)
  52. Data Parallel String Manipulating Programs
    Margus Veanes (Microsoft Research)
    Todd Mytkowicz (Microsoft Research)
    David Molnar (Microsoft Research)
    Ben Livshits (Microsoft Research)