POPL 2017 – Proceedings

44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017), January 15–21, 2017, Paris, France

Frontmatter

Keynotes

The Influence of Dependent Types (Keynote)
Stephanie Weirich
(University of Pennsylvania, USA)
Article: popl17key-key1-p doi:

Rust: From POPL to Practice (Keynote)
Aaron Turon
(Mozilla, USA)
Article: popl17key-key2-p doi:

Abstract Interpretation

Ogre and Pythia: An Invariance Proof Method for Weak Consistency Models
Jade Alglave and Patrick Cousot
(Microsoft Research, UK; University College London, UK; New York University, USA; ENS, France)
Article: popl17main-main232-p doi:

A Posteriori Environment Analysis with Pushdown Delta CFA
Kimball Germane and Matthew Might
(University of Utah, USA)
Article: popl17main-main312-p doi:

Semantic-Directed Clumping of Disjunctive Abstract States
Huisong Li, Francois Berenger, Bor-Yuh Evan Chang, and Xavier Rival
(Inria, France; CNRS, France; ENS, France; University of Colorado at Boulder, USA)
Article: popl17main-main220-p doi:

Fast Polyhedra Abstract Domain
Gagandeep Singh, Markus Püschel, and Martin Vechev
(ETH Zurich, Switzerland)
Article: popl17main-main238-p doi:

Type Systems 1

Polymorphism, Subtyping, and Type Inference in MLsub
Stephen Dolan and Alan Mycroft
(University of Cambridge, UK)
Article: popl17main-main228-p doi:

Java Generics Are Turing Complete
Radu Grigore
(University of Kent, UK)
Article: popl17main-main163-p doi:

Hazelnut: A Bidirectionally Typed Structure Editor Calculus
Cyrus Omar, Ian Voysey, Michael Hilton, Jonathan Aldrich, and Matthew A. Hammer
(Carnegie Mellon University, USA; Oregon State University, USA; University of Colorado at Boulder, USA)
Article: popl17main-main319-p doi:

Modules, Abstraction, and Parametric Polymorphism
Karl Crary
(Carnegie Mellon University, USA)
Article: popl17main-main264-p doi:

Probabilistic Programming

Beginner's Luck: A Language for Property-Based Generators
Leonidas Lampropoulos, Diane Gallois-Wong, Cătălin Hriţcu, John Hughes, Benjamin C. Pierce, and Li-yao Xia
(University of Pennsylvania, USA; Inria, France; ENS, France; Chalmers University of Technology, Sweden)
Article: popl17main-main152-p doi:

Exact Bayesian Inference by Symbolic Disintegration
Chung-chieh Shan and Norman Ramsey
(Indiana University, USA; Tufts University, USA)
Article: popl17main-main95-p doi:

Stochastic Invariants for Probabilistic Termination
Krishnendu Chatterjee, Petr Novotný, and Ðorđe Žikelić
(IST Austria, Austria; University of Cambridge, UK)
Article: popl17main-main182-p doi:

Coupling Proofs Are Probabilistic Product Programs
Gilles Barthe, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub
(IMDEA Software Institute, Spain; Inria, France; University of Pennsylvania, USA; École Polytechnique, France)
Article: popl17main-main290-p doi:

Concurrency 1

A Promising Semantics for Relaxed-Memory Concurrency
Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, and Derek Dreyer
(Seoul National University, South Korea; MPI-SWS, Germany)
Article: popl17main-main65-p doi:

Automatically Comparing Memory Consistency Models
John Wickerson, Mark Batty, Tyler Sorensen, and George A. Constantinides
(Imperial College London, UK; University of Kent, UK)
Article: popl17main-main2-p doi:

Interactive Proofs in Higher-Order Concurrent Separation Logic
Robbert Krebbers, Amin Timany, and Lars Birkedal
(Delft University of Technology, Netherlands; KU Leuven, Belgium; Aarhus University, Denmark)
Article: popl17main-main99-p doi:

A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic
Morten Krogh-Jespersen, Kasper Svendsen, and Lars Birkedal
(Aarhus University, Denmark; University of Cambridge, UK)
Article: popl17main-main192-p doi:

Logic

Monadic Second-Order Logic on Finite Sequences
Loris D'Antoni and Margus Veanes
(University of Wisconsin-Madison, USA; Microsoft Research, USA)
Article: popl17main-main32-p doi:

On the Relationship between Higher-Order Recursion Schemes and Higher-Order Fixpoint Logic
Naoki Kobayashi, Étienne Lozes, and Florian Bruse
(University of Tokyo, Japan; ENS, France; CNRS, France; University of Kassel, Germany)
Article: popl17main-main97-p doi:

Coming to Terms with Quantified Reasoning
Laura Kovács, Simon Robillard, and Andrei Voronkov
(Vienna University of Technology, Austria; Chalmers University of Technology, Sweden; University of Manchester, UK)
Article: popl17main-main253-p doi:

Compiler Optimisation

A Program Optimization for Automatic Database Result Caching
Ziv Scully and Adam Chlipala
(Carnegie Mellon University, USA; Massachusetts Institute of Technology, USA)
Article: popl17main-main260-p doi:

Stream Fusion, to Completeness
Oleg Kiselyov, Aggelos Biboudis, Nick Palladinos, and Yannis Smaragdakis
(Tohoku University, Japan; University of Athens, Greece; Nessos IT, Greece)
Article: popl17main-main218-p doi:

Rigorous Floating-Point Mixed-Precision Tuning
Wei-Fan Chiang, Mark Baranowski, Ian Briggs, Alexey Solovyev, Ganesh Gopalakrishnan, and Zvonimir Rakamarić
(University of Utah, USA)
Article: popl17main-main41-p doi:

Program Analysis

Relational Cost Analysis
Ezgi Çiçek, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Jan Hoffmann
(MPI-SWS, Germany; IMDEA Software Institute, Spain; SUNY Buffalo, USA; Carnegie Mellon University, USA)
Article: popl17main-main107-p doi:

Contract-Based Resource Verification for Higher-Order Functions with Memoization
Ravichandhran Madhavan, Sumith Kulal, and Viktor Kuncak
(EPFL, Switzerland; IIT Bombay, India)
Article: popl17main-main184-p doi:

Towards Automatic Resource Bound Analysis for OCaml
Jan Hoffmann, Ankush Das, and Shu-Chun Weng
(Carnegie Mellon University, USA; Yale University, USA)
Article: popl17main-main17-p doi:

Type Systems 2

Deciding Equivalence with Sums and the Empty Type
Gabriel Scherer
(Northeastern University, USA)
Article: popl17main-main355-p doi:

Contextual Isomorphisms
Paul Blain Levy
(University of Birmingham, UK)
Article: popl17main-main305-p doi:

Typed Self-Evaluation via Intensional Type Functions
Matt Brown and Jens Palsberg
(University of California at Los Angeles, USA)
Article: popl17main-main96-p doi:

Concurrency 2

Mixed-Size Concurrency: ARM, POWER, C/C++11, and SC
Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, and Peter Sewell
(University of Cambridge, UK; University of St. Andrews, UK; Inria, France; University of Kent, UK)
Article: popl17main-main4-p doi:

Dynamic Race Detection for C++11
Christopher Lidbury and Alastair F. Donaldson
(Imperial College London, UK)
Article: popl17main-main106-p doi:

Thread Modularity at Many Levels: A Pearl in Compositional Verification
Jochen Hoenicke, Rupak Majumdar, and Andreas Podelski
(University of Freiburg, Germany; MPI-SWS, Germany)
Article: popl17main-main273-p doi:

Functional Programming with Effects

Do Be Do Be Do
Sam Lindley, Conor McBride, and Craig McLaughlin
(University of Edinburgh, UK; University of Strathclyde, UK)
Article: popl17main-main302-p doi:

Dijkstra Monads for Free
Danel Ahman, Cătălin Hriţcu, Kenji Maillard, Guido Martínez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi, and Nikhil Swamy
(University of Edinburgh, UK; Microsoft Research, USA; Inria, France; ENS, France; Rosario National University, Argentina; Microsoft Research, India)
Article: popl17main-main206-p doi:

Stateful Manifest Contracts
Taro Sekiyama and Atsushi Igarashi
(IBM Research, Japan; Kyoto University, Japan)
Article: popl17main-main187-p doi:

Semantic Foundations

A Semantic Account of Metric Preservation
Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, and Ikram Cherigui
(University of Pennsylvania, USA; SUNY Buffalo, USA; Kyoto University, Japan; ENS, France)
Article: popl17main-main259-p doi:

Cantor Meets Scott: Semantic Foundations for Probabilistic Networks
Steffen Smolka, Praveen Kumar, Nate Foster, Dexter Kozen, and Alexandra Silva
(Cornell University, USA; University College London, UK)
Article: popl17main-main18-p doi:

Logic and Programming

Genesis: Synthesizing Forwarding Tables in Multi-tenant Networks
Kausik Subramanian, Loris D'Antoni, and Aditya Akella
(University of Wisconsin-Madison, USA)
Article: popl17main-main35-p doi:

LOIS: Syntax and Semantics
Eryk Kopczyński and Szymon Toruńczyk
(University of Warsaw, Poland)
Article: popl17main-main189-p doi:

Verification and Synthesis

Component-Based Synthesis for Complex APIs
Yu Feng, Ruben Martins, Yuepeng Wang, Isil Dillig, and Thomas W. Reps
(University of Texas at Austin, USA; University of Wisconsin-Madison, USA)
Article: popl17main-main93-p doi:

Learning Nominal Automata
Joshua Moerman, Matteo Sammartino, Alexandra Silva, Bartek Klin, and Michał Szynwelski
(Radboud University Nijmegen, Netherlands; University College London, UK; University of Warsaw, Poland)
Article: popl17main-main209-p doi:

On Verifying Causal Consistency
Ahmed Bouajjani, Constantin Enea, Rachid Guerraoui, and Jad Hamza
(University of Paris Diderot, France; EPFL, Switzerland; Inria, France)
Article: popl17main-main255-p doi:

Complexity Verification using Guided Theorem Enumeration
Akhilesh Srikanth, Burak Sahin, and William R. Harris
(Georgia Institute of Technology, USA)
Article: popl17main-main137-p doi:

Type Systems 3

Intersection Type Calculi of Bounded Dimension
Andrej Dudenhefner and Jakob Rehof
(TU Dortmund, Germany)
Article: popl17main-main130-p doi:

Type Soundness Proofs with Definitional Interpreters
Nada Amin and Tiark Rompf
(EPFL, Switzerland; Purdue University, USA)
Article: popl17main-main143-p doi:

Computational Higher-Dimensional Type Theory
Carlo Angiuli, Robert Harper, and Todd Wilson
(Carnegie Mellon University, USA; California State University at Fresno, USA)
Article: popl17main-main126-p doi:

Type Systems as Macros
Stephen Chang, Alex Knauth, and Ben Greenman
(Northeastern University, USA)
Article: popl17main-main247-p doi:

Concurrency 3

Parallel Functional Arrays
Ananya Kumar, Guy E. Blelloch, and Robert Harper
(Carnegie Mellon University, USA)
Article: popl17main-main157-p doi:

A Short Counterexample Property for Safety and Liveness Verification of Fault-Tolerant Distributed Algorithms
Igor Konnov, Marijana Lazić, Helmut Veith, and Josef Widder
(Vienna University of Technology, Austria)
Article: popl17main-main116-p doi:

Analyzing Divergence in Bisimulation Semantics
Xinxin Liu, Tingting Yu, and Wenhui Zhang
(Institute of Software at Chinese Academy of Sciences, China)
Article: popl17main-main158-p doi:

Fencing off Go: Liveness and Safety for Channel-Based Programming
Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida
(Imperial College London, UK)
Article: popl17main-main51-p doi:

Gradual Typing and Contracts

Gradual Refinement Types
Nico Lehmann and Éric Tanter
(University of Chile, Chile)
Article: popl17main-main102-p doi:

Sums of Uncertainty: Refinements Go Gradual
Khurram A. Jafery and Joshua Dunfield
(University of British Columbia, Canada)
Article: popl17main-main142-p doi:

Quantum

Invariants of Quantum Programs: Characterisations and Generation
Mingsheng Ying, Shenggang Ying, and Xiaodi Wu
(University of Technology Sydney, Australia; Tsinghua University, China; Institute of Software at Chinese Academy of Sciences, China; University of Oregon, USA)
Article: popl17main-main10-p doi:

The Geometry of Parallelism: Classical, Probabilistic, and Quantum Effects
Ugo Dal Lago, Claudia Faggian, Benoît Valiron, and Akira Yoshimizu
(University of Bologna, Italy; Inria, France; CNRS, France; University of Paris Diderot, France; University of Paris-Saclay, France; University of Tokyo, Japan)
Article: popl17main-main113-p doi:

QWIRE: A Core Language for Quantum Circuits
Jennifer Paykin, Robert Rand, and Steve Zdancewic
(University of Pennsylvania, USA)
Article: popl17main-main278-p doi:

Security and Privacy

LMS-Verify: Abstraction without Regret for Verified Systems Programming
Nada Amin and Tiark Rompf
(EPFL, Switzerland; Purdue University, USA)
Article: popl17main-main144-p doi:

Hypercollecting Semantics and Its Application to Static Analysis of Information Flow
Mounir Assaf, David A. Naumann, Julien Signoles, Éric Totel, and Frédéric Tronel
(Stevens Institute of Technology, USA; CEA LIST, France; CentraleSupélec, France)
Article: popl17main-main256-p doi:

LightDP: Towards Automating Differential Privacy Proofs
Danfeng Zhang and Daniel Kifer
(Pennsylvania State University, USA)
Article: popl17main-main234-p doi: