POPL – Journal Issue

Artifacts Functional Article: popl25main-p2-p doi:10.1145/3704837

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

Artifacts Reusable Article: popl25main-p11-p doi:10.1145/3704838

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)

Artifacts Functional Article: popl25main-p13-p doi:10.1145/3704839

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)

Info

Artifacts Available Article: popl25main-p20-p doi:10.1145/3704840

Affect: An Affine Type and Effect System
Orpheas van Rooij and Robbert Krebbers
(Radboud University, Nijmegen, Netherlands; University of Edinburgh, Edinburgh, UK)

Artifacts Reusable Article: popl25main-p22-p doi:10.1145/3704841

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 Article: popl25main-p27-p doi:10.1145/3704842

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

Artifacts Reusable Article: popl25main-p33-p doi:10.1145/3704843

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

Artifacts Reusable Article: popl25main-p37-p doi:10.1145/3704844

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 Article: popl25main-p38-p doi:10.1145/3704845

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)

Artifacts Reusable Article: popl25main-p40-p doi:10.1145/3704846

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

Artifacts Reusable Article: popl25main-p42-p doi:10.1145/3704847

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

Info

Artifacts Available Article: popl25main-p43-p doi:10.1145/3704848

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

Info

Artifacts Reusable Article: popl25main-p44-p doi:10.1145/3704849

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)

Artifacts Available Article: popl25main-p46-p doi:10.1145/3704850

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

Publisher's Version Article: popl25main-p47-p doi:10.1145/3704851

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

Info Article: popl25main-p51-p doi:10.1145/3704852

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

Artifacts Reusable Article: popl25main-p52-p doi:10.1145/3704853

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)

Artifacts Reusable Article: popl25main-p53-p doi:10.1145/3704854

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 Article: popl25main-p56-p doi:10.1145/3704855

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)

Artifacts Reusable Article: popl25main-p62-p doi:10.1145/3704856

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)

Artifacts Functional Article: popl25main-p65-p doi:10.1145/3704857

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

Artifacts Reusable Article: popl25main-p67-p doi:10.1145/3704858

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)

Artifacts Reusable Article: popl25main-p68-p doi:10.1145/3704859

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 Article: popl25main-p69-p doi:10.1145/3704860

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

Publisher's Version Article: popl25main-p71-p doi:10.1145/3704861

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 Article: popl25main-p81-p doi:10.1145/3704862

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

Artifacts Functional Article: popl25main-p83-p doi:10.1145/3704863

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

Artifacts Available Article: popl25main-p84-p doi:10.1145/3704864

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)

Artifacts Reusable Article: popl25main-p85-p doi:10.1145/3704865

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

Publisher's Version Article: popl25main-p95-p doi:10.1145/3704866

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 Article: popl25main-p98-p doi:10.1145/3704867

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)

Artifacts Reusable Article: popl25main-p100-p doi:10.1145/3704868

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

Info

Artifacts Functional Article: popl25main-p102-p doi:10.1145/3704869

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 Article: popl25main-p114-p doi:10.1145/3704870

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 Article: popl25main-p115-p doi:10.1145/3704871

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

Info Article: popl25main-p118-p doi:10.1145/3704872

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

Artifacts Reusable Article: popl25main-p119-p doi:10.1145/3704873

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)

Artifacts Reusable Article: popl25main-p126-p doi:10.1145/3704874

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

Publisher's Version Article: popl25main-p134-p doi:10.1145/3704875

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 Article: popl25main-p135-p doi:10.1145/3704876

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)

Artifacts Functional Article: popl25main-p139-p doi:10.1145/3704877

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)

Artifacts Reusable Article: popl25main-p140-p doi:10.1145/3704878

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 Article: popl25main-p143-p doi:10.1145/3704879

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)

Artifacts Reusable Article: popl25main-p144-p doi:10.1145/3704880

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)

Artifacts Reusable Article: popl25main-p147-p doi:10.1145/3704881

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

Publisher's Version Article: popl25main-p149-p doi:10.1145/3704882

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 Article: popl25main-p153-p doi:10.1145/3704883

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 Article: popl25main-p155-p doi:10.1145/3704884

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

Publisher's Version Article: popl25main-p176-p doi:10.1145/3704885

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

Artifacts Reusable Article: popl25main-p184-p doi:10.1145/3704886

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

Publisher's Version Article: popl25main-p185-p doi:10.1145/3704887

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

Artifacts Reusable Article: popl25main-p187-p doi:10.1145/3704888

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

Artifacts Reusable Article: popl25main-p191-p doi:10.1145/3704889

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 Article: popl25main-p199-p doi:10.1145/3704890

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 Article: popl25main-p200-p doi:10.1145/3704891

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

Publisher's Version Article: popl25main-p203-p doi:10.1145/3704892

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)

Artifacts Reusable Article: popl25main-p205-p doi:10.1145/3704893

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 Article: popl25main-p206-p doi:10.1145/3704894

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)

Artifacts Functional Article: popl25main-p210-p doi:10.1145/3704895

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 Article: popl25main-p219-p doi:10.1145/3704896

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)

Artifacts Reusable Article: popl25main-p224-p doi:10.1145/3704897

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

Info Article: popl25main-p226-p doi:10.1145/3704898

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

Publisher's Version Article: popl25main-p235-p doi:10.1145/3704899

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)

Info

Artifacts Reusable Article: popl25main-p239-p doi:10.1145/3704900

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 Article: popl25main-p250-p doi:10.1145/3704901

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 Article: popl25main-p252-p doi:10.1145/3704902

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)

Info

Artifacts Reusable Article: popl25main-p255-p doi:10.1145/3704903

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 Article: popl25main-p261-p doi:10.1145/3704904

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 Article: popl25main-p279-p doi:10.1145/3704905

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

Artifacts Reusable Article: popl25main-p280-p doi:10.1145/3704906

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

Artifacts Reusable Article: popl25main-p283-p doi:10.1145/3704907

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)

Artifacts Functional Article: popl25main-p291-p doi:10.1145/3704908

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)

Artifacts Functional Article: popl25main-p293-p doi:10.1145/3704909

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

Artifacts Reusable Article: popl25main-p300-p doi:10.1145/3704910

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

Artifacts Functional Article: popl25main-p301-p doi:10.1145/3704911

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)

Artifacts Reusable Article: popl25main-p305-p doi:10.1145/3704912

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

Artifacts Reusable Article: popl25main-p309-p doi:10.1145/3704913

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 Article: popl25main-p316-p doi:10.1145/3704914

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)