POPL 2016
43rd ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2016)
Powered by
Conference Publishing Consulting

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

POPL 2016 – Proceedings

Contents - Abstracts - Authors


Title Page
Messages from the Chairs


Programming the World of Uncertain Things (Keynote)
Kathryn S. McKinley
(Microsoft Research, USA)
Synthesis of Reactive Controllers for Hybrid Systems (Keynote)
Richard M. Murray
(California Institute of Technology, USA)
Confluences in Programming Languages Research (Keynote)
David Walker
(Princeton University, USA)

Research Papers

Types and Foundations

Breaking through the Normalization Barrier: A Self-Interpreter for F-omega
Matt Brown and Jens PalsbergORCID logo
(University of California at Los Angeles, USA)
Type Theory in Type Theory using Quotient Inductive Types
Thorsten Altenkirch and Ambrus Kaposi
(University of Nottingham, UK)
System F-omega with Equirecursive Types for Datatype-Generic Programming
Yufei Cai, Paolo G. Giarrusso, and Klaus Ostermann ORCID logo
(University of Tübingen, Germany)
A Theory of Effects and Resources: Adjunction Models and Polarised Calculi
Pierre-Louis Curien, Marcelo Fiore ORCID logo, and Guillaume Munch-Maccagnoni
(University of Paris Diderot, France; Inria, France; University of Cambridge, UK)

Algorithmic Verification

Temporal Verification of Higher-Order Functional Programs
Akihiro Murase, Tachio Terauchi, Naoki KobayashiORCID logo, Ryosuke Sato, and Hiroshi UnnoORCID logo
(Nagoya University, Japan; JAIST, Japan; University of Tokyo, Japan; University of Tsukuba, Japan)
Scaling Network Verification using Symmetry and Surgery
Gordon D. Plotkin, Nikolaj Bjørner ORCID logo, Nuno P. Lopes, Andrey Rybalchenko, and George Varghese
(University of Edinburgh, UK; Microsoft Research, USA; Microsoft Research, UK)
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)
Reducing Crash Recoverability to Reachability
Eric Koskinen and Junfeng Yang
(Yale University, USA; Columbia University, USA)

Decision Procedures

Query-Guided Maximum Satisfiability
Xin Zhang, Ravi Mangal, Aditya V. Nori, and Mayur Naik
(Georgia Institute of Technology, USA; Microsoft Research, UK)
String Solving with Word Equations and Transducers: Towards a Logic for Analysing Mutation XSS
Anthony W. Lin ORCID logo and Pablo Barceló
(Yale-NUS College, Singapore; University of Chile, Chile)
Symbolic Computation of Differential Equivalences
Luca Cardelli, Mirco TribastoneORCID logo, Max Tschaikowski, and Andrea Vandin
(Microsoft Research, UK; University of Oxford, UK; IMT Lucca, Italy)
Unboundedness and Downward Closures of Higher-Order Pushdown Automata
Matthew Hague ORCID logo, Jonathan Kochems, and C.-H. Luke Ong ORCID logo
(University of London, UK; University of Oxford, UK)

Correct Compilation

Fully-Abstract Compilation by Approximate Back-Translation
Dominique Devriese, Marco Patrignani, and Frank Piessens
(KU Leuven, Belgium)
Lightweight Verification of Separate Compilation
Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur ORCID logo, Derek DreyerORCID logo, and Viktor VafeiadisORCID logo
(Seoul National University, South Korea; MPI-SWS, Germany)
From MinX to MinC: Semantics-Driven Decompilation of Recursive Datatypes
Ed Robbins, Andy King, and Tom Schrijvers ORCID logo
(University of Kent, UK; KU Leuven, Belgium)
Sound Type-Dependent Syntactic Language Extension
Florian Lorenzen and Sebastian Erdweg
(TU Berlin, Germany; TU Darmstadt, Germany)

Decidability and Complexity

