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

Title Page

Article: popl20foreword-fm000-p doi:

Editorial Message

Article: popl20foreword-fm001-p doi:

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

Publisher's Version Article: popl20main-p6-p doi:10.1145/3371069

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 Article: popl20main-p7-p doi:10.1145/3371070

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 Article: popl20main-p18-p doi:10.1145/3371071

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 Article: popl20main-p24-p doi:10.1145/3371072

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 Article: popl20main-p25-p doi:10.1145/3371073

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 Article: popl20main-p29-p doi:10.1145/3371074

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 Article: popl20main-p31-p doi:10.1145/3371075

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 Article: popl20main-p34-p doi:10.1145/3371076

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 Article: popl20main-p35-p doi:10.1145/3371077

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

Publisher's Version Article: popl20main-p36-p doi:10.1145/3371078

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 Article: popl20main-p39-p doi:10.1145/3371079

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 Article: popl20main-p40-p doi:10.1145/3371080

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

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p42-p doi:10.1145/3371081

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 Article: popl20main-p45-p doi:10.1145/3371082

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 Article: popl20main-p46-p doi:10.1145/3371083

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 Article: popl20main-p48-p doi:10.1145/3371084

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

Publisher's Version Article: popl20main-p50-p doi:10.1145/3371085

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 Article: popl20main-p62-p doi:10.1145/3371086

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 Article: popl20main-p69-p doi:10.1145/3371087

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 Article: popl20main-p73-p doi:10.1145/3371088

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 Article: popl20main-p78-p doi:10.1145/3371089

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 Article: popl20main-p91-p doi:10.1145/3371090

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 Article: popl20main-p93-p doi:10.1145/3371091

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 Article: popl20main-p94-p doi:10.1145/3371092

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 Article: popl20main-p96-p doi:10.1145/3371093

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 Article: popl20main-p97-p doi:10.1145/3371094

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 Article: popl20main-p98-p doi:10.1145/3371095

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 Article: popl20main-p99-p doi:10.1145/3371096

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 Article: popl20main-p104-p doi:10.1145/3371097

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 Article: popl20main-p105-p doi:10.1145/3371098

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 Article: popl20main-p112-p doi:10.1145/3371099

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 Article: popl20main-p114-p doi:10.1145/3371100

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 Article: popl20main-p117-p doi:10.1145/3371101

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 Article: popl20main-p124-p doi:10.1145/3371102

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 Article: popl20main-p125-p doi:10.1145/3371103

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 Article: popl20main-p126-p doi:10.1145/3371104

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 Article: popl20main-p127-p doi:10.1145/3371105

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

Publisher's Version Article: popl20main-p129-p doi:10.1145/3371106

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

Publisher's Version Article: popl20main-p131-p doi:10.1145/3371107

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 Article: popl20main-p136-p doi:10.1145/3371108

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 Article: popl20main-p147-p doi:10.1145/3371109

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 Article: popl20main-p150-p doi:10.1145/3371110

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 Article: popl20main-p153-p doi:10.1145/3371111

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 Article: popl20main-p155-p doi:10.1145/3371112

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 Article: popl20main-p157-p doi:10.1145/3371113

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

Publisher's Version Article: popl20main-p167-p doi:10.1145/3371114

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 Article: popl20main-p169-p doi:10.1145/3371115

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 Article: popl20main-p171-p doi:10.1145/3371116

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 Article: popl20main-p174-p doi:10.1145/3371117

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 Article: popl20main-p175-p doi:10.1145/3371118

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 Article: popl20main-p177-p doi:10.1145/3371119

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

Publisher's Version Article: popl20main-p186-p doi:10.1145/3371120

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 Article: popl20main-p189-p doi:10.1145/3371121

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 Article: popl20main-p194-p doi:10.1145/3371122

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 Article: popl20main-p202-p doi:10.1145/3371123

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 Article: popl20main-p204-p doi:10.1145/3371124

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 Article: popl20main-p213-p doi:10.1145/3371125

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

Publisher's Version Article: popl20main-p216-p doi:10.1145/3371126

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 Article: popl20main-p219-p doi:10.1145/3371127

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 Article: popl20main-p222-p doi:10.1145/3371128

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 Article: popl20main-p229-p doi:10.1145/3371129

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 Article: popl20main-p236-p doi:10.1145/3371130

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 Article: popl20main-p242-p doi:10.1145/3371131

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 Article: popl20main-p243-p doi:10.1145/3371132

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 Article: popl20main-p246-p doi:10.1145/3371133

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 Article: popl20main-p248-p doi:10.1145/3371134

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

Publisher's Version Article: popl20main-p257-p doi:10.1145/3371135

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 Article: popl20main-p265-p doi:10.1145/3371136