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
(preprint from arXiv)
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
(preprint) (paper in HTML format) (artifact)
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
(preprint)
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
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
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
(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
(preprint)
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
(preprint)
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