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 doi:

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

Confluences in Programming Languages Research (Keynote)
David Walker
(Princeton University, USA)
Article: popl16key-key3-p 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 doi:

Type Theory in Type Theory using Quotient Inductive Types
Thorsten Altenkirch and Ambrus Kaposi
(University of Nottingham, UK)
Article: popl16main-mainpopl16-157-p 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 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 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 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 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 doi:

Reducing Crash Recoverability to Reachability
Eric Koskinen and Junfeng Yang
(Yale University, USA; Columbia University, USA)
Article: popl16main-mainpopl16-199-p 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 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 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 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 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 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 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 doi:

Sound Type-Dependent Syntactic Language Extension
Florian Lorenzen and Sebastian Erdweg
(TU Berlin, Germany; TU Darmstadt, Germany)
Article: popl16main-mainpopl16-180-p 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 doi:

The Hardness of Data Packing
Rahman Lavaee
(University of Rochester, USA)
Article: popl16main-mainpopl16-312-p doi:

The Complexity of Interaction
Stéphane Gimenez and Georg Moser
(University of Innsbruck, Austria)
Article: popl16main-mainpopl16-191-p 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 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 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 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 doi:

Estimating Types in Binaries using Predictive Modeling
Omer Katz, Ran El-Yaniv, and Eran Yahav
(Technion, Israel)
Article: popl16main-mainpopl16-342-p 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 doi:

Transforming Spreadsheet Data Types using Examples
Rishabh Singh and Sumit Gulwani
(Microsoft Research, USA)
Article: popl16main-mainpopl16-310-p 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 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 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 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 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 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 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 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 doi:

Abstraction Refinement Guided by a Learnt Probabilistic Model
Radu Grigore and Hongseok Yang
(University of Oxford, UK)
Article: popl16main-mainpopl16-269-p 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 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 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 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 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 doi:

Sessions and Processes

Effects as Sessions, Sessions as Effects
Dominic Orchard and Nobuko Yoshida
(Imperial College London, UK)
Article: popl16main-mainpopl16-123-p 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 doi:

Environmental Bisimulations for Probabilistic Higher-Order Languages
Davide Sangiorgi and Valeria Vignudelli
(University of Bologna, Italy; Inria, France)
Article: popl16main-mainpopl16-215-p 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 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 doi:

Taming Release-Acquire Consistency
Ori Lahav, Nick Giannarakis, and Viktor Vafeiadis
(MPI-SWS, Germany)
Article: popl16main-mainpopl16-173-p 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 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 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 doi:

Binding as Sets of Scopes
Matthew Flatt
(University of Utah, USA)
Article: popl16main-mainpopl16-50-p 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 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 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 doi:

Synthesis

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

Optimizing Synthesis with Metasketches
James Bornholt, Emina Torlak, Dan Grossman, and Luis Ceze
(University of Washington, USA)
Article: popl16main-mainpopl16-299-p 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 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 doi: