POPL 2023
Proceedings of the ACM on Programming Languages, Volume 7, Number POPL
Powered by
Conference Publishing Consulting

Proceedings of the ACM on Programming Languages, Volume 7, Number POPL, January 15–21, 2023, Boston, MA, USA

POPL – Journal Issue

Contents - Abstracts - Authors

Frontmatter

Title Page
Editorial Message
Sponsors

Papers

CN: Verifying Systems C Code with Separation-Logic Refinement Types
Christopher PulteORCID logo, Dhruv C. Makwana ORCID logo, Thomas Sewell ORCID logo, Kayvan Memarian ORCID logo, Peter Sewell ORCID logo, and Neel Krishnaswami ORCID logo
(University of Cambridge, UK)
Publisher's Version
Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice
Alejandro Aguirre ORCID logo and Lars BirkedalORCID logo
(Aarhus University, Denmark)
Publisher's Version
A Type-Based Approach to Divide-and-Conquer Recursion in Coq
Pedro Abreu ORCID logo, Benjamin DelawareORCID logo, Alex Hubers ORCID logo, Christa Jenkins ORCID logo, J. Garrett Morris ORCID logo, and Aaron Stump ORCID logo
(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 ORCID logo, Zixuan Li ORCID logo, Chuan Jiang ORCID logo, Xiaokang QiuORCID logo, and Sanjay Rao ORCID logo
(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. LewORCID logo, Mathieu Huot ORCID logo, Sam StatonORCID logo, and Vikash K. MansinghkaORCID logo
(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 KobayashiORCID logo, Kento Tanahashi ORCID logo, Ryosuke Sato ORCID logo, and Takeshi Tsukada ORCID logo
(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 ORCID logo, Michael Greenberg ORCID logo, and Stephen Chong ORCID logo
(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 ORCID logo, Giulio Manzonetto ORCID logo, and Federico Olimpieri ORCID logo
(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 ORCID logo, Sandrine Blazy ORCID logo, and David Pichardie ORCID logo
(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 ORCID logo, Vijay Ganesh ORCID logo, Nathan Grewal ORCID logo, and Florin Manea ORCID logo
(Loughborough University, UK; University of Waterloo, Canada; University of Göttingen, Germany)
Publisher's Version
Proto-Quipper with Dynamic Lifting
Peng Fu ORCID logo, Kohei Kishida ORCID logo, Neil J. Ross ORCID logo, and Peter Selinger ORCID logo
(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 ORCID logo, Xavier Rival ORCID logo, and Hongseok Yang ORCID logo
(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 KallasORCID logo, Haoran Zhang ORCID logo, Rajeev AlurORCID logo, Sebastian Angel ORCID logo, and Vincent Liu ORCID logo
(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 ORCID logo, Rose Kunkel ORCID logo, Chandrakana Nandi ORCID logo, Max WillseyORCID logo, Zachary Tatlock ORCID logo, and Nadia PolikarpovaORCID logo
(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 ORCID logo, Anitha Gollamudi ORCID logo, Jay Bosamiya ORCID logo, Evan Johnson ORCID logo, Aidan Denlinger ORCID logo, Craig Disselkoen ORCID logo, Conrad Watt ORCID logo, Bryan ParnoORCID logo, Marco Patrignani ORCID logo, Marco Vassena ORCID logo, and Deian Stefan ORCID logo
(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 ORCID logo and Rastislav Bodík ORCID logo
(University of Washington, USA; Google Research, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Locally Nameless Sets
Andrew M. Pitts ORCID logo
(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 ORCID logo, Xuejing Huang ORCID logo, Bruno C. d. S. OliveiraORCID logo, and Steve ZdancewicORCID logo
(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 KokologiannakisORCID logo, Ori LahavORCID logo, and Viktor VafeiadisORCID logo
(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 ORCID logo, Eric Koskinen ORCID logo, Ton Chanh Le ORCID logo, Ramana Nagasamudram ORCID logo, David A. Naumann ORCID logo, and Minh Ngo ORCID logo
(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 ORCID logo, Takeshi Tsukada ORCID logo, and Hiroshi UnnoORCID logo
(University of Tsukuba, Japan; Chiba University, Japan; RIKEN AIP, Japan)
Publisher's Version
Towards a Higher-Order Mathematical Operational Semantics
Sergey GoncharovORCID logo, Stefan Milius ORCID logo, Lutz SchröderORCID logo, Stelios Tsampas ORCID logo, and Henning Urbat ORCID logo
(University of Erlangen-Nuremberg, Germany)
Publisher's Version
Unrealizability Logic
Jinwoo Kim ORCID logo, Loris D'AntoniORCID logo, and Thomas RepsORCID logo
(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 ORCID logo and Pierre Clairambault ORCID logo
(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 ORCID logo, Arthur CharguéraudORCID logo, and François PottierORCID logo
(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'OsualdoORCID logo, Azalea RaadORCID logo, and Viktor VafeiadisORCID logo
(MPI-SWS, Germany; Imperial College London, UK)
Publisher's Version
DimSum: A Decentralized Approach to Multi-language Semantics and Verification
Michael Sammler ORCID logo, Simon Spies ORCID logo, Youngju Song ORCID logo, Emanuele D'OsualdoORCID logo, Robbert KrebbersORCID logo, Deepak GargORCID logo, and Derek DreyerORCID logo
(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 ORCID logo and Romain Péchoux ORCID logo
(Université de Lorraine, France; CNRS, France; Inria, France; LORIA, France)
Publisher's Version
CoqQ: Foundational Verification of Quantum Programs
Li Zhou ORCID logo, Gilles Barthe ORCID logo, Pierre-Yves Strub ORCID logo, Junyi Liu ORCID logo, and Mingsheng Ying ORCID logo
(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 ORCID logo, Kristina Sojakova ORCID logo, Xiong Fan ORCID logo, Elaine Shi ORCID logo, and Greg Morrisett ORCID logo
(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 ORCID logo, Xuejing Huang ORCID logo, and Bruno C. d. S. OliveiraORCID logo
(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 ORCID logo, Liyi Li ORCID logo, Robert RandORCID logo, and Michael HicksORCID logo
(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 ORCID logo, Sumit GulwaniORCID logo, Vu LeORCID logo, Daniel Perelman ORCID logo, Arjun Radhakrishna ORCID logo, Clint Simon ORCID logo, and Ashish Tiwari ORCID logo
(Microsoft, USA)
Publisher's Version
Witnessability of Undecidable Problems
Shuo Ding ORCID logo and Qirun Zhang ORCID logo
(Georgia Institute of Technology, USA)
Publisher's Version
Single-Source-Single-Target Interleaved-Dyck Reachability via Integer Linear Programming
Yuanbo Li ORCID logo, Qirun Zhang ORCID logo, and Thomas RepsORCID logo
(Georgia Institute of Technology, USA; University of Wisconsin-Madison, USA)
Publisher's Version
Higher-Order Leak and Deadlock Free Locks
Jules JacobsORCID logo and Stephanie BalzerORCID logo
(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 AlurORCID logo, Caleb Stanford ORCID logo, and Christopher WatsonORCID logo
(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 ORCID logo, Zhong Shao ORCID logo, and Yixuan Chen ORCID logo
(Yale University, USA)
Publisher's Version Info
Conditional Contextual Refinement
Youngju Song ORCID logo, Minki Cho ORCID logo, Dongjae Lee ORCID logo, Chung-Kil Hur ORCID logo, Michael Sammler ORCID logo, and Derek DreyerORCID logo
(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 LeijenORCID logo and Anton Lorenzen ORCID logo
(Microsoft Research, USA; University of Edinburgh, UK)
Publisher's Version
Top-Down Synthesis for Library Learning
Matthew Bowers ORCID logo, Theo X. Olausson ORCID logo, Lionel Wong ORCID logo, Gabriel Grand ORCID logo, Joshua B. Tenenbaum ORCID logo, Kevin Ellis ORCID logo, and Armando Solar-Lezama ORCID logo
(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 PopescuORCID logo and Dmitriy TraytelORCID logo
(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 ORCID logo, Adam Paszke ORCID logo, Roy Frostig ORCID logo, Matthew J. Johnson ORCID logo, and Dougal Maclaurin ORCID logo
(Google Research, USA; Google Research, Poland)
Publisher's Version
When Less Is More: Consequence-Finding in a Weak Theory of Arithmetic
Zachary Kincaid ORCID logo, Nicolas Koh ORCID logo, and Shaowei Zhu ORCID logo
(Princeton University, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Dynamic Race Detection with O(1) Samples
Mosaad Al Thokair ORCID logo, Minjian Zhang ORCID logo, Umang Mathur ORCID logo, and Mahesh Viswanathan ORCID logo
(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 ORCID logo, Younesse KaddarORCID logo, Hugo Paquet ORCID logo, and Sam StatonORCID logo
(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 ORCID logo, Ambroise Lafont ORCID logo, Liam O'ConnorORCID logo, Gabriele Keller ORCID logo, Craig McLaughlin ORCID logo, Vincent Jackson ORCID logo, and Christine Rizkallah ORCID logo
(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 ORCID logo, Yaoda Zhou ORCID logo, and Bruno C. d. S. OliveiraORCID logo
(University of Hong Kong, China)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Stratified Commutativity in Verification Algorithms for Concurrent Programs
Azadeh FarzanORCID logo, Dominik Klumpp ORCID logo, and Andreas Podelski ORCID logo
(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 ORCID logo, Leni Ven ORCID logo, Pengyuan Shi ORCID logo, and Yizhou ZhangORCID logo
(University of Waterloo, Canada)
Publisher's Version
Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework
Victor Arrial ORCID logo, Giulio Guerrieri ORCID logo, and Delia KesnerORCID logo
(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 JacobsORCID logo and Thorsten Wißmann ORCID logo
(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 ORCID logo and Ori LahavORCID logo
(Tel Aviv University, Israel)
Publisher's Version
Efficient Dual-Numbers Reverse AD via Well-Known Program Transformations
Tom J. Smeding ORCID logo and Matthijs I. L. Vákár ORCID logo
(Utrecht University, Netherlands)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
A Partial Order View of Message-Passing Communication Models
Cinzia Di Giusto ORCID logo, Davide Ferré ORCID logo, Laetitia Laversa ORCID logo, and Etienne Lozes ORCID logo
(Université Côte d'Azur, France; CNRS, France)
Publisher's Version
Combining Functional and Automata Synthesis to Discover Causal Reactive Programs
Ria Das ORCID logo, Joshua B. Tenenbaum ORCID logo, Armando Solar-Lezama ORCID logo, and Zenna Tavares ORCID logo
(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)ORCID logo, Carlo AngiuliORCID logo, and Reed Mullanix ORCID logo
(University of Minnesota, USA; Carnegie Mellon University, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Statically Resolvable Ambiguity
Viktor Palmkvist ORCID logo, Elias Castegren ORCID logo, Philipp Haller ORCID logo, and David Broman ORCID logo
(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 ORCID logo and Shaleen Deep ORCID logo
(University of Wisconsin-Madison, USA; Microsoft, USA)
Publisher's Version
Taking Back Control in an Intermediate Representation for GPU Computing
Vasileios Klimis ORCID logo, Jack Clark ORCID logo, Alan Baker ORCID logo, David Neto ORCID logo, John Wickerson ORCID logo, and Alastair F. DonaldsonORCID logo
(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 ORCID logo, Paul HeORCID logo, Ludovic Henrio ORCID logo, Yannick ZakowskiORCID logo, and Steve ZdancewicORCID logo
(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 ORCID logo and Cas van der RestORCID logo
(Delft University of Technology, Netherlands)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Elements of Quantitative Rewriting
Francesco Gavazzo ORCID logo and Cecilia Di Florio ORCID logo
(University of Pisa, Italy; University of Bologna, Italy)
Publisher's Version
Deconstructing the Calculus of Relations with Tape Diagrams
Filippo Bonchi ORCID logo, Alessandro Di Giorgio ORCID logo, and Alessio SantamariaORCID logo
(University of Pisa, Italy; University of Sussex, UK)
Publisher's Version
SSA Translation Is an Abstract Interpretation
Matthieu Lemerre ORCID logo
(Université Paris-Saclay - CEA LIST, France)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Probabilistic Resource-Aware Session Types
Ankush Das ORCID logo, Di Wang ORCID logo, and Jan Hoffmann ORCID logo
(Amazon, USA; Carnegie Mellon University, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
A Calculus for Amortized Expected Runtimes
Kevin Batz ORCID logo, Benjamin Lucien Kaminski ORCID logo, Joost-Pieter Katoen ORCID logo, Christoph Matheja ORCID logo, and Lena Verscht ORCID logo
(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 ORCID logo, David Sands ORCID logo, and Sandro Stucki ORCID logo
(City University of London, UK; Chalmers University of Technology, Sweden; Amazon Prime Video, Sweden)
Publisher's Version
Higher-Order MSL Horn Constraints
Jerome Jochems ORCID logo, Eddie Jones ORCID logo, and Steven Ramsay ORCID logo
(University of Bristol, UK)
Publisher's Version
Inductive Synthesis of Structurally Recursive Functional Programs from Non-recursive Expressions
Woosuk Lee ORCID logo and Hangyeol Cho ORCID logo
(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 SekiyamaORCID logo and Hiroshi UnnoORCID logo
(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 UnnoORCID logo, Tachio Terauchi ORCID logo, Yu Gu ORCID logo, and Eric Koskinen ORCID logo
(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 ORCID logo, Moses Ganardi ORCID logo, Rupak Majumdar ORCID logo, Ramanathan S. Thinniyam ORCID logo, and Georg Zetzsche ORCID logo
(MPI-SWS, Germany)
Publisher's Version
Impredicative Observational Equality
Loïc Pujet ORCID logo and Nicolas TabareauORCID logo
(Inria, France)
Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable

proc time: 15.32