Links to accepted papers for the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2015). Pull requests welcome!
(Similar pages are available for POPL 2016, POPL 2014, and 2013, ICFP (2012, 2013, 2014) and PLDI 2014.)
Status of links at last commit:
-
A Scalable, Correct Time-Stamped Stack
(paper)
by Mike Dodds, Andreas Haas and Christoph M. Kirsch -
From Communicating Machines to Graphical Choreographies
(preprint)
by Julien Lange, Emilio Tuosto and Nobuko Yoshida -
Equations, contractions, and unique solutions
(paper)
by Davide Sangiorgi -
Formal verification of a C static analyzer
(paper)
by Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy and David Pichardie -
Space-Efficient Manifest Contracts
(paper | tech report)
by Michael Greenberg -
Quantitative Interprocedural Analysis
by Krishnendu Chatterjee, Andreas Pavlogiannis and Yaron Velner -
Integrating Linear and Dependent Types
(paper)
by Neel Krishnaswami, Pierre Pradic and Nick Benton -
Functors are type refinement systems
(paper)
by Paul-André Melliès, Noam Zeilberger -
Safe and Efficient Gradual Typing for TypeScript
(tech report)
by Aseem Rastogi, Nikhil Swamy, Cedric Fournet, Gavin Bierman and Panagiotis Vekris -
Sound Modular Verification of C Code Executing in an Unverified Context
(paper)
by Pieter Agten, Bart Jacobs and Frank Piessens -
Program Boosting: Program Synthesis via Crowd-Sourcing
(paper)
by Robert A Cochran, Loris D'Antoni, Benjamin Livshits, David Molnar and Margus Veanes -
Programming up to Congruence
(paper)
by Vilhelm Sjöberg and Stephanie Weirich -
Deep Specifications and Certified Abstraction Layers
(paper | tech report | site)
by Ronghui Gu, Jeremie Koenig, Tahina Ramananandro, Zhong Shao, Newman Wu, Shu-chun Weng, Haozhong Zhang and Yu Guo -
A Meta Lambda Calculus with Cross-Level Computation
by Kazunori Tobisawa -
Specification Inference Using Context-Free Language Reachability
(paper)
by Osbert Bastani, Saswat Anand, Alex Aiken and Osbert Bastani -
Runtime enforcement of security policies on black box reactive programs
(paper)
by Minh Ngo, Fabio Massacci, Dimiter Milushev and Frank Piessens -
Faster Algorithms for Algebraic Path Properties in RSMs with Constant Treewidth
(arxiv)
by Krishnendu Chatterjee, Prateesh Goyal, Rasmus Ibsen-Jensen and Andreas Pavlogiannis -
Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning
(paper)
by Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal and Derek Dreyer -
DReX: A Declarative Language for Efficiently Computable Regular String Transformations
(draft paper)
by Rajeev Alur, Loris D'Antoni and Mukund Raghothaman -
K-Java: A Complete Semantics of Java
(paper)
by Denis Bogdanas and Grigore Rosu -
Higher Inductive Types as Homotopy-Initial Algebras
(arxiv)
by Kristina Sojakova -
A Calculus for Relaxed Memory
（paper)
by Karl Crary and Michael Sullivan -
Compositional CompCert
(paper)
by Gordon Stewart, Lennart Beringer, Santiago Cuellar and Andrew W. Appel -
Abstract Symbolic Automata
(draft paper)
by Mila Dalla Preda, Roberto Giacobazzi, Arun Lakhotia and Isabella Mastroeni -
Analyzing Program Analyses
by Roberto Giacobazzi, Francesco Logozzo and Francesco Ranzato -
Self-Representation in Girard's System U
(paper)
by Matt Brown and Jens Palsberg -
Conjugate Hylomorphisms: The Mother of All Structured Recursion Schemes
(draft paper)
by Ralf Hinze, Nicolas Wu and Jeremy Gibbons -
Decentralizing SDN Policies
(paper)
by Oded Padon, Neil Immerman, Aleksandr Karbyshev, Ori Lahav, Mooly Sagiv and Sharon Shoham -
Polymorphic Functions with Set-Theoretic Types. Part 2: Local Type Inference and Type Reconstruction
(paper)
by Giuseppe Castagna, Kim Nguyen, Zhiwu Xu and Pietro Abate -
Principal Type Schemes for Gradual Programs
by Ronald Garcia and Matteo Cimini -
Full Abstraction for Signal Flow Graphs
(academia)
by Filippo Bonchi, Pawel Sobocinski and Fabio Zanasi -
Dependent Information Flow Types
(paper)
by Luísa Lourenço and Luís Caires -
Common compiler optimisations are invalid in the C11 memory model and what we can do about it
(paper)
by Viktor Vafeiadis, Thibaut Balabonski, Soham Chakraborty, Robin Morisset and Francesco Zappa Nardelli -
Manifest Contracts for Datatypes
by Taro Sekiyama, Yuki Nishida and Atsushi Igarashi -
Summary-Based Context-Sensitive Data-Dependence Analysis in Presence of Callbacks
(paper)
by Hao Tang, Xiaoyin Wang, Lingming Zhang, Bing Xie, Lu Zhang and Hong Mei -
Leveraging Weighted Automata to Compositional Reasoning of Probabilistic Programs
by Fei He, Xiaowei Gao, Bow-Yaw Wang and Lijun Zhang -
Algebraic effects linearity and quantum programming languages
(paper)
by Sam Staton -
Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy
(arxiv)
by Gilles Barthe, Marco Gaboardi, Emilio Gallego Arias, Justin Hsu, Aaron Roth and Pierre-Yves Strub -
Probabilistic Termination
by Luis Maria Ferrer Fioriti and Holger Hermanns -
Tractable Refinement Checking for Concurrent Objects
(paper)
by Ahmed Bouajjani, Michael Emmi, Constantin Enea and Jad Hamza -
From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification
(paper) by Adam Chlipala -
Ur/Web: A Simple Model for Programming the Web
(paper) by Adam Chlipala -
Differential Privacy: Now it's Getting Personal
(paper | site)
by Hamid Ebadi, David Sands and Gerardo Schneider -
Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant
(paper) by Benjamin Delaware, Clément Pit-Claudel, Jason Gross and Adam Chlipala -
Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests
(arxiv)
by Damien Pous -
Succinct Representation of Concurrent Trace Sets
(paper)
by Ashutosh Gupta, Thomas A. Henzinger, Arjun Radhakrishna, Roopsha Samanta and Thorsten Tarrach -
Predicting Program Properties from Big Code
(paper | site | tool)
by Veselin Raychev, Martin Vechev and Andreas Krause -
On Characterizing the Data Access Complexity of Programs
(arxiv)
by Venmugil Elango, Fabrice Rastello, Louis-Noel Pouchet, J. Ramanujam and P. Sadayappan -
A Coalgebraic Decision Procedure for NetKAT
(research report (13 pages))
by Nate Foster, Dexter Kozen, Matthew Milano, Alexandra Silva and Laure Thompson -
Proof Spaces for Unbounded Parallelism
(paper)
by Azadeh Farzan, Zachary Kincaid and Andreas Podelski -
The Essence of Hygiene
(preprint)
by Michael D. Adams -
Data Parallel String Manipulating Programs
(paper)
by Margus Veanes, Todd Mytkowicz, David Molnar and Ben Livshits