POPL 2023
Proceedings of the ACM on Programming Languages, Volume 7, Number POPL

Title Page

Editorial Message

Sponsors

CN: Verifying Systems C Code with Separation-Logic Refinement Types
Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, and Neel Krishnaswami
(University of Cambridge, UK)

Publisher's Version

Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice
Alejandro Aguirre and Lars Birkedal
(Aarhus University, Denmark)

Publisher's Version

A Type-Based Approach to Divide-and-Conquer Recursion in Coq
Pedro Abreu, Benjamin Delaware, Alex Hubers, Christa Jenkins, J. Garrett Morris, and Aaron Stump
(Purdue University, USA; University of Iowa, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Comparative Synthesis: Learning Near-Optimal Network Designs by Query
Yanjun Wang, Zixuan Li, Chuan Jiang, Xiaokang Qiu, and Sanjay Rao
(Purdue University, USA)

Publisher's Version Archive submitted (1.3 MB) Artifacts Functional

ADEV: Sound Automatic Differentiation of Expected Values of Probabilistic Programs
Alexander K. Lew, Mathieu Huot, Sam Staton, and Vikash K. Mansinghka
(Massachusetts Institute of Technology, USA; University of Oxford, UK)

Publisher's Version Archive submitted (1 MB)

HFL(Z) Validity Checking for Automated Program Verification
Naoki Kobayashi, Kento Tanahashi, Ryosuke Sato, and Takeshi Tsukada
(University of Tokyo, Japan; Chiba University, Japan)

Publisher's Version

From SMT to ASP: Solver-Based Approaches to Solving Datalog Synthesis-as-Rule-Selection Problems
Aaron Bembenek, Michael Greenberg, and Stephen Chong
(Harvard University, USA; Stevens Institute of Technology, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Why Are Proofs Relevant in Proof-Relevant Models?
Axel Kerinec, Giulio Manzonetto, and Federico Olimpieri
(Université Sorbonne Paris Nord, France; LIPN, France; CNRS, France; University of Leeds, UK)

Publisher's Version

Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler
Aurèle Barrière, Sandrine Blazy, and David Pichardie
(University of Rennes, France; Inria, France; CNRS, France; IRISA, France; Meta, France)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable

On the Expressive Power of String Constraints
Joel D. Day, Vijay Ganesh, Nathan Grewal, and Florin Manea
(Loughborough University, UK; University of Waterloo, Canada; University of Göttingen, Germany)

Publisher's Version

Proto-Quipper with Dynamic Lifting
Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger
(Dalhousie University, Canada; University of Illinois at Urbana-Champaign, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Smoothness Analysis for Probabilistic Programs with Application to Optimised Variational Inference
Wonyeol Lee, Xavier Rival, and Hongseok Yang
(Stanford University, USA; Inria, France; ENS, France; CNRS, France; PSL University, France; KAIST, South Korea; IBS, South Korea)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Executing Microservice Applications on Serverless, Correctly
Konstantinos Kallas, Haoran Zhang, Rajeev Alur, Sebastian Angel, and Vincent Liu
(University of Pennsylvania, USA; Microsoft Research, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

babble: Learning Better Abstractions with E-Graphs and Anti-unification
David Cao, Rose Kunkel, Chandrakana Nandi, Max Willsey, Zachary Tatlock, and Nadia Polikarpova
(University of California at San Diego, USA; Certora, USA; University of Washington, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code
Alexandra E. Michael, Anitha Gollamudi, Jay Bosamiya, Evan Johnson, Aidan Denlinger, Craig Disselkoen, Conrad Watt, Bryan Parno, Marco Patrignani, Marco Vassena, and Deian Stefan
(University of California at San Diego, USA; University of Washington, USA; University of Massachusetts Lowell, USA; Carnegie Mellon University, USA; Arm, USA; University of Cambridge, UK; University of Trento, Italy; Utrecht University, Netherlands)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Functional

Grisette: Symbolic Compilation as a Functional Programming Library
Sirui Lu and Rastislav Bodík
(University of Washington, USA; Google Research, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Locally Nameless Sets
Andrew M. Pitts
(University of Cambridge, UK)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable

A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F⋈
Nick Rioux, Xuejing Huang, Bruno C. d. S. Oliveira, and Steve Zdancewic
(University of Pennsylvania, USA; University of Hong Kong, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Kater: Automating Weak Memory Model Metatheory and Consistency Checking
Michalis Kokologiannakis, Ori Lahav, and Viktor Vafeiadis
(MPI-SWS, Germany; Tel Aviv University, Israel)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

An Algebra of Alignment for Relational Verification
Timos Antonopoulos, Eric Koskinen, Ton Chanh Le, Ramana Nagasamudram, David A. Naumann, and Minh Ngo
(Yale University, USA; Stevens Institute of Technology, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Optimal CHC Solving via Termination Proofs
Yu Gu, Takeshi Tsukada, and Hiroshi Unno
(University of Tsukuba, Japan; Chiba University, Japan; RIKEN AIP, Japan)

Publisher's Version

Towards a Higher-Order Mathematical Operational Semantics
Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat
(University of Erlangen-Nuremberg, Germany)

Publisher's Version

Unrealizability Logic
Jinwoo Kim, Loris D'Antoni, and Thomas Reps
(University of Wisconsin-Madison, USA; Seoul National University, South Korea)

Publisher's Version

The Geometry of Causality: Multi-token Geometry of Interaction and Its Causal Unfolding
Simon Castellan and Pierre Clairambault
(University of Rennes, France; Inria, France; CNRS, France; IRISA, France; Université Aix-Marseille, France; Université de Toulon, France; LIS, France)

Publisher's Version Info Artifacts Functional

A High-Level Separation Logic for Heap Space under Garbage Collection
Alexandre Moine, Arthur Charguéraud, and François Pottier
(Inria, France; Université de Strasbourg, France; CNRS, France; ICube, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

The Path to Durable Linearizability
Emanuele D'Osualdo, Azalea Raad, and Viktor Vafeiadis
(MPI-SWS, Germany; Imperial College London, UK)

Publisher's Version

DimSum: A Decentralized Approach to Multi-language Semantics and Verification
Michael Sammler, Simon Spies, Youngju Song, Emanuele D'Osualdo, Robbert Krebbers, Deepak Garg, and Derek Dreyer
(MPI-SWS, Germany; Radboud University Nijmegen, Netherlands)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

A General Noninterference Policy for Polynomial Time
Emmanuel Hainry and Romain Péchoux
(Université de Lorraine, France; CNRS, France; Inria, France; LORIA, France)

Publisher's Version

CoqQ: Foundational Verification of Quantum Programs
Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, and Mingsheng Ying
(MPI-SP, Germany; Institute of Software at Chinese Academy of Sciences, China; IMDEA Software Institute, Spain; Meta, France; University of Chinese Academy of Sciences, China; Tsinghua University, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

A Core Calculus for Equational Proofs of Cryptographic Protocols
Joshua Gancher, Kristina Sojakova, Xiong Fan, Elaine Shi, and Greg Morrisett
(Carnegie Mellon University, USA; Inria, France; Rutgers University, USA; Cornell University, USA)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable

Making a Type Difference: Subtraction on Intersection Types as Generalized Record Operations
Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira
(Peking University, China; University of Hong Kong, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Qunity: A Unified Language for Quantum and Classical Computing
Finn Voichick, Liyi Li, Robert Rand, and Michael Hicks
(University of Maryland, USA; University of Chicago, USA; Amazon, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

FlashFill++: Scaling Programming by Example by Cutting to the Chase
José Cambronero, Sumit Gulwani, Vu Le, Daniel Perelman, Arjun Radhakrishna, Clint Simon, and Ashish Tiwari
(Microsoft, USA)

Publisher's Version

Witnessability of Undecidable Problems
Shuo Ding and Qirun Zhang
(Georgia Institute of Technology, USA)

Publisher's Version

Single-Source-Single-Target Interleaved-Dyck Reachability via Integer Linear Programming
Yuanbo Li, Qirun Zhang, and Thomas Reps
(Georgia Institute of Technology, USA; University of Wisconsin-Madison, USA)

Publisher's Version

Higher-Order Leak and Deadlock Free Locks
Jules Jacobs and Stephanie Balzer
(Radboud University Nijmegen, Netherlands; Carnegie Mellon University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

A Robust Theory of Series Parallel Graphs
Rajeev Alur, Caleb Stanford, and Christopher Watson
(University of Pennsylvania, USA; University of California at San Diego, USA; University of California at Davis, USA)

Publisher's Version

A Compositional Theory of Linearizability
Arthur Oliveira Vale, Zhong Shao, and Yixuan Chen
(Yale University, USA)

Publisher's Version Info

Conditional Contextual Refinement
Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Sammler, and Derek Dreyer
(Seoul National University, South Korea; MPI-SWS, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Tail Recursion Modulo Context: An Equational Approach
Daan Leijen and Anton Lorenzen
(Microsoft Research, USA; University of Edinburgh, UK)

Publisher's Version

Top-Down Synthesis for Library Learning
Matthew Bowers, Theo X. Olausson, Lionel Wong, Gabriel Grand, Joshua B. Tenenbaum, Kevin Ellis, and Armando Solar-Lezama
(Massachusetts Institute of Technology, USA; Cornell University, USA)

Publisher's Version Published Artifact Archive submitted (1.6 MB) Info Artifacts Available Artifacts Reusable

Admissible Types-to-PERs Relativization in Higher-Order Logic
Andrei Popescu and Dmitriy Traytel
(University of Sheffield, UK; University of Copenhagen, Denmark)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

You Only Linearize Once: Tangents Transpose to Gradients
Alexey Radul, Adam Paszke, Roy Frostig, Matthew J. Johnson, and Dougal Maclaurin
(Google Research, USA; Google Research, Poland)

Publisher's Version

When Less Is More: Consequence-Finding in a Weak Theory of Arithmetic
Zachary Kincaid, Nicolas Koh, and Shaowei Zhu
(Princeton University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Dynamic Race Detection with O(1) Samples
Mosaad Al Thokair, Minjian Zhang, Umang Mathur, and Mahesh Viswanathan
(University of Illinois at Urbana-Champaign, USA; National University of Singapore, Singapore)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Affine Monads and Lazy Structures for Bayesian Programming
Swaraj Dash, Younesse Kaddar, Hugo Paquet, and Sam Staton
(University of Oxford, UK)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable

Dargent: A Silver Bullet for Verified Data Layout Refinement
Zilin Chen, Ambroise Lafont, Liam O'Connor, Gabriele Keller, Craig McLaughlin, Vincent Jackson, and Christine Rizkallah
(UNSW, Australia; University of Cambridge, UK; University of Edinburgh, UK; Utrecht University, Netherlands; University of Melbourne, Australia)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Recursive Subtyping for All
Litao Zhou, Yaoda Zhou, and Bruno C. d. S. Oliveira
(University of Hong Kong, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Stratified Commutativity in Verification Algorithms for Concurrent Programs
Azadeh Farzan, Dominik Klumpp, and Andreas Podelski
(University of Toronto, Canada; University of Freiburg, Germany)

Publisher's Version Archive submitted (780 kB)

Type-Preserving, Dependence-Aware Guide Generation for Sound, Effective Amortized Probabilistic Inference
Jianlin Li, Leni Ven, Pengyuan Shi, and Yizhou Zhang
(University of Waterloo, Canada)

Publisher's Version

Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework
Victor Arrial, Giulio Guerrieri, and Delia Kesner
(Université Paris Cité - CNRS - IRIF, France; Aix Marseille Université - CNRS - LIS, France; Edinburgh Research Centre - Central Software Institute - Huawei, UK; Institut Universitaire de France, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Fast Coalgebraic Bisimilarity Minimization
Jules Jacobs and Thorsten Wißmann
(Radboud University Nijmegen, Netherlands)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

An Operational Approach to Library Abstraction under Relaxed Memory Concurrency
Abhishek Kr Singh and Ori Lahav
(Tel Aviv University, Israel)

Publisher's Version

Efficient Dual-Numbers Reverse AD via Well-Known Program Transformations
Tom J. Smeding and Matthijs I. L. Vákár
(Utrecht University, Netherlands)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

A Partial Order View of Message-Passing Communication Models
Cinzia Di Giusto, Davide Ferré, Laetitia Laversa, and Etienne Lozes
(Université Côte d'Azur, France; CNRS, France)

Publisher's Version

Combining Functional and Automata Synthesis to Discover Causal Reactive Programs
Ria Das, Joshua B. Tenenbaum, Armando Solar-Lezama, and Zenna Tavares
(Stanford University, USA; Massachusetts Institute of Technology, USA; Basis, USA; Columbia University, USA)

Publisher's Version Archive submitted (780 kB)

An Order-Theoretic Analysis of Universe Polymorphism
Kuen-Bang Hou (Favonia), Carlo Angiuli, and Reed Mullanix
(University of Minnesota, USA; Carnegie Mellon University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Statically Resolvable Ambiguity
Viktor Palmkvist, Elias Castegren, Philipp Haller, and David Broman
(KTH Royal Institute of Technology, Sweden; Uppsala University, Sweden)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

The Fine-Grained Complexity of CFL Reachability
Paraschos Koutris and Shaleen Deep
(University of Wisconsin-Madison, USA; Microsoft, USA)

Publisher's Version

Taking Back Control in an Intermediate Representation for GPU Computing
Vasileios Klimis, Jack Clark, Alan Baker, David Neto, John Wickerson, and Alastair F. Donaldson
(Imperial College London, UK; Google, Canada; Google, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq
Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, and Steve Zdancewic
(University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, France; University of Pennsylvania, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Hefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects
Casper Bach Poulsen and Cas van der Rest
(Delft University of Technology, Netherlands)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Elements of Quantitative Rewriting
Francesco Gavazzo and Cecilia Di Florio
(University of Pisa, Italy; University of Bologna, Italy)

Publisher's Version

Deconstructing the Calculus of Relations with Tape Diagrams
Filippo Bonchi, Alessandro Di Giorgio, and Alessio Santamaria
(University of Pisa, Italy; University of Sussex, UK)

Publisher's Version

SSA Translation Is an Abstract Interpretation
Matthieu Lemerre
(Université Paris-Saclay - CEA LIST, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Probabilistic Resource-Aware Session Types
Ankush Das, Di Wang, and Jan Hoffmann
(Amazon, USA; Carnegie Mellon University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

A Calculus for Amortized Expected Runtimes
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Lena Verscht
(RWTH Aachen University, Germany; Saarland University, Germany; University College London, UK; DTU, Denmark)

Publisher's Version

Reconciling Shannon and Scott with a Lattice of Computable Information
Sebastian Hunt, David Sands, and Sandro Stucki
(City University of London, UK; Chalmers University of Technology, Sweden; Amazon Prime Video, Sweden)

Publisher's Version

Higher-Order MSL Horn Constraints
Jerome Jochems, Eddie Jones, and Steven Ramsay
(University of Bristol, UK)

Publisher's Version

Inductive Synthesis of Structurally Recursive Functional Programs from Non-recursive Expressions
Woosuk Lee and Hangyeol Cho
(Hanyang University, South Korea)

Publisher's Version Published Artifact Archive submitted (710 kB) Artifacts Available Artifacts Reusable

Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations
Taro Sekiyama and Hiroshi Unno
(National Institute of Informatics, Japan; University of Tsukuba, Japan; RIKEN AIP, Japan)

Publisher's Version Archive submitted (940 kB)

Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification
Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinen
(University of Tsukuba, Japan; RIKEN AIP, Japan; Waseda University, Japan; Stevens Institute of Technology, USA)

Publisher's Version

Context-Bounded Verification of Context-Free Specifications
Pascal Baumann, Moses Ganardi, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche
(MPI-SWS, Germany)

Publisher's Version

Impredicative Observational Equality
Loïc Pujet and Nicolas Tabareau
(Inria, France)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable