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

Proceedings of the ACM on Programming Languages, Volume 9, Number POPL, January 19–25, 2025, Denver, CO, USA

POPL – Journal Issue

Contents - Abstracts - Authors

Frontmatter

Title Page
Editorial Message
POPL 2025 Sponsors and Supporters

Papers

RE#: High Performance Derivative-Based Regex Matching with Intersection, Complement, and Restricted Lookarounds
Ian Erik Varatalu, Margus Veanes, and Juhan Ernits
(Tallinn University of Technology, Estonia; Microsoft Research, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Symbolic Automata: Omega-Regularity Modulo Theories
Margus Veanes, Thomas Ball, Gabriel Ebner, and Ekaterina Zhuchko
(Microsoft Research, USA; Tallinn University of Technology, Estonia)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Maximal Simplification of Polyhedral Reductions
Louis Narmour, Tomofumi Yuki, and Sanjay Rajopadhye
(Colorado State University, USA; University of Rennes - Inria - CNRS - IRISA, France; Unaffiliated, Japan)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
MimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age
Roland Leißa, Marcel Ullrich, Joachim Meyer, and Sebastian Hack
(University of Mannheim, Germany; Saarland University, Germany)
Publisher's Version Published Artifact Info Artifacts Available
Affect: An Affine Type and Effect System
Orpheas van Rooij and Robbert Krebbers
(Radboud University, Nijmegen, Netherlands; University of Edinburgh, Edinburgh, UK)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Qurts: Automatic Quantum Uncomputation by Affine Types with Lifetime
Kengo Hirata and Chris Heunen
(University of Edinburgh, United Kingdom; Kyoto University, Japan)
Publisher's Version
Consistency of a Dependent Calculus of Indistinguishability
Yiyun Liu, Jonathan Chan, and Stephanie Weirich
(University of Pennsylvania, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
BiSikkel: A Multimode Logical Framework in Agda
Joris Ceulemans, Andreas Nuyts, and Dominique Devriese
(KU Leuven, Belgium)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Flo: A Semantic Foundation for Progressive Stream Processing
Shadaj Laddad, Alvin Cheung, Joseph M. Hellerstein, and Mae Milano
(University of California at Berkeley, USA; Princeton University, USA)
Publisher's Version
Inference Plans for Hybrid Particle Filtering
Ellie Y. Cheng, Eric Atkinson, Guillaume Baudart, Louis Mandel, and Michael Carbin
(Massachusetts Institute of Technology, USA; Binghamton University, USA; Université Paris Cité - CNRS - Inria - IRIF, France; IBM, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Program Logics à la Carte
Max Vistrup, Michael Sammler, and Ralf Jung
(ETH Zurich, Switzerland)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
The Duality of λ-Abstraction
Vikraman Choudhury and Simon J. Gay
(University of Bologna, Italy; Inria, France; University of Glasgow, United Kingdom)
Publisher's Version Published Artifact Info Artifacts Available
Finite-Choice Logic Programming
Chris Martens, Robert J. Simmons, and Michael Arntzenius
(Northeastern University, USA; Unaffiliated, USA)
Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable
On Extending Incorrectness Logic with Backwards Reasoning
Freek Verbeek, Md Syadus Sefat, Zhoulai Fu, and Binoy Ravindran
(Open University of the Netherlands, Netherlands; Virginia Tech, USA; State University of New York, South Korea; Stony Brook University, USA)
Publisher's Version Published Artifact Artifacts Available
A Dependent Type Theory for Meta-programming with Intensional Analysis
Jason Z. S. Hu and Brigitte Pientka
(McGill University, Canada)
Publisher's Version
Calculational Design of Hyperlogics by Abstract Interpretation
Patrick Cousot and Jeffery Wang
(New York University, USA)
Publisher's Version Info
Axe ’Em: Eliminating Spurious States with Induction Axioms
Neta Elad and Sharon Shoham
(Tel Aviv University, Israel)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Program Analysis via Multiple Context Free Language Reachability
Giovanna Kobus Conrado, Adam Husted Kjelstrøm, Jaco van de Pol, and Andreas Pavlogiannis
(Hong Kong University of Science and Technology, Hong Kong; Aarhus University, Denmark)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
A Demonic Outcome Logic for Randomized Nondeterminism
Noam Zilberstein, Dexter Kozen, Alexandra Silva, and Joseph Tassarotti
(Cornell University, USA; New York University, USA)
Publisher's Version
Formal Foundations for Translational Separation Logic Verifiers
Thibault Dardinier, Michael Sammler, Gaurav Parthasarathy, Alexander J. Summers, and Peter Müller
(ETH Zurich, Switzerland; University of British Columbia, Canada)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
CF-GKAT: Efficient Validation of Control-Flow Transformations
Cheng Zhang, Tobias Kappé, David E. Narváez, and Nico Naus
(University College London, United Kingdom; Leiden University, Netherlands; Virginia Tech, USA; Open University of the Netherlands, Netherlands)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Progressful Interpreters for Efficient WebAssembly Mechanisation
Xiaojia Rao, Stefan Radziuk, Conrad Watt, and Philippa Gardner
(Imperial College London, United Kingdom; Nanyang Technological University, Singapore)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Data Race Freedom à la Mode
Aïna Linn Georges, Benjamin Peters, Laila Elbeheiry, Leo White, Stephen Dolan, Richard A. Eisenberg, Chris Casinghino, François Pottier, and Derek Dreyer
(MPI-SWS, Germany; Jane Street, United Kingdom; Jane Street, USA; Inria, France)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
A Verified Foreign Function Interface between Coq and C
Joomy Korkut, Kathrin Stark, and Andrew W. Appel
(Princeton University, USA; Bloomberg, USA; Heriot-Watt University, United Kingdom)
Publisher's Version
Algebras for Deterministic Computation Are Inherently Incomplete
Balder ten Cate and Tobias Kappé
(University of Amsterdam, Netherlands; Leiden University, Netherlands)
Publisher's Version
Simple Linear Loops: Algebraic Invariants and Applications
Rida Ait El Manssour, George Kenison, Mahsa Shirmohammadi, and Anton Varonka
(CNRS - IRIF, France; Liverpool John Moores University, United Kingdom; TU Wien, Austria)
Publisher's Version
Denotational Semantics of Gradual Typing using Synthetic Guarded Domain Theory
Eric Giovannini, Tingting Ding, and Max S. New
(University of Michigan, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Pantograph: A Fluid and Typed Structure Editor
Jacob Prinz, Henry Blanchette, and Leonidas Lampropoulos
(University of Maryland at College Park, USA)
Publisher's Version Published Artifact Artifacts Available
TensorRight: Automated Verification of Tensor Graph Rewrites
Jai Arora, Sirui Lu, Devansh Jain, Tianfan Xu, Farzin Houshmand, Phitchaya Mangpo Phothilimthana, Mohsen Lesani, Praveen Narayanan, Karthik Srinivasa Murthy, Rastislav Bodik, Amit Sabne, and Charith Mendis
(University of Illinois at Urbana-Champaign, USA; University of Washington, USA; Google, USA; Google DeepMind, USA; University of California at Santa Cruz, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
A Modal Deconstruction of Löb Induction
Daniel Gratzer
(Aarhus University, Denmark)
Publisher's Version
Do You Even Lift? Strengthening Compiler Security Guarantees against Spectre Attacks
Xaver Fabian, Marco Patrignani, Marco Guarnieri, and Michael Backes
(CISPA Helmholtz Center for Information Security, Germany; University of Trento, Italy; IMDEA Software Institute, Spain)
Publisher's Version
Verifying Quantum Circuits with Level-Synchronized Tree Automata
Parosh Aziz Abdulla, Yo-Ga Chen, Yu-Fang Chen, Lukáš Holík, Ondřej Lengál, Jyun-Ao Lin, Fang-Yi Lo, and Wei-Lun Tsai
(Uppsala University, Sweden; Academia Sinica, Taiwan; Brno University of Technology, Czechia; Aalborg University, Denmark; National Taipei University of Technology, Taiwan)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
QuickSub: Efficient Iso-Recursive Subtyping
Litao Zhou and Bruno C. d. S. Oliveira
(University of Hong Kong, China)
Publisher's Version Published Artifact Info Artifacts Available Artifacts Functional
The Decision Problem for Regular First Order Theories
Umang Mathur, David Mestel, and Mahesh Viswanathan
(National University of Singapore, Singapore; Maastricht University, Netherlands; University of Illinois at Urbana-Champaign, USA)
Publisher's Version
Abstract Operational Methods for Call-by-Push-Value
Sergey Goncharov, Stelios Tsampas, and Henning Urbat
(University of Birmingham, United Kingdom; FAU Erlangen-Nuremberg, Germany)
Publisher's Version
Top-Down or Bottom-Up? Complexity Analyses of Synchronous Multiparty Session Types
Thien Udomsrirungruang and Nobuko Yoshida
(University of Oxford, United Kingdom)
Publisher's Version Info
Linear and Non-linear Relational Analyses for Quantum Program Optimization
Matthew Amy and Joseph Lunderville
(Simon Fraser University, Canada)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Guaranteed Bounds on Posterior Distributions of Discrete Probabilistic Programs with Loops
Fabian Zaiser, Andrzej S. Murawski, and C.-H. Luke Ong
(University of Oxford, United Kingdom; Nanyang Technological University, Singapore)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus
Naoki Kobayashi
(University of Tokyo, Japan)
Publisher's Version
A Quantitative Probabilistic Relational Hoare Logic
Martin Avanzini, Gilles Barthe, Davide Davoli, and Benjamin Grégoire
(Centre Inria d’Université Côte d’Azur, France; MPI-SP, Germany; IMDEA Software Institute, Spain)
Publisher's Version
Approximate Relational Reasoning for Higher-Order Probabilistic Programs
Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Joseph Tassarotti, and Lars Birkedal
(Aarhus University, Denmark; New York University, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Automating Equational Proofs in Dirac Notation
Yingte Xu, Gilles Barthe, and Li Zhou
(MPI-SP, Germany; Institute of Software at Chinese Academy of Sciences, China; IMDEA Software Institute, Spain)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Fulminate: Testing CN Separation-Logic Specifications in C
Rini Banerjee, Kayvan Memarian, Dhruv Makwana, Christopher Pulte, Neel Krishnaswami, and Peter Sewell
(University of Cambridge, United Kingdom)
Publisher's Version
Preservation of Speculative Constant-Time by Compilation
Santiago Arranz Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, and Vincent Laporte
(MPI-SP, Germany; IMDEA Software Institute, Spain; Inria, France; Université de Lorraine, France)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting
Yonghyun Kim, Minki Cho, Jaehyung Lee, Jinwoo Kim, Taeyoung Yoon, Youngju Song, and Chung-Kil Hur
(Seoul National University, South Korea; MPI-SWS, Germany)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
The Best of Abstract Interpretations
Roberto Giacobazzi and Francesco Ranzato
(University of Arizona, USA; University of Padova, Italy)
Publisher's Version
Flexible Type-Based Resource Estimation in Quantum Circuit Description Languages
Andrea Colledan and Ugo Dal Lago
(University of Bologna, Italy; Inria, France)
Publisher's Version
Modelling Recursion and Probabilistic Choice in Guarded Type Theory
Philipp Stassen, Rasmus Ejlers Møgelberg, Maaike Annebet Zwart, Alejandro Aguirre, and Lars Birkedal
(Aarhus University, Denmark; IT University of Copenhagen, Denmark)
Publisher's Version
Generic Refinement Types
Nico Lehmann, Cole Kurashige, Nikhil Akiti, Niroop Krishnakumar, and Ranjit Jhala
(University of California at San Diego, USA)
Publisher's Version
Derivative-Guided Symbolic Execution
Yongwei Yuan, Zhe Zhou, Julia Belyakova, and Suresh Jagannathan
(Purdue University, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations
Sören van der Wall and Roland Meyer
(TU Braunschweig, Germany)
Publisher's Version
Translation of Temporal Logic for Efficient Infinite-State Reactive Synthesis
Philippe Heim and Rayna Dimitrova
(CISPA Helmholtz Center for Information Security, Germany)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Coinductive Proofs for Temporal Hyperliveness
Arthur Correnson and Bernd Finkbeiner
(CISPA Helmholtz Center for Information Security, Germany)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Compositional Imprecise Probability: A Solution from Graded Monads and Markov Categories
Jack Liell-Cock and Sam Staton
(University of Oxford, United Kingdom)
Publisher's Version
Interaction Equivalence
Beniamino Accattoli, Adrienne Lancelot, Giulio Manzonetto, and Gabriele Vanoni
(Inria - Ecole Polytechnique, France; Inria - Ecole Polytechnique - IRIF - Université Paris Cité, France; Université Paris Cité, France)
Publisher's Version
Formalising Graph Algorithms with Coinduction
Donnacha Oisín Kidney and Nicolas Wu
(Imperial College London, United Kingdom)
Publisher's Version
Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings
Jan van Brügge, James McKinna, Andrei Popescu, and Dmitriy Traytel
(Heriot-Watt University, United Kingdom; University of Sheffield, United Kingdom; University of Copenhagen, Denmark)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Bluebell: An Alliance of Relational Lifting and Independence for Probabilistic Reasoning
Jialu Bao, Emanuele D'Osualdo, and Azadeh Farzan
(Cornell University, USA; MPI-SWS, Germany; University of Konstanz, Germany; University of Toronto, Canada)
Publisher's Version
Semantic Logical Relations for Timed Message-Passing Protocols
Yue Yao, Grant Iraci, Cheng-En Chuang, Stephanie Balzer, and Lukasz Ziarek
(Carnegie Mellon University, USA; University at Buffalo, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests
Lena Verscht and Benjamin Lucien Kaminski
(Saarland University, Germany; RWTH Aachen University, Germany; University College London, United Kingdom)
Publisher's Version
VeriRT: An End-to-End Verification Framework for Real-Time Distributed Systems
Yoonseung Kim, Sung-Hwan Lee, Yonghyun Kim, and Chung-Kil Hur
(Seoul National University, South Korea; Yale University, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Reachability Analysis of the Domain Name System
Dhruv Nevatia, Si Liu, and David Basin
(ETH Zurich, Switzerland)
Publisher's Version Info
Sound and Complete Proof Rules for Probabilistic Termination
Rupak Majumdar and V.R. Sathiyanarayana
(MPI-SWS, Germany)
Publisher's Version
Unifying Compositional Verification and Certified Compilation with a Three-Dimensional Refinement Algebra
Yu Zhang, Jérémie Koenig, Zhong Shao, and Yuting Wang
(Yale University, USA; Shanghai Jiao Tong University, China)
Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable
An Incremental Algorithm for Algebraic Program Analysis
Chenyu Zhou, Yuzhou Fang, Jingbo Wang, and Chao Wang
(University of Southern California, USA; Purdue University, USA)
Publisher's Version
Avoiding Signature Avoidance in ML Modules with Zippers
Clément Blaudeau, Didier Rémy, and Gabriel Radanne
(Inria, France; Université de Paris Cité, France; EnsL, France; Université Claude Bernard Lyon 1, France; CNRS, France)
Publisher's Version
Generically Automating Separation Logic by Functors, Homomorphisms, and Modules
Qiyuan Xu, David Sanan, Zhe Hou, Xiaokun Luan, Conrad Watt, and Yang Liu
(Nanyang Technological University, Singapore; Singapore Institute of Technology, Singapore; Griffith University, Australia; Peking University, China)
Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable
A Primal-Dual Perspective on Program Verification Algorithms
Takeshi Tsukada, Hiroshi Unno, Oded Padon, and Sharon Shoham
(Chiba University, Japan; Tohoku University, Japan; Weizmann Institute of Science, Israel; Tel Aviv University, Israel)
Publisher's Version
Automated Program Refinement: Guide and Verify Code Large Language Model with Refinement Calculus
Yufan Cai, Zhe Hou, David Sanan, Xiaokun Luan, Yun Lin, Jun Sun, and Jin Song Dong
(Ningbo University, China; National University of Singapore, Singapore; Griffith University, Australia; Singapore Institute of Technology, Singapore; Peking University, China; Shanghai Jiao Tong University, China; Singapore Management University, Singapore)
Publisher's Version
RELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency
Pavel Golovin, Michalis Kokologiannakis, and Viktor Vafeiadis
(MPI-SWS, Germany; ETH Zurich, Switzerland)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Bidirectional Higher-Rank Polymorphism with Intersection and Union Types
Shengyi Jiang, Chen Cui, and Bruno C. d. S. Oliveira
(University of Hong Kong, China)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Relaxed Memory Concurrency Re-executed
Evgenii Moiseenko, Matteo Meluzzi, Innokentii Meleshchenko, Ivan Kabashnyi, Anton Podkopaev, and Soham Chakraborty
(JetBrains Research, Serbia; TU Delft, Netherlands; JetBrains Research, Cyprus; Neapolis University Pafos, Cyprus; JetBrains Research, Germany; Constructor University Bremen, Germany; JetBrains Research, Netherlands)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Grove: A Bidirectionally Typed Collaborative Structure Editor Calculus
Michael D. Adams, Eric Griffis, Thomas J. Porter, Sundara Vishnu Satish, Eric Zhao, and Cyrus Omar
(National University of Singapore, Singapore; University of Michigan, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Biparsers: Exact Printing for Data Synchronisation
Ruifeng Xie, Tom Schrijvers, and Zhenjiang Hu
(Peking University, China; KU Leuven, Belgium)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Model Checking C/C++ with Mixed-Size Accesses
Iason Marmanis, Michalis Kokologiannakis, and Viktor Vafeiadis
(MPI-SWS, Germany; ETH Zurich, Switzerland)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants
Josselin Poiret, Gaëtan Gilbert, Kenji Maillard, Pierre-Marie Pédrot, Matthieu Sozeau, Nicolas Tabareau, and Éric Tanter
(Nantes Université, France; Inria, France; University of Chile, Chile)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Dis/Equality Graphs
George Zakhour, Pascal Weisenburger, Jahrim Gabriele Cesario, and Guido Salvaneschi
(University of St. Gallen, Switzerland)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order Programs
Taro Sekiyama and Hiroshi Unno
(National Institute of Informatics, Japan; SOKENDAI, Japan; Tohoku University, Japan)
Publisher's Version
Tail Modulo Cons, OCaml, and Relational Separation Logic
Clément Allain, Frédéric Bour, Basile Clément, François Pottier, and Gabriel Scherer
(Inria, France; Tarides, France; OCamlPro, France; Université Paris Cité, France)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

proc time: 30.5