POPL 2025
Proceedings of the ACM on Programming Languages, Volume 9, Number POPL

Title Page

Editorial Message

Sponsors

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)

Article Search Artifacts Available

Symbolic Automata: Omega-Regularity Modulo Theories
Margus Veanes, Thomas Ball, Gabriel Ebner, and Ekaterina Zhuchko
(Microsoft Research, USA; Tallinn University of Technology, Estonia)

Article Search Artifacts Available

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)

Article Search Artifacts Available

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)

Preprint 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)

Article Search Artifacts Available

Qurts: Automatic Quantum Uncomputation by Affine Types with Lifetime
Kengo Hirata and Chris Heunen
(University of Edinburgh, United Kingdom; Kyoto University, Japan)

Article Search

Consistency of a Dependent Calculus of Indistinguishability
Yiyun Liu, Jonathan Chan, and Stephanie Weirich
(University of Pennsylvania, USA)

Article Search Artifacts Available

BiSikkel: A Multimode Logical Framework in Agda
Joris Ceulemans, Andreas Nuyts, and Dominique Devriese
(KU Leuven, Belgium)

Article Search Artifacts Available

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)

Article Search

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)

Article Search Artifacts Available

Program Logics à la Carte
Max Vistrup, Michael Sammler, and Ralf Jung
(ETH Zurich, Switzerland)

Article Search Artifacts Available

The Duality of λ-Abstraction
Vikraman Choudhury and Simon J. Gay
(University of Bologna, Italy; Inria, France; University of Glasgow, United Kingdom)

Preprint Info Artifacts Available

Finite-Choice Logic Programming
Chris Martens, Robert J. Simmons, and Michael Arntzenius
(Northeastern University, USA; Unaffiliated, USA)

Preprint Info Artifacts Available

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)

Article Search Artifacts Available

A Dependent Type Theory for Meta-programming with Intensional Analysis
Jason Z. S. Hu and Brigitte Pientka
(McGill University, Canada)

Article Search

Calculational Design of Hyperlogics by Abstract Interpretation
Patrick Cousot and Jeffery Wang
(New York University, USA)

Preprint

Axe ’Em: Eliminating Spurious States with Induction Axioms
Neta Elad and Sharon Shoham
(Tel Aviv University, Israel)

Article Search Artifacts Available

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)

Article Search Artifacts Available

A Demonic Outcome Logic for Randomized Nondeterminism
Noam Zilberstein, Dexter Kozen, Alexandra Silva, and Joseph Tassarotti
(Cornell University, USA; New York University, USA)

Article Search

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)

Preprint Artifacts Available

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)

Preprint Artifacts Available

Progressful Interpreters for Efficient WebAssembly Mechanisation
Xiaojia Rao, Stefan Radziuk, Conrad Watt, and Philippa Gardner
(Imperial College London, United Kingdom; Nanyang Technological University, Singapore)

Preprint Artifacts Available

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)

Article Search Artifacts Available

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)

Article Search

Algebras for Deterministic Computation Are Inherently Incomplete
Balder ten Cate and Tobias Kappé
(University of Amsterdam, Netherlands; Leiden University, Netherlands)

Preprint

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)

Article Search

Denotational Semantics of Gradual Typing using Synthetic Guarded Domain Theory
Eric Giovannini, Tingting Ding, and Max S. New
(University of Michigan, USA)

Article Search Artifacts Available

Pantograph: A Fluid and Typed Structure Editor
Jacob Prinz, Henry Blanchette, and Leonidas Lampropoulos
(University of Maryland at College Park, USA)

Preprint 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)

Article Search Artifacts Available

A Modal Deconstruction of Löb Induction
Daniel Gratzer
(Aarhus University, Denmark)

Article Search

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)

Article Search

Verifying Quantum Circuits with Level-Synchronized Tree Automata
Parosh Aziz Abdulla, Yo-Ga Chen, Yu-Fang Chen, Lukáš Holík, Ondrej Lengal, 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)

Preprint Artifacts Available

QuickSub: Efficient Iso-Recursive Subtyping
Litao Zhou and Bruno C. d. S. Oliveira
(University of Hong Kong, China)

Article Search Info Artifacts Available

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)

Article Search

Abstract Operational Methods for Call-by-Push-Value
Sergey Goncharov, Stelios Tsampas, and Henning Urbat
(University of Birmingham, United Kingdom; FAU Erlangen-Nuremberg, Germany)

Article Search

Top-Down or Bottom-Up? Complexity Analyses of Synchronous Multiparty Session Types
Thien Udomsrirungruang and Nobuko Yoshida
(University of Oxford, United Kingdom)

