Links to publicly available preprints for the POPL'16 conference
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Failed to load latest commit information.


Links to accepted papers for the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016). Pull requests welcome!

(Similar pages are available for POPL 2015, POPL 2014, and 2013, ICFP (2012, 2013, 2014) and PLDI 2014.)

Note: the POPL'16 website, powered by the increasingly convenient conf.researchr platform, has nice eye-candy display of paper abstract on click, etc, and they also have the ability to link to article preprints. Unfortunately, we couldn't find any information on how to contribute such links, so git repositories still remain the most convenient way to help crowd-source preprint gathering. We hope to be able to contribute the links contributed here to their platform, to benefit an even larger audience.

POPL 2016

  • 'Cause I'm Strong Enough: Reasoning about Consistency Choices in Distributed Systems
    by Alexey Gotsman, Hongseok Yang, Carla Ferreira, Mahsa Najafzadeh, Marc Shapiro

  • A Program Logic for Concurrent Objects under Fair Scheduling
    (preprint) (extended version)
    by Hongjin Liang, Xinyu Feng

  • A Theory of Effects and Resources: Adjunction Models and Polarised Calculi
    (author's version)
    by Pierre-Louis Curien, Marcelo Fiore, Guillaume Munch-Maccagnoni

  • A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions
    by Jean Pichon-Pharabod, Peter Sewell

  • Abstracting Gradual Typing
    by Ronald Garcia, Alison M. Clark, Éric Tanter

  • Abstraction Refinement Guided by a Learnt Probabilistic Model
    (preprint from arXiv)
    by Radu Grigore, Hongseok Yang

  • Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs
    (preprint from arXiv)
    by Krishnendu Chatterjee, Hongfei Fu, Rouzbeh Hasheminezhad, Petr Novotny

  • Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components
    (preprint from arxiv)
    by Krishnendu Chatterjee, Rasmus Ibsen-Jensen, Andreas Pavlogiannis

  • Binding as Sets of Scopes
    (preprint) (earlier version in HTML format) (artifact)
    by Matthew Flatt

  • Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega
    (paper website) (preprint) (artifact)
    by Matt Brown, Jens Palsberg

  • Casper: An Efficient Approach to Call Trace Collection
    by Rongxin Wu, Xiao Xiao, Shing-Chi Cheung, Hongyu Zhang, Charles Zhang

  • Chapar: Certified Causally Consistent Distributed Key-Value Stores
    (preprint) (website)
    by Mohsen Lesani, Christian J. Bell, Adam Chlipala

  • Combining Static Analysis with Probabilistic Models to Enable Market-Scale Analysis
    by Damien Octeau, Somesh Jha, Matthew Dering, Patrick McDaniel, Alexandre Bartel, Hongyu Li, Jacques Klein, Yves Le Traon

  • Decidability of Inferring Inductive Invariants
    by Oded Padon, Neil Immermal, Sharon Shoham, Aleksandr Karbyshev, Mooly Sagiv

  • Dependent Types and Multi-Monadic Effects in F*
    (paper website) (preprint)
    by Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cedric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, Santiago Zanella-Beguelin

  • Effects as sessions, sessions as effects
    (preprint) (artifact)
    by Dominic Orchard, Nobuko Yoshida

  • Environmental Bisimulations for Probabilistic Higher-Order Languages
    (preprint (weblink))
    by Davide Sangiorgi, Valeria Vignudelli

  • Estimating types in binaries using predictive modeling
    by Omer Katz, Ran El-Yaniv, Eran Yahav

  • Example-Directed Synthesis: A Type-Theoretic Interpretation
    (preprint) (website)
    by Jonathan Frankle, Peter-Michael Osera, David Walker, Steve Zdancewic

  • Fabular: Regression Formulas as Probabilistic Programming
    by Johannes Borgstrom, Andrew D. Gordon, Long Ouyang, Claudio Russo, Adam Scibior, Marcin Szymczak

  • From MinX to MinC: Semantics-Driven Decompilation of Recursive Datatypes
    by Ed Robbins, Andy King, Tom Schrijvers

  • Fully-Abstract Compilation by Approximate Back-Translation
    (preprint) (technical appendix)
    by Dominique Devriese, Marco Patrignani, Frank Piessens

  • Is Sound Gradual Typing Dead?
    (preprint) (artifact)
    by Asumu Takikawa, Daniel Feltey, Ben Greenman, Max New, Jan Vitek, Matthias Felleisen

  • Kleenex: Compiling Nondeterministic Transducers to Deterministic Streaming Transducers
    (preprint) (IFIP WG 2.8 slides)
    by Bjørn Bugge Grathwohl, Fritz Henglein, Ulrik Terp Rasmussen, Kristoffer Aalund Søholm, Sebastian Paaske Tørholm

  • Lattice-Theoretic Progress Measures and Coalgebraic Model Checking
    (preprint from arXiv)
    by Ichiro Hasuo, Shunsuke Shimizu, Corina Cirstea

  • Learning Invariants using Decision Trees and Implication Counterexamples
    by Pranav Garg, Daniel Neider, P. Madhusudan, Dan Roth

  • Lightweight Verification of Separate Compilation
    (paper website) (preprint)
    by Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis

  • Maximal Specification Synthesis
    by Aws Albarghouthi, Isil Dillig, Arie Gurfinkel

  • Memoryful Geometry of Interaction II: Recursion and Adequacy
    by Koko Muroya, Naohiko Hoshino, Ichiro Hasuo

  • Model Checking for Symbolic-Heap Separation Logic with Inductive Predicates
    by James Brotherston, Nikos Gorogiannis, Max Kanovich, Reuben Rowe

  • Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA
    (paper website) (preprint)
    by Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Luc Maranget, Ali Sezgin, Will Deacon, Peter Sewell

  • Monitors and Blame Assignment for Higher-Order Session Types
    (technical report (TR website))
    by Limin Jia, Hannah Gommerstadt, Frank Pfenning

  • Newtonian Program Analysis via Tensor Product
    by Thomas Reps, Emma Turetsky, Prathmesh Prabhu

  • Optimizing Synthesis with Metasketches
    by James Bornholt, Emina Torlak, Dan Grossman, Luis Ceze

  • Overhauling SC atomics in C11 and OpenCL
    (preprint, also available on arXiv)
    by John Wickerson, Mark Batty, Alastair Donaldson

  • PSync: a partially synchronous language for fault-tolerant distributed algorithms
    by Cezara Drăgoi, Thomas A. Henzinger, Damien Zufferey

  • PolyCheck: Dynamic Verification of Iteration Space Transformations on Affine Programs
    by Wenlei Bao, Sriram Krishnamoorthy, Louis-Noel Pouchet, Fabrice Rastello, P. (Saday) Sadayappan

  • Principal Type Inference for GADTs
    by Sheng Chen, Martin Erwig

  • Printing Floating-Point Numbers: A Faster, Always Correct Method
    (preprint) by Marc Andrysco, Ranjit Jhala, Sorin Lerner

  • Program Synthesis with Noise
    by Veselin Raychev, Pavol Bielik, Martin Vechev, Andreas Krause

  • Prophet: Automatic Patch Generation via Learning from Successful Patches
    (technical report (uri))
    by Fan Long, Martin Rinard

  • Pushdown Control-flow Analysis for Free
    (preprint from arXiv)
    by Thomas Gilray, Steven Lyde, Michael D. Adams, Matthew Might, David Van Horn

  • Query-Guided Maximum Satisfiability
    by Xin Zhang, Ravi Mangal, Aditya Nori, Mayur Naik

  • Reducing Crash Recoverability to Reachability
    by Eric Koskinen, Junfeng Yang

  • SMO: An Integrated Approach to Intra-Array and Inter-Array Storage Optimization
    by Somashekaracharya G Bhaskaracharya, Uday Bondhugula, Albert Cohen

  • Satisfiability Modulo Differential Equivalence Relations
    by Luca Cardelli, Mirco Tribastone, Max Tschaikowski, Andrea Vandin

  • Scaling Network Verification using Symmetry and Surgery
    by Gordon Plotkin, Nikolaj Bjørner, Nuno P. Lopes, Andrey Rybalchenko, George Varghese

  • Sound Type-dependent Syntactic Language Extension
    by Florian Lorenzen, Sebastian Erdweg

  • String Solving with Word Equations and Transducers: Decidability and Applications to Detecting Mutation XSS
    (preprint from arXiv)
    by Anthony Widjaja Lin, Pablo Barcelo

  • Symbolic Abstract Data Type Inference
    by Michael Emmi, Constantin Enea

  • System F-omega with Equirecursive Types for Datatype-Generic Programming
    (preprint) (technical report) (project website)
    by Yufei Cai, Paolo G. Giarrusso, Klaus Ostermann

  • Taming Release-Acquire Consistency
    (paper website) (preprint)
    by Ori Lahav, Nick Giannarakis, Viktor Vafeiadis

  • Temporal Verification of Higher-order Functional Programs
    by Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno

  • The Complexity of Interaction
    (long version from arXiv)
    by Stéphane Gimenez, Georg Moser

  • The Gradualizer: a methodology and algorithm for generating gradual type systems
    by Matteo Cimini, Jeremy Siek

  • The Hardness of Data Packing
    by Rahman Lavaee, Chen Ding

  • Transforming Spreadsheet Data Types using Examples
    by Rishabh Singh, Sumit Gulwani

  • Type Theory in Type Theory using Quotient Inductive Types
    by Thorsten Altenkirch, Ambrus Kaposi

  • Unboundedness and Downward Closures of Higher-Order Pushdown Automata
    (long version from arXiv)
    by Matthew Hague, Jonathan Kochems, C.-H. Luke Ong