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


Title Page
Editorial Message


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)
Article Search
Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice
Alejandro Aguirre ORCID logo and Lars BirkedalORCID logo
(Aarhus University, Denmark)
Article Search
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)
Article Search
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)
Article Search Archive submitted (1.3 MB)
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)
Article Search
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)
Article Search
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)
Article Search
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; University of Leeds, UK)
Article Search
Formally Verified Native Code Generation in an Effectful JIT - or: 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)
Preprint Info
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)
Article Search
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)
Article Search
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; KAIST, South Korea; IBS, n.n.)
Article Search
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)
Article Search
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, n.n.; University of Washington, USA)
Article Search
MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code
Alexandra E. Michael ORCID logo, Anitha Gollamudi ORCID logo, Jay Bosamiya, Evan Johnson, Aidan Denlinger, Craig Disselkoen, Conrad Watt, Bryan ParnoORCID logo, Marco Patrignani ORCID logo, Marco Vassena, and Deian Stefan
(University of California at San Diego, USA; University of Massachusetts Lowell, USA; Carnegie Mellon University, USA; University of Cambridge, UK; University of Trento, Italy; Utrecht University, Netherlands)
Article Search Info
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)
Article Search
Locally Nameless Sets
Andrew M. Pitts ORCID logo
(University of Cambridge, UK)
Preprint Info
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)
Article Search
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)
Article Search
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)
Article Search
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)
Article Search
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)
Article Search
Unrealizability Logic
Jinwoo Kim ORCID logo, Loris D'AntoniORCID logo, and Thomas RepsORCID logo
(University of Wisconsin-Madison, USA; Seoul National University, South Korea)
Article Search
The Geometry of Causality: Multi-token Geometry of Interaction and Its Causal Unfolding
Simon Castellan ORCID logo and Pierre Clairambault ORCID logo
(Inria, France; IRISA, France; CNRS, France; Université Aix-Marseille, France)
Preprint Info
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)
Article Search
The Path to Durable Linearizability
Emanuele D'OsualdoORCID logo, Azalea RaadORCID logo, and Viktor VafeiadisORCID logo
(MPI-SWS, Germany; Imperial College London, UK)
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)
Article Search
A General Noninterference Policy for Polynomial Time
Emmanuel Hainry ORCID logo and Romain Péchoux ORCID logo
(Inria, France; Université de Lorraine, France)
Article Search
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)
Article Search
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)
Article Search Info
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)
Article Search
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)
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; Microsoft, Vietnam)
Article Search
Witnessability of Undecidable Problems
Shuo Ding ORCID logo and Qirun Zhang ORCID logo
(Georgia Institute of Technology, USA)
Article Search
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, USA)
Article Search
Higher-Order Leak and Deadlock Free Locks
Jules JacobsORCID logo and Stephanie BalzerORCID logo
(Radboud University Nijmegen, Netherlands; Carnegie Mellon University, USA)
A Robust Theory of Series Parallel Graphs
Rajeev AlurORCID logo, Caleb StanfordORCID logo, and Christopher WatsonORCID logo
(University of Pennsylvania, USA; University of California at San Diego, USA; University of California at Davis, USA)
Article Search
A Compositional Theory of Linearizability
Arthur Oliveira Vale ORCID logo, Zhong Shao ORCID logo, and Yixuan Chen ORCID logo
(Yale University, USA)
Article Search 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)
Article Search
Tail Recursion Modulo Context: An Equational Approach
Daan LeijenORCID logo and Anton Lorenzen ORCID logo
(Microsoft Research, USA; University of Edinburgh, UK)
Article Search
Top-Down Synthesis for Library Learning
Matthew Bowers ORCID logo, Theo X. Olausson ORCID logo, Catherine 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)
Article Search Archive submitted (1.6 MB)
Admissible Types-to-PERs Relativization in Higher-Order Logic
Andrei PopescuORCID logo and Dmitriy TraytelORCID logo
(University of Sheffield, UK; University of Copenhagen, Denmark)
Article Search
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)
Article Search
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)
Article Search
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)
Article Search
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)
Article Search Info
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)
Article Search
Recursive Subtyping for All
Litao Zhou ORCID logo, Yaoda Zhou ORCID logo, and Bruno C. d. S. OliveiraORCID logo
(University of Hong Kong, China)
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)
Article Search 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)
Article Search
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)
Article Search
Fast Coalgebraic Bisimilarity Minimization
Jules JacobsORCID logo and Thorsten Wißmann ORCID logo
(Radboud University Nijmegen, Netherlands)
An Operational Approach to Library Abstraction under Relaxed Memory Concurrency
Abhishek Kr Singh ORCID logo and Ori LahavORCID logo
(Tel Aviv University, Israel)
Article Search
Efficient Dual-Numbers Reverse AD via Well-Known Program Transformations
Tom Smeding ORCID logo and Matthijs Vákár ORCID logo
(Utrecht University, Netherlands)
Article Search
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)
Article Search
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
(Massachusetts Institute of Technology, USA; Basis, USA; Columbia University, USA)
Article Search 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)
Article Search
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)
Article Search
The Fine-Grained Complexity of CFL Reachability
Paraschos Koutris ORCID logo and Shaleen Deep ORCID logo
(University of Wisconsin-Madison, USA; Microsoft, USA)
Article Search
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, UK)
Article Search
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
(ENS de Lyon, France; University of Pennsylvania, USA; CNRS, France; Inria, France)
Article Search
Hefty Algebras for Higher-Order Algebraic Operations
Casper Bach Poulsen ORCID logo
(Delft University of Technology, Netherlands)
Article Search
Elements of Quantitative Rewriting
Francesco Gavazzo ORCID logo and Cecilia Di Florio ORCID logo
(University of Pisa, Italy; University of Bologna, Italy)
Article Search
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)
Article Search
SSA Translation Is an Abstract Interpretation
Matthieu Lemerre ORCID logo
(CEA LIST, France)
Probabilistic Resource-Aware Session Types
Ankush Das ORCID logo, Di Wang ORCID logo, and Jan Hoffmann ORCID logo
(Amazon, USA; Carnegie Mellon University, USA)
Article Search
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)
Article Search
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)
Article Search
Higher-Order MSL Horn Constraints
Jerome Jochems ORCID logo, Eddie Jones ORCID logo, and Steven Ramsay ORCID logo
(University of Bristol, UK)
Article Search
Inductive Synthesis of Structurally Recursive Functional Programs from Non-recursive Expressions
Woosuk Lee and Hangyeol Cho
(Hanyang University, South Korea)
Article Search
Temporal Verification with Answer-Effect Modification
Taro SekiyamaORCID logo and Hiroshi UnnoORCID logo
(National Institute of Informatics, Japan; University of Tsukuba, Japan)
Article Search 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; Waseda University, Japan; Stevens Institute of Technology, USA)
Article Search
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)
Article Search
Impredicative Observational Equality
Loïc Pujet and Nicolas TabareauORCID logo
(Inria, France)
Article Search Info

proc time: 5.09