Skip to content

Latest commit

 

History

History
274 lines (208 loc) · 14.9 KB

README.md

File metadata and controls

274 lines (208 loc) · 14.9 KB
Raw

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
    (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