POPL 2020
Proceedings of the ACM on Programming Languages, Volume 4, Number POPL

Title Page

Editorial Message

Taylor Subsumes Scott, Berry, Kahn and Plotkin
Davide Barbarossa and Giulio Manzonetto
(University of Paris 13, France)


Publisher's Version

Deductive Verification with Ghost Monitors
Martin Clochard, Claude Marché, and Andrei Paskevich
(ETH Zurich, Switzerland; Inria, France; University of Paris-Saclay, France; LRI, France; University of Paris-Sud, France; CNRS, France)


Publisher's Version

Dependent Type Systems as Macros
Stephen Chang, Michael Ballantyne, Milo Turner, and William J. Bowman
(Northeastern University, USA; PLT Group, USA; University of British Columbia, Canada)


Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

The Next 700 Relational Program Logics
Kenji Maillard, Cătălin Hriţcu, Exequiel Rivas, and Antoine Van Muylder
(Inria, France; ENS, France; University of Paris, France)


Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Complexity and Information in Invariant Inference
Yotam M. Y. Feldman, Neil Immerman, Mooly Sagiv, and Sharon Shoham
(Tel Aviv University, Israel; University of Massachusetts, USA)


Publisher's Version

Actris: Session-Type Based Reasoning in Separation Logic
Jonas Kastberg Hinrichsen, Jesper Bengtson, and Robbert Krebbers
(IT University of Copenhagen, Denmark; Delft University of Technology, Netherlands)


Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Formal Verification of a Constant-Time Preserving C Compiler
Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, and Alix Trieu
(MPI for Security and Privacy, Germany; IMDEA Software Institute, Spain; University of Rennes, France; Inria, France; CNRS, France; IRISA, France; Aarhus University, Denmark)


Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq
Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, and Théo Winterhalter
(Inria, France; IRIF, France; CNRS, France; University of Paris Diderot, France; Saarland University, Germany)


Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Undecidability of D_<: and Its Decidable Fragments
Jason Z. S. Hu and Ondřej Lhoták
(McGill University, Canada; University of Waterloo, Canada)


Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Incorrectness Logic
Peter W. O'Hearn
(Facebook, UK; University College London, UK)


Publisher's Version

Persistency Semantics of the Intel-x86 Architecture
Azalea Raad, John Wickerson, Gil Neiger, and Viktor Vafeiadis
(MPI-SWS, Germany; Imperial College London, UK; Intel Labs, USA)


Publisher's Version

Program Synthesis by Type-Guided Abstraction Refinement
Zheng Guo, Michael James, David Justo, Jiaxiao Zhou, Ziteng Wang, Ranjit Jhala, and Nadia Polikarpova
(University of California at San Diego, USA)


Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Reductions for Safety Proofs
Azadeh Farzan and Anthony Vandikas
(University of Toronto, Canada)


Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Deterministic Parallel Fixpoint Computation
Sung Kook Kim, Arnaud J. Venet, and Aditya V. Thakur
(University of California at Davis, USA; Facebook, USA)


Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Recurrence Extraction for Functional Programs through Call-by-Push-Value
G. A. Kavvos, Edward Morehouse, Daniel R. Licata, and Norman Danner
(Wesleyan University, USA)


Publisher's Version

Towards Verified Stochastic Variational Inference for Probabilistic Programs
Wonyeol Lee, Hangyeol Yu, Xavier Rival, and Hongseok Yang
(KAIST, South Korea; Inria, France; ENS, France; CNRS, France; PSL University, France)


Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Fast, Sound, and Effectively Complete Dynamic Race Prediction
Andreas Pavlogiannis
(Aarhus University, Denmark)


Publisher's Version

Par Means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs
Federico Aschieri and Francesco A. Genco
(TU Vienna, Austria; University of Paris 1, France)


Publisher's Version

Trace Types and Denotational Semantics for Sound Programmable Inference in Probabilistic Languages
Alexander K. Lew, Marco F. Cusumano-Towner, Benjamin Sherman, Michael Carbin, and Vikash K. Mansinghka
(Massachusetts Institute of Technology, USA)


Publisher's Version

Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation
Mengqi Liu, Lionel Rieg, Zhong Shao, Ronghui Gu, David Costanzo, Jung-Eun Kim, and Man-Ki Yoon
(Yale University, USA; Grenoble Alps University, France; CNRS, France; Grenoble INP, France; VERIMAG, France; Columbia University, USA)


Publisher's Version Artifacts Functional

Relational Proofs for Quantum Programs
Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, and Li Zhou
(MPI for Security and Privacy, Germany; IMDEA Software Institute, Spain; University of Wisconsin-Madison, USA; University of Technology Sydney, Australia; Institute of Software at Chinese Academy of Sciences, China; Tsinghua University, China)


Publisher's Version

Seminaïve Evaluation for a Higher-Order Functional Language
Michael Arntzenius and Neel Krishnaswami
(University of Birmingham, UK; University of Cambridge, UK)


Publisher's Version Published Artifact Artifacts Available Artifacts Functional

CompCertM: CompCert with C-Assembly Linking and Lightweight Modular Verification
Youngju Song, Minki Cho, Dongjoo Kim, Yonghyun Kim, Jeehoon Kang, and Chung-Kil Hur
(Seoul National University, South Korea; KAIST, South Korea)


Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Liquidate Your Assets: Reasoning about Resource Usage in Liquid Haskell
Martin A. T. Handley, Niki Vazou, and Graham Hutton
(University of Nottingham, UK; IMDEA Software Institute, Spain)


Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time
Peixin Wang, Hongfei Fu, Krishnendu Chatterjee, Yuxin Deng, and Ming Xu
(Shanghai Jiao Tong University, China; IST Austria, Austria; East China Normal University, China; Pengcheng Laboratory, China)


Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Parameterized Verification under TSO is PSPACE-Complete
Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Rojin Rezvan
(Uppsala University, Sweden; Sharif University of Technology, Iran)


Publisher's Version

The Weak Call-by-Value λ-Calculus Is Reasonable for Both Time and Space
Yannick Forster, Fabian Kunze, and Marc Roth
(Saarland University, Germany; M2CI, Germany; University of Oxford, UK)


Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Abstract Extensionality: On the Properties of Incomplete Abstract Interpretations
Roberto Bruni, Roberto Giacobazzi, Roberta Gori, Isabel Garcia-Contreras, and Dusko Pavlovic
(University of Pisa, Italy; University of Verona, Italy; IMDEA Software Institute, Spain; Universidad Politécnica de Madrid, Spain; University of Hawaii, USA)


Publisher's Version

What Is Decidable about Gradual Types?
Zeina Migeed and Jens Palsberg
(University of California at Los Angeles, USA)


Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Decomposition Diversity with Symmetric Data and Codata
David Binder, Julian Jabs, Ingo Skupin, and Klaus Ostermann
(University of Tübingen, Germany)


Publisher's Version Artifacts Functional

Reduction Monads and Their Signatures
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, and Marco Maggesi
(University of Birmingham, UK; University of Côte d'Azur, France; IMT Atlantique, France; University of Florence, Italy)


Publisher's Version

The High-Level Benefits of Low-Level Sandboxing
Michael Sammler, Deepak Garg, Derek Dreyer, and Tadeusz Litak
(MPI-SWS, Germany; Friedrich-Alexander University Erlangen-Nürnberg, Germany)


Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Spy Game: Verifying a Local Generic Solver in Iris
Paulo Emílio de Vilhena, François Pottier, and Jacques-Henri Jourdan
(Inria, France; CNRS, France; LRI, France; University of Paris-Saclay, France)


Publisher's Version

RustBelt Meets Relaxed Memory
Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser, and Derek Dreyer
(MPI-SWS, Germany; LRI, France; CNRS, France; University of Paris-Saclay, France)


Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Deciding Memory Safety for Single-Pass Heap-Manipulating Programs
Umang Mathur, Adithya Murali, Paul Krogmeier, P. Madhusudan, and Mahesh Viswanathan
(University of Illinois at Urbana-Champaign, USA)


Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Optimal Approximate Sampling from Discrete Probability Distributions
Feras A. Saad, Cameron E. Freer, Martin C. Rinard, and Vikash K. Mansinghka
(Massachusetts Institute of Technology, USA)


Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Aiming Low Is Harder: Induction for Lower Bounds in Probabilistic Program Verification
Marcel Hark, Benjamin Lucien Kaminski, Jürgen Giesl, and Joost-Pieter Katoen
(RWTH Aachen University, Germany)


Publisher's Version

A Simple Differentiable Programming Language
Martín Abadi and Gordon D. Plotkin
(Google Research, USA)


Publisher's Version

PλωNK: Functional Probabilistic NetKAT
Alexander Vandenbroucke and Tom Schrijvers
(KU Leuven, Belgium)


Publisher's Version

Partial Type Constructors: Or, Making Ad Hoc Datatypes Less Ad Hoc
Mark P. Jones, J. Garrett Morris, and Richard A. Eisenberg
(Portland State University, USA; University of Kansas, USA; Bryn Mawr College, USA; Tweag I/O, UK)


Publisher's Version

Stacked Borrows: An Aliasing Model for Rust
Ralf Jung, Hoang-Hai Dang, Jeehoon Kang, and Derek Dreyer
(MPI-SWS, Germany; Mozilla, USA; KAIST, South Korea)


Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Abstract Interpretation of Distributed Network Control Planes
Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker
(Microsoft Research, USA; Princeton University, USA; University of Washington, USA; Intentionet, USA)


Publisher's Version

Executable Formal Semantics for the POSIX Shell
Michael Greenberg and Austin J. Blatt
(Pomona College, USA; Puppet Labs, USA)


Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset
Timothy Bourke, Lélio Brun, and Marc Pouzet
(Inria, France; ENS, France; PSL University, France; Sorbonne University, France)


Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

The Future is Ours: Prophecy Variables in Separation Logic
Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, and Bart Jacobs
(MPI-SWS, Germany; ETH Zurich, Switzerland; University of Waterloo, Canada; KU Leuven, Belgium)


Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Graduality and Parametricity: Together Again for the First Time
Max S. New, Dustin Jamner, and Amal Ahmed
(Northeastern University, USA)


Publisher's Version

Disentanglement in Nested-Parallel Programs
Sam Westrick, Rohan Yadav, Matthew Fluet, and Umut A. Acar
(Carnegie Mellon University, USA; Rochester Institute of Technology, USA)


Publisher's Version

Binders by Day, Labels by Night: Effect Instances via Lexically Scoped Handlers
Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski
(University of Wrocław, Poland)


Publisher's Version Artifacts Functional

Visualization by Example
Chenglong Wang, Yu Feng, Rastislav Bodik, Alvin Cheung, and Isil Dillig
(University of Washington, USA; University of California at Santa Barbara, USA; University of California at Berkeley, USA; University of Texas at Austin, USA)


Publisher's Version Published Artifact Artifacts Available Artifacts Functional

A Language for Probabilistically Oblivious Computation
David Darais, Ian Sweet, Chang Liu, and Michael Hicks
(University of Vermont, USA; University of Maryland, USA; Citadel Securities, USA)


Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Interaction Trees: Representing Recursive and Impure Programs in Coq
Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic
(University of Pennsylvania, USA; Seoul National University, South Korea; BedRock Systems, USA)


Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Synthesizing Replacement Classes
Malavika Samak, Deokhwan Kim, and Martin C. Rinard
(Massachusetts Institute of Technology, USA)


Publisher's Version

Kind Inference for Datatypes
Ningning Xie, Richard A. Eisenberg, and Bruno C. d. S. Oliveira
(University of Hong Kong, China; Bryn Mawr College, USA; Tweag I/O, UK)


Publisher's Version

Synthesis of Coordination Programs from Linear Temporal Specifications
Suguman Bansal, Kedar S. Namjoshi, and Yaniv Sa'ar
(Rice University, USA; Nokia Bell Labs, USA; Nokia Bell Labs, Israel)


Publisher's Version Artifacts Functional

A Probabilistic Separation Logic
Gilles Barthe, Justin Hsu, and Kevin Liao
(MPI for Security and Privacy, Germany; IMDEA Software Institute, Spain; University of Wisconsin-Madison, USA; University of Illinois at Urbana-Champaign, USA)


Publisher's Version

Augmented Example-Based Synthesis using Relational Perturbation Properties
Shengwei An, Rishabh Singh, Sasa Misailovic, and Roopsha Samanta
(Purdue University, USA; Google, USA; University of Illinois at Urbana-Champaign, USA)


Publisher's Version

Semantics of Higher-Order Probabilistic Programs with Conditioning
Fredrik Dahlqvist and Dexter Kozen
(University College London, UK; Imperial College London, UK; Cornell University, USA)


Publisher's Version

The Fire Triangle: How to Mix Substitution, Dependent Elimination, and Effects
Pierre-Marie Pédrot and Nicolas Tabareau
(Inria, France)


Publisher's Version

SyTeCi: Automating Contextual Equivalence for Higher-Order Programs with References
Guilhem Jaber
(University of Nantes, France; LS2N CNRS, France; Inria, France)


Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Detecting Floating-Point Errors via Atomic Conditions
Daming Zou, Muhan Zeng, Yingfei Xiong, Zhoulai Fu, Lu Zhang, and Zhendong Su
(Peking University, China; IT University of Copenhagen, Denmark; ETH Zurich, Switzerland)


Publisher's Version

Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time
Steffen Smolka, Nate Foster, Justin Hsu, Tobias Kappé, Dexter Kozen, and Alexandra Silva
(Cornell University, USA; University of Wisconsin-Madison, USA; University College London, UK)


Publisher's Version

Provenance-Guided Synthesis of Datalog Programs
Mukund Raghothaman, Jonathan Mendelson, David Zhao, Mayur Naik, and Bernhard Scholz
(University of Southern California, USA; University of Pennsylvania, USA; University of Sydney, Australia)


Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Full Abstraction for the Quantum Lambda-Calculus
Pierre Clairambault and Marc de Visme
(University of Lyon, France; ENS Lyon, France; CNRS, France; LIP, France)


Publisher's Version

Backpropagation in the Simply Typed Lambda-Calculus with Linear Negation
Aloïs Brunel, Damiano Mazza, and Michele Pagani
(Deepomatic, France; CNRS, France; IRIF, France; University of Paris Diderot, France)


Publisher's Version

Does Blame Shifting Work?
Lukas Lazarek, Alexis King, Samanvitha Sundar, Robert Bruce Findler, and Christos Dimoulas
(Northwestern University, USA)


Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Decidable Subtyping for Path Dependent Types
Julian Mackay, Alex Potanin, Jonathan Aldrich, and Lindsay Groves
(Victoria University of Wellington, New Zealand; Carnegie Mellon University, USA)


Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Label-Dependent Session Types
Peter Thiemann and Vasco T. Vasconcelos
(University of Freiburg, Germany; University of Lisbon, Portugal)


Publisher's Version

Pointer Life Cycle Types for Lock-Free Data Structures with Memory Reclamation
Roland Meyer and Sebastian Wolff
(TU Braunschweig, Germany)


Publisher's Version Published Artifact Artifacts Available Artifacts Reusable