POPL 2016 – Proceedings

43rd ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2016), January 20–22, 2016, St. Petersburg, FL, USA

Frontmatter

Keynotes

Programming the World of Uncertain Things (Keynote)
Kathryn S. McKinley
(Microsoft Research, USA)
Article: popl16key-key2-p (type: Invited Talk Abstract (2 page)) doi:

Synthesis of Reactive Controllers for Hybrid Systems (Keynote)
Richard M. Murray
(California Institute of Technology, USA)
Article: popl16key-key1-p (type: Invited Talk Abstract (2 page)) doi:

Confluences in Programming Languages Research (Keynote)
David Walker
(Princeton University, USA)
Article: popl16key-key3-p (type: Invited Talk Abstract (2 page)) doi:

Research Papers

Types and Foundations

Breaking through the Normalization Barrier: A Self-Interpreter for F-omega
Matt Brown and Jens Palsberg
(University of California at Los Angeles, USA)
Article: popl16main-mainpopl16-57-p (type: Full Paper (12 pages + refs)) doi:

Type Theory in Type Theory using Quotient Inductive Types
Thorsten Altenkirch and Ambrus Kaposi
(University of Nottingham, UK)
Article: popl16main-mainpopl16-157-p (type: Full Paper (12 pages + refs)) doi:

System F-omega with Equirecursive Types for Datatype-Generic Programming
Yufei Cai, Paolo G. Giarrusso, and Klaus Ostermann
(University of Tübingen, Germany)
Article: popl16main-mainpopl16-68-p (type: Full Paper (12 pages + refs)) doi:

A Theory of Effects and Resources: Adjunction Models and Polarised Calculi
Pierre-Louis Curien, Marcelo Fiore, and Guillaume Munch-Maccagnoni
(University of Paris Diderot, France; Inria, France; University of Cambridge, UK)
Article: popl16main-mainpopl16-216-p (type: Full Paper (12 pages + refs)) doi:

Algorithmic Verification

Temporal Verification of Higher-Order Functional Programs
Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, and Hiroshi Unno
(Nagoya University, Japan; JAIST, Japan; University of Tokyo, Japan; University of Tsukuba, Japan)
Article: popl16main-mainpopl16-309-p (type: Full Paper (12 pages + refs)) doi:

Scaling Network Verification using Symmetry and Surgery
Gordon D. Plotkin, Nikolaj Bjørner, Nuno P. Lopes, Andrey Rybalchenko, and George Varghese
(University of Edinburgh, UK; Microsoft Research, USA; Microsoft Research, UK)
Article: popl16main-mainpopl16-245-p (type: Full Paper (12 pages + refs)) doi:

Model Checking for Symbolic-Heap Separation Logic with Inductive Predicates
James Brotherston, Nikos Gorogiannis, Max Kanovich, and Reuben Rowe
(University College London, UK; Middlesex University, UK; National Research University Higher School of Economics, Russia)
Article: popl16main-mainpopl16-54-p (type: Full Paper (12 pages + refs)) doi:

Reducing Crash Recoverability to Reachability
Eric Koskinen and Junfeng Yang
(Yale University, USA; Columbia University, USA)
Article: popl16main-mainpopl16-199-p (type: Full Paper (12 pages + refs)) doi:

Decision Procedures

Query-Guided Maximum Satisfiability
Xin Zhang, Ravi Mangal, Aditya V. Nori, and Mayur Naik
(Georgia Institute of Technology, USA; Microsoft Research, UK)
Article: popl16main-mainpopl16-247-p (type: Full Paper (12 pages + refs)) doi:

String Solving with Word Equations and Transducers: Towards a Logic for Analysing Mutation XSS
Anthony W. Lin and Pablo Barceló
(Yale-NUS College, Singapore; University of Chile, Chile)
Article: popl16main-mainpopl16-166-p (type: Full Paper (12 pages + refs)) doi:

Symbolic Computation of Differential Equivalences
Luca Cardelli, Mirco Tribastone, Max Tschaikowski, and Andrea Vandin
(Microsoft Research, UK; University of Oxford, UK; IMT Lucca, Italy)
Article: popl16main-mainpopl16-207-p (type: Full Paper (12 pages + refs)) doi:

Unboundedness and Downward Closures of Higher-Order Pushdown Automata
Matthew Hague, Jonathan Kochems, and C.-H. Luke Ong
(University of London, UK; University of Oxford, UK)
Article: popl16main-mainpopl16-70-p (type: Full Paper (12 pages + refs)) doi:

Correct Compilation

Fully-Abstract Compilation by Approximate Back-Translation
Dominique Devriese, Marco Patrignani, and Frank Piessens
(KU Leuven, Belgium)
Article: popl16main-mainpopl16-21-p (type: Full Paper (12 pages + refs)) doi:

