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

Frontmatter

Title Page
Messages from the Chairs
Committees
Sponsors

Keynotes

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

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)
Publisher's Version Article Search
Type Theory in Type Theory using Quotient Inductive Types
Thorsten Altenkirch and Ambrus Kaposi
(University of Nottingham, UK)
Publisher's Version Article Search Info
System F-omega with Equirecursive Types for Datatype-Generic Programming
Yufei Cai, Paolo G. Giarrusso, and Klaus Ostermann
(University of Tübingen, Germany)
Publisher's Version Article Search Info
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)
Publisher's Version Article Search

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)
Publisher's Version Article Search
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)
Publisher's Version Article Search
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)
Publisher's Version Article Search
Reducing Crash Recoverability to Reachability
Eric Koskinen and Junfeng Yang
(Yale University, USA; Columbia University, USA)
Publisher's Version Article Search

Decision Procedures

Query-Guided Maximum Satisfiability
Xin Zhang, Ravi Mangal, Aditya V. Nori, and Mayur Naik
(Georgia Institute of Technology, USA; Microsoft Research, UK)
Publisher's Version Article Search
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)
Publisher's Version Article Search
Symbolic Computation of Differential Equivalences
Luca Cardelli, Mirco Tribastone, Max Tschaikowski, and Andrea Vandin
(Microsoft Research, UK; University of Oxford, UK; IMT Lucca, Italy)
Publisher's Version Article Search
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)
Publisher's Version Article Search Info

Correct Compilation

Fully-Abstract Compilation by Approximate Back-Translation
Dominique Devriese, Marco Patrignani, and Frank Piessens
(KU Leuven, Belgium)
Publisher's Version Article Search
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)
Publisher's Version Article Search Info
From MinX to MinC: Semantics-Driven Decompilation of Recursive Datatypes
Ed Robbins, Andy King, and Tom Schrijvers
(University of Kent, UK; KU Leuven, Belgium)
Publisher's Version Article Search
Sound Type-Dependent Syntactic Language Extension
Florian Lorenzen and Sebastian Erdweg
(TU Berlin, Germany; TU Darmstadt, Germany)
Publisher's Version Article Search

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)
Publisher's Version Article Search
The Hardness of Data Packing
Rahman Lavaee
(University of Rochester, USA)
Publisher's Version Article Search
The Complexity of Interaction
Stéphane Gimenez and Georg Moser
(University of Innsbruck, Austria)
Publisher's Version Article Search

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)
Publisher's Version Article Search Info
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)
Publisher's Version Article Search
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)
Publisher's Version Article Search

Probabilistic and Statistical Analysis

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

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)
Publisher's Version Article Search
'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)
Publisher's Version Article Search
A Program Logic for Concurrent Objects under Fair Scheduling
Hongjin Liang and Xinyu Feng
(University of Science and Technology of China, China)
Publisher's Version Article Search
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)
Publisher's Version Article Search

Types, Generally or Gradually

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

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)
Publisher's Version Article Search
Abstraction Refinement Guided by a Learnt Probabilistic Model
Radu Grigore and Hongseok Yang
(University of Oxford, UK)
Publisher's Version Article Search Info
Learning Invariants using Decision Trees and Implication Counterexamples
Pranav Garg, Daniel Neider, P. Madhusudan, and Dan Roth
(University of Illinois at Urbana-Champaign, USA)
Publisher's Version Article Search
Symbolic Abstract Data Type Inference
Michael Emmi and Constantin Enea
(IMDEA Software Institute, Spain; University of Paris Diderot, France)
Publisher's Version Article Search

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)
Publisher's Version Article Search
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)
Publisher's Version Article Search
Printing Floating-Point Numbers: A Faster, Always Correct Method
Marc Andrysco, Ranjit Jhala, and Sorin Lerner
(University of California at San Diego, USA)
Publisher's Version Article Search

Sessions and Processes

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

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)
Publisher's Version Article Search Info
A Concurrency Semantics for Relaxed Atomics that Permits Optimisation and Avoids Thin-Air Executions
Jean Pichon-Pharabod and Peter Sewell
(University of Cambridge, UK)
Publisher's Version Article Search Info
Overhauling SC Atomics in C11 and OpenCL
Mark Batty, Alastair F. Donaldson, and John Wickerson
(University of Kent, UK; Imperial College London, UK)
Publisher's Version Article Search
Taming Release-Acquire Consistency
Ori Lahav, Nick Giannarakis, and Viktor Vafeiadis
(MPI-SWS, Germany)
Publisher's Version Article Search Info

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)
Publisher's Version Article Search
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)
Publisher's Version Article Search
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)
Publisher's Version Article Search
Binding as Sets of Scopes
Matthew Flatt
(University of Utah, USA)
Publisher's Version Article Search Info

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

Synthesis

Learning Programs from Noisy Data
Veselin Raychev, Pavol Bielik, Martin Vechev, and Andreas Krause
(ETH Zurich, Switzerland)
Publisher's Version Article Search
Optimizing Synthesis with Metasketches
James Bornholt, Emina Torlak, Dan Grossman, and Luis Ceze
(University of Washington, USA)
Publisher's Version Article Search
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)
Publisher's Version Article Search
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)
Publisher's Version Article Search

proc time: 0.31