POPL 2017
44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017)
Powered by
Conference Publishing Consulting

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

POPL 2017 – Proceedings

Contents - Abstracts - Authors

Frontmatter

Title Page
POPL 2017 General and Program Chairs' Message
POPL 2017 AEC Chairs' Report
POPL 2017 Organization
Sponsors and Supporters

Keynotes

The Influence of Dependent Types (Keynote)
Stephanie Weirich
(University of Pennsylvania, USA)
Publisher's Version Article Search
Rust: From POPL to Practice (Keynote)
Aaron Turon
(Mozilla, USA)
Publisher's Version Article Search

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)
Publisher's Version Article Search Info
A Posteriori Environment Analysis with Pushdown Delta CFA
Kimball Germane and Matthew Might
(University of Utah, USA)
Publisher's Version Article Search
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)
Publisher's Version Article Search
Fast Polyhedra Abstract Domain
Gagandeep Singh, Markus Püschel, and Martin Vechev
(ETH Zurich, Switzerland)
Publisher's Version Article Search Video Info

Type Systems 1

Polymorphism, Subtyping, and Type Inference in MLsub
Stephen Dolan and Alan Mycroft
(University of Cambridge, UK)
Publisher's Version Article Search Info
Java Generics Are Turing Complete
Radu Grigore
(University of Kent, UK)
Publisher's Version Article Search Info
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)
Publisher's Version Article Search Info
Modules, Abstraction, and Parametric Polymorphism
Karl Crary
(Carnegie Mellon University, USA)
Publisher's Version Article Search

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)
Publisher's Version Article Search
Exact Bayesian Inference by Symbolic Disintegration
Chung-chieh Shan and Norman Ramsey
(Indiana University, USA; Tufts University, USA)
Publisher's Version Article Search Video
Stochastic Invariants for Probabilistic Termination
Krishnendu Chatterjee, Petr Novotný, and Ðorđe Žikelić
(IST Austria, Austria; University of Cambridge, UK)
Publisher's Version Article Search
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)
Publisher's Version Article Search

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)
Publisher's Version Article Search Info
Automatically Comparing Memory Consistency Models
John Wickerson, Mark Batty, Tyler Sorensen, and George A. Constantinides
(Imperial College London, UK; University of Kent, UK)
Publisher's Version Article Search Info
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)
Publisher's Version Article Search
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)
Publisher's Version Article Search Info

Logic

Monadic Second-Order Logic on Finite Sequences
Loris D'Antoni and Margus Veanes
(University of Wisconsin-Madison, USA; Microsoft Research, USA)
Publisher's Version Article Search
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)
Publisher's Version Article Search
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)
Publisher's Version Article Search

Compiler Optimisation

A Program Optimization for Automatic Database Result Caching
Ziv Scully and Adam Chlipala
(Carnegie Mellon University, USA; Massachusetts Institute of Technology, USA)
Publisher's Version Article Search
Stream Fusion, to Completeness
Oleg Kiselyov, Aggelos Biboudis, Nick Palladinos, and Yannis Smaragdakis
(Tohoku University, Japan; University of Athens, Greece; Nessos IT, Greece)
Publisher's Version Article Search Info
Rigorous Floating-Point Mixed-Precision Tuning
Wei-Fan Chiang, Mark Baranowski, Ian Briggs, Alexey Solovyev, Ganesh Gopalakrishnan, and Zvonimir Rakamarić
(University of Utah, USA)
Publisher's Version Article Search

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)
Publisher's Version Article Search
Contract-Based Resource Verification for Higher-Order Functions with Memoization
Ravichandhran Madhavan, Sumith Kulal, and Viktor Kuncak
(EPFL, Switzerland; IIT Bombay, India)
Publisher's Version Article Search
Context-Sensitive Data-Dependence Analysis via Linear Conjunctive Language Reachability
Qirun Zhang and Zhendong Su
(University of California at Davis, USA)
Publisher's Version Article Search
Towards Automatic Resource Bound Analysis for OCaml
Jan Hoffmann, Ankush Das, and Shu-Chun Weng
(Carnegie Mellon University, USA; Yale University, USA)
Publisher's Version Article Search Info

Type Systems 2

Deciding Equivalence with Sums and the Empty Type
Gabriel Scherer
(Northeastern University, USA)
Publisher's Version Article Search
The exp-log Normal Form of Types: Decomposing Extensional Equality and Representing Terms Compactly
Danko Ilik
(Trusted Labs, France)
Publisher's Version Article Search Info
Contextual Isomorphisms
Paul Blain Levy
(University of Birmingham, UK)
Publisher's Version Article Search
Typed Self-Evaluation via Intensional Type Functions
Matt Brown and Jens Palsberg
(University of California at Los Angeles, USA)
Publisher's Version Article Search

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)
Publisher's Version Article Search Info
Dynamic Race Detection for C++11
Christopher Lidbury and Alastair F. Donaldson
(Imperial College London, UK)
Publisher's Version Article Search
Serializability for Eventual Consistency: Criterion, Analysis, and Applications
Lucas Brutschy, Dimitar Dimitrov, Peter Müller, and Martin Vechev
(ETH Zurich, Switzerland)
Publisher's Version Article Search
Thread Modularity at Many Levels: A Pearl in Compositional Verification
Jochen Hoenicke, Rupak Majumdar, and Andreas Podelski
(University of Freiburg, Germany; MPI-SWS, Germany)
Publisher's Version Article Search