Article Search Info

Linear and Non-linear Relational Analyses for Quantum Program Optimization
Matthew Amy and Joseph Lunderville
(Simon Fraser University, Canada)

Preprint Artifacts Available

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)

Article Search Artifacts Available

On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus
Naoki Kobayashi
(University of Tokyo, Japan)

Article Search

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)

Article Search

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)

Preprint

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)

Preprint Artifacts Available

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)

Article Search

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)

Article Search

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)

Article Search Artifacts Available

The Best of Abstract Interpretations
Roberto Giacobazzi and Francesco Ranzato
(University of Arizona, USA; University of Padova, Italy)

Article Search

Flexible Type-Based Resource Estimation in Quantum Circuit Description Languages
Andrea Colledan and Ugo Dal Lago
(University of Bologna, Italy; Inria, France)

Article Search

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)

Article Search

Generic Refinement Types
Nico Lehmann, Cole Kurashige, Nikhil Akiti, Niroop Krishnakumar, and Ranjit Jhala
(University of California at San Diego, USA)

Article Search

Derivative-Guided Symbolic Execution
Yongwei Yuan, Zhe Zhou, Julia Belyakova, and Suresh Jagannathan
(Purdue University, USA)

Preprint Artifacts Available

SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations
Sören van der Wall and Roland Meyer
(TU Braunschweig, Germany)

Preprint

Translation of Temporal Logic for Efficient Infinite-State Reactive Synthesis
Philippe Heim and Rayna Dimitrova
(CISPA Helmholtz Center for Information Security, Germany)

Article Search Artifacts Available

Coinductive Proofs for Temporal Hyperliveness
Arthur Correnson and Bernd Finkbeiner
(CISPA Helmholtz Center for Information Security, Germany)

Article Search Artifacts Available

Compositional Imprecise Probability: A Solution from Graded Monads and Markov Categories
Jack Liell-Cock and Sam Staton
(University of Oxford, United Kingdom)

Article Search

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)

Article Search

Formalising Graph Algorithms with Coinduction
Donnacha Oisín Kidney and Nicolas Wu
(Imperial College London, United Kingdom)

Preprint

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)

Article Search Artifacts Available

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)

Preprint

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)

Preprint Artifacts Available

A Taxonomy of Hoare-Like Logics
Lena Verscht and Benjamin Lucien Kaminski
(Saarland University, Germany; RWTH Aachen University, Germany; University College London, United Kingdom)

Preprint

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)

Article Search Artifacts Available

Reachability Analysis of the Domain Name System
Dhruv Nevatia, Si Liu, and David Basin
(ETH Zurich, Switzerland)

Article Search Info

Sound and Complete Proof Rules for Probabilistic Termination
Rupak Majumdar and V.R. Sathiyanarayana
(MPI-SWS, Germany)

Article Search

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)

Article Search Info Artifacts Available

An Incremental Algorithm for Algebraic Program Analysis
Chenyu Zhou, Yuzhou Fang, Jingbo Wang, and Chao Wang
(University of Southern California, USA; Purdue University, USA)

Article Search

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)

Article Search

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)

Preprint Info Artifacts Available

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)

Article Search

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; Nanyang Technological University, Singapore; Peking University, China; Shanghai Jiao Tong University, China; Singapore Management University, Singapore)

Article Search

RELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency
Pavel Golovin, Michalis Kokologiannakis, and Viktor Vafeiadis
(MPI-SWS, Germany; ETH Zurich, Switzerland)

Article Search

Bidirectional Higher-Rank Polymorphism with Intersection and Union Types
Shengyi Jiang, Chen Cui, and Bruno C. d. S. Oliveira
(University of Hong Kong, China)

Article Search Artifacts Available

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, n.n.; Constructor University Bremen, Germany)

Article Search Artifacts Available

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)

Article Search Artifacts Available

Biparsers: Exact Printing for Data Synchronisation
Ruifeng Xie, Tom Schrijvers, and Zhenjiang Hu
(Peking University, China; KU Leuven, Belgium)

Article Search Artifacts Available

Model Checking C/C++ with Mixed-Size Accesses
Iason Marmanis, Michalis Kokologiannakis, and Viktor Vafeiadis
(MPI-SWS, Germany; ETH Zurich, Switzerland)

Article Search

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)

Article Search Artifacts Available

Dis/Equality Graphs
George Zakhour, Pascal Weisenburger, Jahrim Gabriele Cesario, and Guido Salvaneschi
(University of St. Gallen, Switzerland)

Article Search Artifacts Available

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)

Article Search

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)

Article Search