Decidability of Inferring Inductive Invariants
Oded Padon, Neil Immerman, Sharon Shoham ORCID logo, Aleksandr Karbyshev, and Mooly Sagiv ORCID logo
(Tel Aviv University, Israel; University of Massachusetts at Amherst, USA; Academic College of Tel Aviv Yaffo, Israel)
The Hardness of Data Packing
Rahman Lavaee
(University of Rochester, USA)
The Complexity of Interaction
Stéphane Gimenez and Georg Moser ORCID logo
(University of Innsbruck, Austria)

Language Design

Dependent Types and Multi-monadic Effects in F*
Nikhil Swamy ORCID logo, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet ORCID logo, Pierre-Yves Strub ORCID logo, 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)
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)
Kleenex: Compiling Nondeterministic Transducers to Deterministic Streaming Transducers
Bjørn Bugge Grathwohl, Fritz Henglein ORCID logo, Ulrik Terp Rasmussen, Kristoffer Aalund Søholm, and Sebastian Paaske Tørholm
(University of Copenhagen, Denmark; Jobindex, Denmark)

Probabilistic and Statistical Analysis

Automatic Patch Generation by Learning Correct Code
Fan Long and Martin RinardORCID logo
(Massachusetts Institute of Technology, USA)
Estimating Types in Binaries using Predictive Modeling
Omer Katz, Ran El-Yaniv, and Eran Yahav
(Technion, Israel)
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)
Transforming Spreadsheet Data Types using Examples
Rishabh Singh and Sumit GulwaniORCID logo
(Microsoft Research, USA)

Foundations of Distributed Systems

Chapar: Certified Causally Consistent Distributed Key-Value Stores
Mohsen Lesani, Christian J. Bell, and Adam ChlipalaORCID logo
(Massachusetts Institute of Technology, USA)
'Cause I'm Strong Enough: Reasoning about Consistency Choices in Distributed Systems
Alexey Gotsman, Hongseok YangORCID logo, Carla Ferreira ORCID logo, Mahsa Najafzadeh, and Marc Shapiro
(IMDEA Software Institute, Spain; University of Oxford, UK; Universidade Nova Lisboa, Potugal; Sorbonne, France; Inria, France; UPMC, France)
A Program Logic for Concurrent Objects under Fair Scheduling
Hongjin Liang and Xinyu Feng
(University of Science and Technology of China, China)
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)

Types, Generally or Gradually

Principal Type Inference for GADTs
Sheng Chen and Martin Erwig
(University of Louisiana at Lafayette, USA; Oregon State University, USA)
Abstracting Gradual Typing
Ronald GarciaORCID logo, Alison M. Clark, and Éric TanterORCID logo
(University of British Columbia, Canada; University of Chile, Chile)
The Gradualizer: A Methodology and Algorithm for Generating Gradual Type Systems
Matteo Cimini and Jeremy G. Siek ORCID logo
(Indiana University, USA)
Is Sound Gradual Typing Dead?
Asumu Takikawa, Daniel Feltey, Ben Greenman, Max S. New, Jan Vitek ORCID logo, and Matthias Felleisen ORCID logo
(Northeastern University, USA)

Learning and Verification

Combining Static Analysis with Probabilistic Models to Enable Market-Scale Android Inter-component Analysis
Damien Octeau, Somesh Jha ORCID logo, Matthew Dering, Patrick McDaniel, Alexandre Bartel, Li Li, Jacques KleinORCID logo, and Yves Le Traon
(University of Wisconsin, USA; Pennsylvania State University, USA; IMDEA Software Institute, Spain; TU Darmstadt, Germany; University of Luxembourg, Luxembourg)
Abstraction Refinement Guided by a Learnt Probabilistic Model
Radu Grigore and Hongseok YangORCID logo
(University of Oxford, UK)
Learning Invariants using Decision Trees and Implication Counterexamples
Pranav Garg, Daniel Neider, P. MadhusudanORCID logo, and Dan Roth
(University of Illinois at Urbana-Champaign, USA)
Symbolic Abstract Data Type Inference
Michael Emmi and Constantin Enea
(IMDEA Software Institute, Spain; University of Paris Diderot, France)


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)
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)
Printing Floating-Point Numbers: A Faster, Always Correct Method
Marc Andrysco, Ranjit Jhala ORCID logo, and Sorin LernerORCID logo
(University of California at San Diego, USA)