Functional Programming with Effects

Type Directed Compilation of Row-Typed Algebraic Effects
Daan Leijen
(Microsoft Research, USA)
Publisher's Version Article Search Info
Do Be Do Be Do
Sam Lindley, Conor McBride, and Craig McLaughlin
(University of Edinburgh, UK; University of Strathclyde, UK)
Publisher's Version Article Search
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)
Publisher's Version Article Search
Stateful Manifest Contracts
Taro Sekiyama and Atsushi Igarashi
(IBM Research, Japan; Kyoto University, Japan)
Publisher's Version Article Search

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

Logic and Programming

Genesis: Synthesizing Forwarding Tables in Multi-tenant Networks
Kausik Subramanian, Loris D'Antoni, and Aditya Akella
(University of Wisconsin-Madison, USA)
Publisher's Version Article Search
LOIS: Syntax and Semantics
Eryk Kopczyński and Szymon Toruńczyk
(University of Warsaw, Poland)
Publisher's Version Article Search Info

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)
Publisher's Version Article Search
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)
Publisher's Version Article Search
On Verifying Causal Consistency
Ahmed Bouajjani, Constantin Enea, Rachid Guerraoui, and Jad Hamza
(University of Paris Diderot, France; EPFL, Switzerland; Inria, France)
Publisher's Version Article Search
Complexity Verification using Guided Theorem Enumeration
Akhilesh Srikanth, Burak Sahin, and William R. Harris
(Georgia Institute of Technology, USA)
Publisher's Version Article Search

Type Systems 3

Intersection Type Calculi of Bounded Dimension
Andrej Dudenhefner and Jakob Rehof
(TU Dortmund, Germany)
Publisher's Version Article Search
Type Soundness Proofs with Definitional Interpreters
Nada Amin and Tiark Rompf
(EPFL, Switzerland; Purdue University, USA)
Publisher's Version Article Search
Computational Higher-Dimensional Type Theory
Carlo Angiuli, Robert Harper, and Todd Wilson
(Carnegie Mellon University, USA; California State University at Fresno, USA)
Publisher's Version Article Search
Type Systems as Macros
Stephen Chang, Alex Knauth, and Ben Greenman
(Northeastern University, USA)
Publisher's Version Article Search

Concurrency 3

Parallel Functional Arrays
Ananya Kumar, Guy E. Blelloch, and Robert Harper
(Carnegie Mellon University, USA)
Publisher's Version Article Search
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)
Publisher's Version Article Search Info
Analyzing Divergence in Bisimulation Semantics
Xinxin Liu, Tingting Yu, and Wenhui Zhang
(Institute of Software at Chinese Academy of Sciences, China)
Publisher's Version Article Search
Fencing off Go: Liveness and Safety for Channel-Based Programming
Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida
(Imperial College London, UK)
Publisher's Version Article Search

Gradual Typing and Contracts

Big Types in Little Runtime: Open-World Soundness and Collaborative Blame for Gradual Type Systems
Michael M. Vitousek, Cameron Swords, and Jeremy G. Siek
(Indiana University, USA)
Publisher's Version Article Search Info
Gradual Refinement Types
Nico Lehmann and Éric Tanter
(University of Chile, Chile)
Publisher's Version Article Search
Automatically Generating the Dynamic Semantics of Gradually Typed Languages
Matteo Cimini and Jeremy G. Siek
(Indiana University, USA)
Publisher's Version Article Search
Sums of Uncertainty: Refinements Go Gradual
Khurram A. Jafery and Joshua Dunfield
(University of British Columbia, Canada)
Publisher's Version Article Search

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)
Publisher's Version Article Search
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)
Publisher's Version Article Search
QWIRE: A Core Language for Quantum Circuits
Jennifer Paykin, Robert Rand, and Steve Zdancewic
(University of Pennsylvania, USA)
Publisher's Version Article Search

Security and Privacy

LMS-Verify: Abstraction without Regret for Verified Systems Programming
Nada Amin and Tiark Rompf
(EPFL, Switzerland; Purdue University, USA)
Publisher's Version Article Search
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)
Publisher's Version Article Search
LightDP: Towards Automating Differential Privacy Proofs
Danfeng Zhang and Daniel Kifer
(Pennsylvania State University, USA)
Publisher's Version Article Search

proc time: 0.24