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.
'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
(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
(preprint)
by Jean Pichon-Pharabod, Peter Sewell
Abstracting Gradual Typing
(preprint)
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
(preprint)
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
(preprint)
by Damien Octeau, Somesh Jha, Matthew Dering, Patrick McDaniel, Alexandre Bartel, Hongyu Li, Jacques Klein, Yves Le Traon
Decidability of Inferring Inductive Invariants
(preprint)
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
(preprint)
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
(preprint)
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
(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
(draft)
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
(preprint)
by Aws Albarghouthi, Isil Dillig, Arie Gurfinkel
Memoryful Geometry of Interaction II: Recursion and Adequacy
(preprint)
by Koko Muroya, Naohiko Hoshino, Ichiro Hasuo
Model Checking for Symbolic-Heap Separation Logic with Inductive Predicates
(preprint)
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
(preprint)
by Thomas Reps, Emma Turetsky, Prathmesh Prabhu
Optimizing Synthesis with Metasketches
(preprint)
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
(preprint)
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
(preprint)
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
(preprint)
by Xin Zhang, Ravi Mangal, Aditya Nori, Mayur Naik
Reducing Crash Recoverability to Reachability
(preprint)
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
(preprint)
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
(preprint from arXiv)
by Anthony Widjaja Lin, Pablo Barcelo
Symbolic Abstract Data Type Inference
(preprint)
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
(preprint)
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
(preprint)
by Matteo Cimini, Jeremy Siek
The Hardness of Data Packing
(preprint)
by Rahman Lavaee, Chen Ding
Transforming Spreadsheet Data Types using Examples
(preprint)
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
(long version from arXiv)
by Matthew Hague, Jonathan Kochems, C.-H. Luke Ong