popl2016-papers

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
  (preprint)
  by Alexey Gotsman, Hongseok Yang, Carla Ferreira, Mahsa Najafzadeh, Marc Shapiro

• A Program Logic for Concurrent Objects under Fair Scheduling
  by Hongjin Liang, Xinyu Feng

• A Theory of Effects and Resources: Adjunction Models and Polarised Calculi
  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
  by Radu Grigore, Hongseok Yang

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

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

• Binding as Sets of Scopes
  by Matthew Flatt

• Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega
  (no preprint found) (website)
  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

• Certified Causally Consistent Distributed Key-Value Stores
  (no preprint found) (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
  by Dominic Orchard, Nobuko Yoshida

• Environmental Bisimulations for Probabilistic Higher-Order Languages
  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
  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?
  by Asumu Takikawa, Daniel Feltey, Ben Greenman, Max New, Jan Vitek, Matthias Felleisen

• Kleenex: Compiling Nondeterministic Transducers to Deterministic Streaming Transducers
  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
  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
  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
  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 from 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
  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
  by Fan Long, Martin Rinard

• Pushdown Control-flow Analysis for Free
  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
  (preprint)
  by Florian Lorenzen, Sebastian Erdweg

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

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

• System Fω with Equirecursive Types for Datatype-generic Programming
  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
  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
  (preprint)
  by Thorsten Altenkirch, Ambrus Kaposi

• Unboundedness and Downward Closures of Higher-Order Pushdown Automata
  by Matthew Hague, Jonathan Kochems, C.-H. Luke Ong