POPL 2021
Proceedings of the ACM on Programming Languages, Volume 5, Number POPL

Title Page

Editorial Message

Cyclic Proofs, System T, and the Power of Contraction
Denis Kuperberg, Laureline Pinault, and Damien Pous
(University of Lyon, France; CNRS, France; ENS Lyon, France; Claude Bernard University Lyon 1, France; LIP, France)

Publisher's Version

Diamonds Are Not Forever: Liveness in Reactive Programming with Guarded Recursion
Patrick Bahr, Christian Uldal Graulund, and Rasmus Ejlers Møgelberg
(IT University of Copenhagen, Denmark)

Publisher's Version

𝜆ₛ: Computable Semantics for Differentiable Programming with Higher-Order Functions and Datatypes
Benjamin Sherman, Jesse Michel, and Michael Carbin
(Massachusetts Institute of Technology, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

Verifying Observational Robustness against a C11-Style Memory Model
Roy Margalit and Ori Lahav
(Tel Aviv University, Israel)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

On Algebraic Abstractions for Concurrent Separation Logics
František Farka, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, and Ignacio Fábregas
(IMDEA Software Institute, Spain; Nomadic Labs, France; Complutense University of Madrid, Spain)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable Artifacts Functional

Efficient and Provable Local Capability Revocation using Uninitialized Capabilities
Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Sander Huyghebaert, Dominique Devriese, and Lars Birkedal
(Aarhus University, Denmark; KU Leuven, Belgium; Vrije Universiteit Brussel, Belgium)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Fully Abstract from Static to Gradual
Koen Jacobs, Amin Timany, and Dominique Devriese
(KU Leuven, Belgium; Aarhus University, Denmark; Vrije Universiteit Brussel, Belgium)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

Deciding Accuracy of Differential Privacy Schemes
Gilles Barthe, Rohit Chadha, Paul Krogmeier, A. Prasad Sistla, and Mahesh Viswanathan
(MPI-SP, Germany; University of Missouri, USA; University of Illinois at Urbana-Champaign, USA; University of Illinois at Chicago, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

A Computational Interpretation of Compact Closed Categories: Reversible Programming with Negative and Fractional Types
Chao-Hong Chen and Amr Sabry
(Indiana University, USA)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable Artifacts Functional

Mechanized Logical Relations for Termination-Insensitive Noninterference
Simon Oddershede Gregersen, Johan Bay, Amin Timany, and Lars Birkedal
(Aarhus University, Denmark)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable Artifacts Functional

Probabilistic Programming Semantics for Name Generation
Marcin Sabok, Sam Staton, Dario Stein, and Michael Wolman
(McGill University, Canada; University of Oxford, UK)

Publisher's Version

Internalizing Representation Independence with Univalence
Carlo Angiuli, Evan Cavallo, Anders Mörtberg, and Max Zeuner
(Carnegie Mellon University, USA; Stockholm University, Sweden)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Transfinite Step-Indexing for Termination
Simon Spies, Neel Krishnaswami, and Derek Dreyer
(MPI-SWS, Germany; University of Cambridge, UK)

Publisher's Version Info

Generating Collection Transformations from Proofs
Michael Benedikt and Pierre Pradic
(University of Oxford, UK)

Publisher's Version

Learning the Boundary of Inductive Invariants
Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, and James R. Wilcox
(Tel Aviv University, Israel; Certora, USA)

Publisher's Version

Precise Subtyping for Asynchronous Multiparty Sessions
Silvia Ghilezan, Jovanka Pantović, Ivan Prokić, Alceste Scalas, and Nobuko Yoshida
(University of Novi Sad, Serbia; DTU, Denmark; Aston University, UK; Imperial College London, UK)

Publisher's Version

Verifying Correct Usage of Context-Free API Protocols
Kostas Ferles, Jon Stephens, and Isil Dillig
(University of Texas at Austin, USA)

Publisher's Version

Provably Space-Efficient Parallel Functional Programming
Jatin Arora, Sam Westrick, and Umut A. Acar
(Carnegie Mellon University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

Data Flow Refinement Type Inference
Zvonimir Pavlinovic, Yusen Su, and Thomas Wies
(New York University, USA; Google, USA; University of Waterloo, Canada)

Publisher's Version

Simplifying Dependent Reductions in the Polyhedral Model
Cambridge Yang, Eric Atkinson, and Michael Carbin
(Massachusetts Institute of Technology, USA)

Publisher's Version

On the Semantic Expressiveness of Recursive Types
Marco Patrignani, Eric Mark Martin, and Dominique Devriese
(Stanford University, USA; CISPA, Germany; Vrije Universiteit Brussel, Belgium)

Publisher's Version

Intrinsically Typed Compilation with Nameless Labels
Arjen Rouvoet, Robbert Krebbers, and Eelco Visser
(Delft University of Technology, Netherlands; Radboud University Nijmegen, Netherlands)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

egg: Fast and Extensible Equality Saturation
Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha
(University of Washington, USA; University of Utah, USA)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable Artifacts Functional

Asynchronous Effects
Danel Ahman and Matija Pretnar
(University of Ljubljana, Slovenia)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

Modeling and Analyzing Evaluation Cost of CUDA Kernels
Stefan K. Muller and Jan Hoffmann
(Illinois Institute of Technology, USA; Carnegie Mellon University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

Dijkstra Monads Forever: Termination-Sensitive Specifications for Interaction Trees
Lucas Silver and Steve Zdancewic
(University of Pennsylvania, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

A Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis
Vineet Rajani, Marco Gaboardi, Deepak Garg, and Jan Hoffmann
(MPI-SP, Germany; Boston University, USA; MPI-SWS, Germany; Carnegie Mellon University, USA)

Publisher's Version

Automatic Differentiation in PCF
Damiano Mazza and Michele Pagani
(CNRS, France; University of Paris, France)

Publisher's Version

An Approach to Generate Correctly Rounded Math Libraries for New Floating Point Variants
Jay P. Lim, Mridul Aanjaneya, John Gustafson, and Santosh Nagarakatte
(Rutgers University, USA; National University of Singapore, Singapore)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

Semantics-Guided Synthesis
Jinwoo Kim, Qinheping Hu, Loris D'Antoni, and Thomas Reps
(University of Wisconsin-Madison, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

An Abstract Interpretation for SPMD Divergence on Reducible Control Flow Graphs
Julian Rosemann, Simon Moll, and Sebastian Hack
(Saarland University, Germany; NEC, Germany)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Functional

Intersection Types and (Positive) Almost-Sure Termination
Ugo Dal Lago, Claudia Faggian, and Simona Ronchi Della Rocca
(University of Bologna, Italy; University of Paris, France; IRIF, France; CNRS, France; University of Turin, Italy)

Publisher's Version

A Separation Logic for Effect Handlers
Paulo Emílio de Vilhena and François Pottier
(Inria, France)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable Artifacts Functional

The Fine-Grained and Parallel Complexity of Andersen’s Pointer Analysis
Anders Alnor Mathiasen and Andreas Pavlogiannis
(Aarhus University, Denmark)

Publisher's Version

Giving Semantics to Program-Counter Labels via Secure Effects
Andrew K. Hirsch and Ethan Cecchetti
(MPI-SWS, Germany; Cornell University, USA)

Publisher's Version Info

Optimal Prediction of Synchronization-Preserving Races
Umang Mathur, Andreas Pavlogiannis, and Mahesh Viswanathan
(University of Illinois at Urbana-Champaign, USA; Aarhus University, Denmark)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

A Verified Optimizer for Quantum Circuits
Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, and Michael Hicks
(University of Maryland, USA; University of Chicago, USA)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Functional

Automata and Fixpoints for Asynchronous Hyperproperties
Jens Oliver Gutsfeld, Markus Müller-Olm, and Christoph Ohrem
(University of Münster, Germany)

Publisher's Version

Relatively Complete Verification of Probabilistic Programs: An Expressive Language for Expectation-Based Reasoning
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja
(RWTH Aachen University, Germany; University College London, UK; ETH Zurich, Switzerland)

Publisher's Version

Verified Code Generation for the Polyhedral Model
Nathanaël Courant and Xavier Leroy
(Inria, France; Collège de France, France; PSL University, France)

Publisher's Version

Petr4: Formal Foundations for P4 Data Planes
Ryan Doenges, Mina Tahmasbi Arashloo, Santiago Bautista, Alexander Chang, Newton Ni, Samwise Parkinson, Rudy Peterson, Alaia Solko-Breslin, Amanda Xu, and Nate Foster
(Cornell University, USA; ENS Rennes, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic
Léon Gondelman, Simon Oddershede Gregersen, Abel Nieto, Amin Timany, and Lars Birkedal
(Aarhus University, Denmark)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

PerSeVerE: Persistency Semantics for Verification under Ext4
Michalis Kokologiannakis, Ilya Kaysin, Azalea Raad, and Viktor Vafeiadis
(MPI-SWS, Germany; National Research University Higher School of Economics, Russia; JetBrains Research, Russia; Imperial College London, UK)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable Artifacts Functional

Context-Bounded Verification of Liveness Properties for Multithreaded Shared-Memory Programs
Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche
(MPI-SWS, Germany)

Publisher's Version

A Practical Mode System for Recursive Definitions
Alban Reynaud, Gabriel Scherer, and Jeremy Yallop
(ENS Lyon, France; Inria, France; University of Cambridge, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

Formally Verified Speculation and Deoptimization in a JIT Compiler
Aurèle Barrière, Sandrine Blazy, Olivier Flückiger, David Pichardie, and Jan Vitek
(University of Rennes, France; Inria, France; CNRS, France; IRISA, France; Northeastern University, USA; Czech Technical University, Czechia)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

Taming x86-TSO Persistency
Artem Khyzha and Ori Lahav
(Tel Aviv University, Israel)

Publisher's Version

Deciding ω-Regular Properties on Linear Recurrence Sequences
Shaull Almagor, Toghrul Karimov, Edon Kelmendi, Joël Ouaknine, and James Worrell
(Technion, Israel; MPI-SWS, Germany; University of Oxford, UK)

Publisher's Version

Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade
Marco Vassena, Craig Disselkoen, Klaus von Gleissenthall, Sunjay Cauligi, Rami Gökhan Kıcı, Ranjit Jhala, Dean Tullsen, and Deian Stefan
(CISPA, Germany; University of California at San Diego, USA; Vrije Universiteit Amsterdam, Netherlands)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

A Graded Dependent Type System with a Usage-Aware Semantics
Pritam Choudhury, Harley Eades III, Richard A. Eisenberg, and Stephanie Weirich
(University of Pennsylvania, USA; Augusta University, USA; Tweag I/O, France; Bryn Mawr College, USA)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable Artifacts Functional

The (In)Efficiency of Interaction
Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni
(Inria, France; École Polytechnique, France; University of Bologna, Italy)

Publisher's Version

A Pre-expectation Calculus for Probabilistic Sensitivity
Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja
(IMDEA Software Institute, Spain; Universidad Politécnica de Madrid, Spain; MPI-SP, Germany; University of Wisconsin-Madison, USA; University College London, UK; RWTH Aachen University, Germany; ETH Zurich, Switzerland)

Publisher's Version

Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification
Cameron Moy, Phúc C. Nguyễn, Sam Tobin-Hochstadt, and David Van Horn
(Northeastern University, USA; University of Maryland, USA; Indiana University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

Combining the Top-Down Propagation and Bottom-Up Enumeration for Inductive Program Synthesis
Woosuk Lee
(Hanyang University, South Korea)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

Intensional Datatype Refinement: With Application to Scalable Verification of Pattern-Match Safety
Eddie Jones and Steven Ramsay
(University of Bristol, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

Deciding Reachability under Persistent x86-TSO
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan
(Uppsala University, Sweden; University of Paris, France; Chennai Mathematical Institute, India; CNRS UMI ReLaX, India; Institute of Mathematical Sciences, India)

Publisher's Version

Functorial Semantics for Partial Theories
Ivan Di Liberti, Fosco Loregian, Chad Nester, and Paweł Sobociński
(Czech Academy of Sciences, Czechia; Tallinn University of Technology, Estonia)

Publisher's Version

Paradoxes of Probabilistic Programming: And How to Condition on Events of Measure Zero with Infinitesimal Probabilities
Jules Jacobs
(Radboud University Nijmegen, Netherlands; Delft University of Technology, Netherlands)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

On the Complexity of Bidirected Interleaved Dyck-Reachability
Yuanbo Li, Qirun Zhang, and Thomas Reps
(Georgia Institute of Technology, USA; University of Wisconsin-Madison, USA)

Publisher's Version

The Taming of the Rew: A Type Theory with Computational Assumptions
Jesper Cockx, Nicolas Tabareau, and Théo Winterhalter
(Delft University of Technology, Netherlands; Inria, France; LS2N, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Abstracting Gradual Typing Moving Forward: Precise and Space-Efficient
Felipe Bañados Schwerter, Alison M. Clark, Khurram A. Jafery, and Ronald Garcia
(University of British Columbia, Canada; Amazon, Canada)

Publisher's Version