Lightweight Verification of Separate Compilation
Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, and Viktor Vafeiadis
(Seoul National University, South Korea; MPI-SWS, Germany)
Article: popl16main-mainpopl16-171-p (type: Full Paper (12 pages + refs)) doi:

From MinX to MinC: Semantics-Driven Decompilation of Recursive Datatypes
Ed Robbins, Andy King, and Tom Schrijvers
(University of Kent, UK; KU Leuven, Belgium)
Article: popl16main-mainpopl16-119-p (type: Full Paper (12 pages + refs)) doi:

Sound Type-Dependent Syntactic Language Extension
Florian Lorenzen and Sebastian Erdweg
(TU Berlin, Germany; TU Darmstadt, Germany)
Article: popl16main-mainpopl16-180-p (type: Full Paper (12 pages + refs)) doi:

Decidability and Complexity

Decidability of Inferring Inductive Invariants
Oded Padon, Neil Immerman, Sharon Shoham, Aleksandr Karbyshev, and Mooly Sagiv
(Tel Aviv University, Israel; University of Massachusetts at Amherst, USA; Academic College of Tel Aviv Yaffo, Israel)
Article: popl16main-mainpopl16-160-p (type: Full Paper (12 pages + refs)) doi:

The Hardness of Data Packing
Rahman Lavaee
(University of Rochester, USA)
Article: popl16main-mainpopl16-312-p (type: Full Paper (12 pages + refs)) doi:

The Complexity of Interaction
Stéphane Gimenez and Georg Moser
(University of Innsbruck, Austria)
Article: popl16main-mainpopl16-191-p (type: Full Paper (12 pages + refs)) doi:

Language Design

Dependent Types and Multi-monadic Effects in F*
Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, and Santiago Zanella-Béguelin
(Microsoft Research, USA; Inria, France; University of Maryland, USA; ENS, France; IMDEA Software Institute, Spain; Microsoft Research, UK)
Article: popl16main-mainpopl16-230-p (type: Full Paper (12 pages + refs)) doi:

Fabular: Regression Formulas as Probabilistic Programming
Johannes Borgström, Andrew D. Gordon, Long Ouyang, Claudio Russo, Adam Ścibior, and Marcin Szymczak
(Uppsala University, Sweden; Microsoft Research, UK; University of Edinburgh, UK; Stanford University, USA; University of Cambridge, UK; MPI Tübingen, Germany)
Article: popl16main-mainpopl16-220-p (type: Full Paper (12 pages + refs)) doi:

Kleenex: Compiling Nondeterministic Transducers to Deterministic Streaming Transducers
Bjørn Bugge Grathwohl, Fritz Henglein, Ulrik Terp Rasmussen, Kristoffer Aalund Søholm, and Sebastian Paaske Tørholm
(University of Copenhagen, Denmark; Jobindex, Denmark)
Article: popl16main-mainpopl16-195-p (type: Full Paper (12 pages + refs)) doi:

Probabilistic and Statistical Analysis

Automatic Patch Generation by Learning Correct Code
Fan Long and Martin Rinard
(Massachusetts Institute of Technology, USA)
Article: popl16main-mainpopl16-12-p (type: Full Paper (12 pages + refs)) doi:

Estimating Types in Binaries using Predictive Modeling
Omer Katz, Ran El-Yaniv, and Eran Yahav
(Technion, Israel)
Article: popl16main-mainpopl16-342-p (type: Full Paper (12 pages + refs)) doi:

Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs
Krishnendu Chatterjee, Hongfei Fu, Petr Novotný, and Rouzbeh Hasheminezhad
(IST Austria, Austria; Institute of Software at Chinese Academy of Sciences, China; Sharif University of Technology, Iran)
Article: popl16main-mainpopl16-159-p (type: Full Paper (12 pages + refs)) doi:

Transforming Spreadsheet Data Types using Examples
Rishabh Singh and Sumit Gulwani
(Microsoft Research, USA)
Article: popl16main-mainpopl16-310-p (type: Full Paper (12 pages + refs)) doi:

Foundations of Distributed Systems

Chapar: Certified Causally Consistent Distributed Key-Value Stores
Mohsen Lesani, Christian J. Bell, and Adam Chlipala
(Massachusetts Institute of Technology, USA)
Article: popl16main-mainpopl16-56-p (type: Full Paper (12 pages + refs)) doi:

'Cause I'm Strong Enough: Reasoning about Consistency Choices in Distributed Systems
Alexey Gotsman, Hongseok Yang, Carla Ferreira, Mahsa Najafzadeh, and Marc Shapiro
(IMDEA Software Institute, Spain; University of Oxford, UK; Universidade Nova Lisboa, Potugal; Sorbonne, France; Inria, France; UPMC, France)
Article: popl16main-mainpopl16-65-p (type: Full Paper (12 pages + refs)) doi:

A Program Logic for Concurrent Objects under Fair Scheduling
Hongjin Liang and Xinyu Feng
(University of Science and Technology of China, China)
Article: popl16main-mainpopl16-139-p (type: Full Paper (12 pages + refs)) doi:

PSync: A Partially Synchronous Language for Fault-Tolerant Distributed Algorithms
Cezara Drăgoi, Thomas A. Henzinger, and Damien Zufferey
(Inria, France; ENS, France; CNRS, France; IST Austria, Austria; Massachusetts Institute of Technology, USA)
Article: popl16main-mainpopl16-212-p (type: Full Paper (12 pages + refs)) doi:

Types, Generally or Gradually

Principal Type Inference for GADTs
Sheng Chen and Martin Erwig
(University of Louisiana at Lafayette, USA; Oregon State University, USA)
Article: popl16main-mainpopl16-286-p (type: Full Paper (12 pages + refs)) doi:

Abstracting Gradual Typing
Ronald Garcia, Alison M. Clark, and Éric Tanter
(University of British Columbia, Canada; University of Chile, Chile)
Article: popl16main-mainpopl16-314-p (type: Full Paper (12 pages + refs)) doi:

The Gradualizer: A Methodology and Algorithm for Generating Gradual Type Systems
Matteo Cimini and Jeremy G. Siek
(Indiana University, USA)
Article: popl16main-mainpopl16-91-p (type: Full Paper (12 pages + refs)) doi:

Is Sound Gradual Typing Dead?
Asumu Takikawa, Daniel Feltey, Ben Greenman, Max S. New, Jan Vitek, and Matthias Felleisen
(Northeastern University, USA)
Article: popl16main-mainpopl16-81-p (type: Full Paper (12 pages + refs)) doi:

Learning and Verification

Combining Static Analysis with Probabilistic Models to Enable Market-Scale Android Inter-component Analysis
Damien Octeau, Somesh Jha, Matthew Dering, Patrick McDaniel, Alexandre Bartel, Li Li, Jacques Klein, and Yves Le Traon
(University of Wisconsin, USA; Pennsylvania State University, USA; IMDEA Software Institute, Spain; TU Darmstadt, Germany; University of Luxembourg, Luxembourg)
Article: popl16main-mainpopl16-257-p (type: Full Paper (12 pages + refs)) doi:

Abstraction Refinement Guided by a Learnt Probabilistic Model
Radu Grigore and Hongseok Yang
(University of Oxford, UK)
Article: popl16main-mainpopl16-269-p (type: Full Paper (12 pages + refs)) doi:

Learning Invariants using Decision Trees and Implication Counterexamples
Pranav Garg, Daniel Neider, P. Madhusudan, and Dan Roth
(University of Illinois at Urbana-Champaign, USA)
Article: popl16main-mainpopl16-278-p (type: Full Paper (12 pages + refs)) doi:

Symbolic Abstract Data Type Inference
Michael Emmi and Constantin Enea
(IMDEA Software Institute, Spain; University of Paris Diderot, France)
Article: popl16main-mainpopl16-187-p (type: Full Paper (12 pages + refs)) doi:

Optimization

SMO: An Integrated Approach to Intra-array and Inter-array Storage Optimization
Somashekaracharya G. Bhaskaracharya, Uday Bondhugula, and Albert Cohen
(Indian Institute of Science, India; National Instruments, India; Inria, France; ENS, France)
Article: popl16main-mainpopl16-150-p (type: Full Paper (12 pages + refs)) doi:

PolyCheck: Dynamic Verification of Iteration Space Transformations on Affine Programs
Wenlei Bao, Sriram Krishnamoorthy, Louis-Noël Pouchet, Fabrice Rastello, and P. Sadayappan
(Ohio State University, USA; Pacific Northwest National Laboratory, USA; Inria, France)
Article: popl16main-mainpopl16-237-p (type: Full Paper (12 pages + refs)) doi:

Printing Floating-Point Numbers: A Faster, Always Correct Method
Marc Andrysco, Ranjit Jhala, and Sorin Lerner
(University of California at San Diego, USA)
Article: popl16main-mainpopl16-225-p (type: Full Paper (12 pages + refs)) doi:

Sessions and Processes

Effects as Sessions, Sessions as Effects
Dominic Orchard and Nobuko Yoshida
(Imperial College London, UK)
Article: popl16main-mainpopl16-123-p (type: Full Paper (12 pages + refs)) doi:

