 |
POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming LanguagesTata Institute of Fundamental Research, Mumbai, India
|
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.
-
A Scalable, Correct Time-Stamped Stack
Mike Dodds (University of York)
Andreas Haas (University of Salzburg)
Christoph M. Kirsch (University of Salzburg) -
From Communicating Machines to Graphical Choreographies
Julien Lange (Imperial Colllege London)
Emilio Tuosto (University of Leicester)
Nobuko Yoshida (Imperial Colllege London) - Equations, contractions, and unique solutions
Davide Sangiorgi (University of Bologna and INRIA) -
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) - Space-Efficient Manifest Contracts
Michael Greenberg (Princeton University) -
Quantitative Interprocedural Analysis
Krishnendu Chatterjee (IST Austria)
Andreas Pavlogiannis (IST Austria)
Yaron Velner (Tel Aviv University) -
Integrating Linear and Dependent Types
Neel Krishnaswami (University of Birmingham)
Pierre Pradic (ENS Lyon)
Nick Benton (Microsoft Research) - Functors are type refinement systems
Paul-André Melliès (CNRS, Université Paris Diderot)
Noam Zeilberger (MSR-Inria) -
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) -
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) - 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) -
Programming up to Congruence
Vilhelm Sjöberg (University of Pennsylvania)
Stephanie Weirich (University of Pennsylvania) -
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) - A Meta Lambda Calculus with Cross-Level Computation
Kazunori Tobisawa (Graduate School of Mathematical Sciences, The University of Tokyo) - Specification Inference Using Context-Free Language Reachability
Osbert Bastani (Stanford University)
Saswat Anand (Stanford University)
Alex Aiken (Stanford Univeristy) - 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) - 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) -
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) -
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) -
K-Java: A Complete Semantics of Java
Denis Bogdanas (Alexandru Ioan Cuza University Iasi, Romania)
Grigore Rosu (University of Illinois at Urbana-Champaign) - Higher Inductive Types as Homotopy-Initial Algebras
Kristina Sojakova (Carnegie Mellon University) -
A Calculus for Relaxed Memory
Karl Crary (Carnegie Mellon University)
Michael Sullivan (Carnegie Mellon University) -
Compositional CompCert
Gordon Stewart (Princeton University)
Lennart Beringer (Princeton University)
Santiago Cuellar (Princeton University)
Andrew W. Appel (Princeton University) - Abstract Symbolic Automata
Mila Dalla Preda (University of Verona)
Roberto Giacobazzi (University of Verona)
Arun Lakhotia (University of Louisiana)
Isabella Mastroeni (University of Verona) - Analyzing Program Analyses
Roberto Giacobazzi (University of Verona)
Francesco Logozzo (Microsoft Research)
Francesco Ranzato (University of Padova) -
Self-Representation in Girard's System U
Matt Brown (UCLA)
Jens Palsberg (UCLA) - Conjugate Hylomorphisms: The Mother of All Structured Recursion Schemes
Ralf Hinze (University of Oxford)
Nicolas Wu (University of Oxford)
Jeremy Gibbons (University of Oxford) - 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) -
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) - Principal Type Schemes for Gradual Programs
Ronald Garcia (University of British Columbia)
Matteo Cimini (Indiana University) - 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 - 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) -
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) -
Manifest Contracts for Datatypes
Taro Sekiyama (Kyoto University)
Yuki Nishida (Kyoto University)
Atsushi Igarashi (Kyoto University) -
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) - 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) - Algebraic effects linearity and quantum programming languages
Sam Staton (Radboud University Nijmegen) -
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) - Probabilistic Termination
Luis Maria Ferrer Fioriti (Saarland University)
Holger Hermanns (Saarland University) - 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) -
From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification
Adam Chlipala (MIT CSAIL) -
Ur/Web: A Simple Model for Programming the Web
Adam Chlipala (MIT CSAIL) - 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) -
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) -
Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests
Damien Pous (CNRS, France) -
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) -
Predicting Program Properties from Big Code
Veselin Raychev (ETH Zurich)
Martin Vechev (ETH Zurich)
Andreas Krause (ETH Zurich) - 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) -
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) - Proof Spaces for Unbounded Parallelism
Azadeh Farzan (University of Toronto)
Zachary Kincaid (University of Toronto)
Andreas Podelski (University of Freiburg) - Towards the Essence of Hygiene
Michael D. Adams (University of Utah, University of Illinois at Urbana/Champaign) - Data Parallel String Manipulating Programs
Margus Veanes (Microsoft Research)
Todd Mytkowicz (Microsoft Research)
David Molnar (Microsoft Research)
Ben Livshits (Microsoft Research)