Sessions and Processes

Effects as Sessions, Sessions as Effects
Dominic Orchard and Nobuko Yoshida ORCID logo
(Imperial College London, UK)
Monitors and Blame Assignment for Higher-Order Session Types
Limin Jia ORCID logo, Hannah Gommerstadt, and Frank Pfenning ORCID logo
(Carnegie Mellon University, USA)
Environmental Bisimulations for Probabilistic Higher-Order Languages
Davide Sangiorgi and Valeria Vignudelli
(University of Bologna, Italy; Inria, France)

Semantics and Memory Models

Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA
Shaked Flur, Kathryn E. Gray, Christopher PulteORCID logo, Susmit Sarkar, Ali Sezgin, Luc Maranget ORCID logo, Will Deacon, and Peter Sewell ORCID logo
(University of Cambridge, UK; University of St. Andrews, UK; Inria, France; ARM, UK)
A Concurrency Semantics for Relaxed Atomics that Permits Optimisation and Avoids Thin-Air Executions
Jean Pichon-Pharabod and Peter Sewell ORCID logo
(University of Cambridge, UK)
Overhauling SC Atomics in C11 and OpenCL
Mark Batty ORCID logo, Alastair F. DonaldsonORCID logo, and John Wickerson ORCID logo
(University of Kent, UK; Imperial College London, UK)
Taming Release-Acquire Consistency
Ori Lahav, Nick Giannarakis, and Viktor VafeiadisORCID logo
(MPI-SWS, Germany)

Program Design and Analysis

Newtonian Program Analysis via Tensor Product
Thomas RepsORCID logo, Emma Turetsky, and Prathmesh Prabhu
(University of Wisconsin-Madison, USA; GrammaTech, USA; Google, USA)
Casper: An Efficient Approach to Call Trace Collection
Rongxin Wu, Xiao Xiao, Shing-Chi CheungORCID logo, Hongyu Zhang, and Charles ZhangORCID logo
(Hong Kong University of Science and Technology, China; Microsoft Research, China)
Pushdown Control-Flow Analysis for Free
Thomas Gilray, Steven Lyde, Michael D. Adams, Matthew Might, and David Van HornORCID logo
(University of Utah, USA; University of Maryland, USA)
Binding as Sets of Scopes
Matthew Flatt ORCID logo
(University of Utah, USA)

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)
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)
Memoryful Geometry of Interaction II: Recursion and Adequacy
Koko Muroya, Naohiko Hoshino, and Ichiro Hasuo
(University of Tokyo, Japan; Kyoto University, Japan)


Learning Programs from Noisy Data
Veselin Raychev, Pavol Bielik, Martin VechevORCID logo, and Andreas Krause
(ETH Zurich, Switzerland)
Optimizing Synthesis with Metasketches
James Bornholt, Emina Torlak ORCID logo, Dan Grossman, and Luis Ceze ORCID logo
(University of Washington, USA)
Maximal Specification Synthesis
Aws Albarghouthi ORCID logo, Isil Dillig ORCID logo, and Arie Gurfinkel
(University of Wisconsin-Madison, USA; University of Texas at Austin, USA; Carnegie Mellon University, USA)
Example-Directed Synthesis: A Type-Theoretic Interpretation
Jonathan Frankle, Peter-Michael Osera, David Walker ORCID logo, and Steve ZdancewicORCID logo
(Princeton University, USA; Grinnell College, USA; University of Pennsylvania, USA)

proc time: 0.92