Monitors and Blame Assignment for Higher-Order Session Types
Limin Jia, Hannah Gommerstadt, and Frank Pfenning
(Carnegie Mellon University, USA)
Article: popl16main-mainpopl16-265-p (type: Full Paper (12 pages + refs)) doi:

Environmental Bisimulations for Probabilistic Higher-Order Languages
Davide Sangiorgi and Valeria Vignudelli
(University of Bologna, Italy; Inria, France)
Article: popl16main-mainpopl16-215-p (type: Full Paper (12 pages + refs)) doi:

Semantics and Memory Models

Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA
Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, and Peter Sewell
(University of Cambridge, UK; University of St. Andrews, UK; Inria, France; ARM, UK)
Article: popl16main-mainpopl16-4-p (type: Full Paper (12 pages + refs)) doi:

A Concurrency Semantics for Relaxed Atomics that Permits Optimisation and Avoids Thin-Air Executions
Jean Pichon-Pharabod and Peter Sewell
(University of Cambridge, UK)
Article: popl16main-mainpopl16-5-p (type: Full Paper (12 pages + refs)) doi:

Overhauling SC Atomics in C11 and OpenCL
Mark Batty, Alastair F. Donaldson, and John Wickerson
(University of Kent, UK; Imperial College London, UK)
Article: popl16main-mainpopl16-156-p (type: Full Paper (12 pages + refs)) doi:

Taming Release-Acquire Consistency
Ori Lahav, Nick Giannarakis, and Viktor Vafeiadis
(MPI-SWS, Germany)
Article: popl16main-mainpopl16-173-p (type: Full Paper (12 pages + refs)) doi:

Program Design and Analysis

Newtonian Program Analysis via Tensor Product
Thomas Reps, Emma Turetsky, and Prathmesh Prabhu
(University of Wisconsin-Madison, USA; GrammaTech, USA; Google, USA)
Article: popl16main-mainpopl16-254-p (type: Full Paper (12 pages + refs)) doi:

Casper: An Efficient Approach to Call Trace Collection
Rongxin Wu, Xiao Xiao, Shing-Chi Cheung, Hongyu Zhang, and Charles Zhang
(Hong Kong University of Science and Technology, China; Microsoft Research, China)
Article: popl16main-mainpopl16-38-p (type: Full Paper (12 pages + refs)) doi:

Pushdown Control-Flow Analysis for Free
Thomas Gilray, Steven Lyde, Michael D. Adams, Matthew Might, and David Van Horn
(University of Utah, USA; University of Maryland, USA)
Article: popl16main-mainpopl16-87-p (type: Full Paper (12 pages + refs)) doi:

Binding as Sets of Scopes
Matthew Flatt
(University of Utah, USA)
Article: popl16main-mainpopl16-50-p (type: Full Paper (12 pages + refs)) doi:

Foundations of Model Checking

Lattice-Theoretic Progress Measures and Coalgebraic Model Checking
Ichiro Hasuo, Shunsuke Shimizu, and Corina Cîrstea
(University of Tokyo, Japan; University of Southampton, UK)
Article: popl16main-mainpopl16-337-p (type: Full Paper (12 pages + refs)) doi:

Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components
Krishnendu Chatterjee, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis
(IST Austria, Austria)
Article: popl16main-mainpopl16-60-p (type: Full Paper (12 pages + refs)) doi:

Memoryful Geometry of Interaction II: Recursion and Adequacy
Koko Muroya, Naohiko Hoshino, and Ichiro Hasuo
(University of Tokyo, Japan; Kyoto University, Japan)
Article: popl16main-mainpopl16-335-p (type: Full Paper (12 pages + refs)) doi:

Synthesis

Learning Programs from Noisy Data
Veselin Raychev, Pavol Bielik, Martin Vechev, and Andreas Krause
(ETH Zurich, Switzerland)
Article: popl16main-mainpopl16-332-p (type: Full Paper (12 pages + refs)) doi:

Optimizing Synthesis with Metasketches
James Bornholt, Emina Torlak, Dan Grossman, and Luis Ceze
(University of Washington, USA)
Article: popl16main-mainpopl16-299-p (type: Full Paper (12 pages + refs)) doi:

Maximal Specification Synthesis
Aws Albarghouthi, Isil Dillig, and Arie Gurfinkel
(University of Wisconsin-Madison, USA; University of Texas at Austin, USA; Carnegie Mellon University, USA)
Article: popl16main-mainpopl16-72-p (type: Full Paper (12 pages + refs)) doi:

Example-Directed Synthesis: A Type-Theoretic Interpretation
Jonathan Frankle, Peter-Michael Osera, David Walker, and Steve Zdancewic
(Princeton University, USA; Grinnell College, USA; University of Pennsylvania, USA)
Article: popl16main-mainpopl16-80-p (type: Full Paper (12 pages + refs)) doi: