POPL 2024
Proceedings of the ACM on Programming Languages, Volume 8, Number POPL

Title Page

Editorial Message

Sponsors

Ramsey Quantifiers in Linear Arithmetics
Pascal Bergsträßer , Moses Ganardi , Anthony W. Lin , and Georg Zetzsche 
(University of Kaiserslautern-Landau, Germany; MPI-SWS, Germany)

Published Artifact Artifacts Available

Deciding Asynchronous Hyperproperties for Recursive Programs
Jens Oliver Gutsfeld , Markus Müller-Olm , and Christoph Ohrem 
(University of Münster, Germany)

Shoggoth: A Formal Foundation for Strategic Rewriting
Xueying Qin , Liam O’Connor , Rob van Glabbeek , Peter Höfner , Ohad Kammar , and Michel Steuwer 
(University of Edinburgh, UK; UNSW, Sydney, Australia; Australian National University, Australia; TU Berlin, Germany)

Published Artifact Artifacts Available

Reachability in Continuous Pushdown VASS
A. R. Balasubramanian , Rupak Majumdar , Ramanathan S. Thinniyam , and Georg Zetzsche 
(MPI-SWS, Germany; Uppsala University, Sweden)

Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers
Fuga Kawamata , Hiroshi Unno , Taro Sekiyama , and Tachio Terauchi 
(Waseda University, Japan; University of Tsukuba, Japan; National Institute of Informatics, Japan)

An Iris Instance for Verifying CompCert C Programs
William Mansky  and Ke Du 
(University of Illinois Chicago, USA)

Published Artifact Artifacts Available

Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation
Patrick Cousot 
(New York University, USA)

Published Artifact Archive submitted (1.7 MB) Video Info Artifacts Available

Internal and Observational Parametricity for Cubical Agda
Antoine Van Muylder , Andreas Nuyts , and Dominique Devriese 
(KU Leuven, Belgium)

Published Artifact Artifacts Available

Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
Amin Timany , Simon Oddershede Gregersen , Léo Stefanesco , Jonas Kastberg Hinrichsen , Léon Gondelman , Abel Nieto , and Lars Birkedal 
(Aarhus University, Denmark; MPI-SWS, Germany)

Decalf: A Directed, Effectful Cost-Aware Logical Framework
Harrison Grodin , Yue Niu , Jonathan Sterling , and Robert Harper 
(Carnegie Mellon University, USA; University of Cambridge, UK)

Published Artifact

DisLog: A Separation Logic for Disentanglement
Alexandre Moine , Sam Westrick , and Stephanie Balzer 
(Inria, France; Carnegie Mellon University, USA)

Published Artifact Artifacts Available

Modular Denotational Semantics for Effects with Guarded Interaction Trees
Dan Frumin , Amin Timany , and Lars Birkedal 
(University of Groningen, Netherlands; Aarhus University, Denmark)

Enriched Presheaf Model of Quantum FPC
Takeshi Tsukada  and Kazuyuki Asada 
(Chiba University, Japan; Tohoku University, Japan)

Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs
Guannan Wei , Oliver Bračevac , Songlin Jia , Yuyan Bao , and Tiark Rompf 
(Purdue University, USA; Galois, USA; Augusta University, USA)

Nominal Recursors as Epi-Recursors
Andrei Popescu 
(University of Sheffield, UK)

Published Artifact

Optimal Program Synthesis via Abstract Interpretation
Stephen Mell , Steve Zdancewic , and Osbert Bastani 
(University of Pennsylvania, USA)

Published Artifact Artifacts Available

Pipelines and Beyond: Graph Types for ADTs with Futures
Francis Rinaldi , june wunder , Arthur Azevedo de Amorim , and Stefan K. Muller 
(Illinois Institute of Technology, USA; Boston University, USA; Rochester Institute of Technology, USA)

Published Artifact Artifacts Available

Programming-by-Demonstration for Long-Horizon Robot Tasks
Noah Patton , Kia Rahmani , Meghana Missula , Joydeep Biswas , and Işıl Dillig 
(University of Texas, Austin, USA)

Published Artifact Artifacts Available

With a Few Square Roots, Quantum Computing Is as Easy as Pi
Jacques Carette , Chris Heunen , Robin Kaarsgaard , and Amr Sabry 
(McMaster University, Canada; University of Edinburgh, UK; University of Southern Denmark, Denmark; Indiana University, USA)

The Logical Essence of Well-Bracketed Control Flow
Amin Timany , Armaël Guéneau , and Lars Birkedal 
(Aarhus University, Denmark; Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria - Laboratoire Méthodes Formelles, Gif-sur-Yvette, France)

Published Artifact Artifacts Available

An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic
Angus Hammond , Zongyuan Liu , Thibaut Pérami , Peter Sewell , Lars Birkedal , and Jean Pichon-Pharabod 
(University of Cambridge, UK; Aarhus University, Denmark)

Published Artifact

Regular Abstractions for Array Systems
Chih-Duo Hong  and Anthony W. Lin 
(National Chengchi University, Taiwan; University of Kaiserslautern-Landau, Germany; MPI-SWS, Germany)

A Core Calculus for Documents
Will Crichton  and Shriram Krishnamurthi 
(Brown University, USA)

Published Artifact Artifacts Available

The Essence of Generalized Algebraic Data Types
Filip Sieczkowski , Sergei Stepanenko , Jonathan Sterling , and Lars Birkedal 
(Heriot-Watt University, UK; Aarhus University, Denmark; University of Cambridge, UK)

Published Artifact

Solvable Polynomial Ideals: The Ideal Reflection for Program Analysis
John Cyphert  and Zachary Kincaid 
(University of Wisconsin-Madison, USA; Princeton University, USA)

Published Artifact Artifacts Available

Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
Simon Oddershede Gregersen , Alejandro Aguirre , Philipp G. Haselwarter , Joseph Tassarotti , and Lars Birkedal 
(Aarhus University, Denmark; New York University, USA)

Published Artifact Info Artifacts Available

Quotient Haskell: Lightweight Quotient Types for All
Brandon Hewer  and Graham Hutton 
(University of Nottingham, UK)

Semantic Code Refactoring for Abstract Data Types
Shankara Pailoor , Yuepeng Wang , and Işıl Dillig 
(University of Texas, Austin, USA; Simon Fraser University, Canada)

EasyBC: A Cryptography-Specific Language for Security Analysis of Block Ciphers against Differential Cryptanalysis
Pu Sun , Fu Song , Yuqi Chen , and Taolue Chen 
(ShanghaiTech University, China; Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; Birkbeck University of London, UK)

Info

Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs
Julian Müllner , Marcel Moosbrugger , and Laura Kovács 
(TU Wien, Austria)

Coarser Equivalences for Causal Concurrency
Azadeh Farzan  and Umang Mathur 
(University of Toronto, Canada; National University of Singapore, Singapore)

Implementation and Synthesis of Math Library Functions
Ian Briggs , Yash Lad , and Pavel Panchekha 
(University of Utah, USA)

An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification
Neta Elad , Oded Padon , and Sharon Shoham 
(Tel Aviv University, Israel; VMware Research, USA)

Published Artifact Artifacts Available

On Learning Polynomial Recursive Programs
Alex Buna-Marginean , Vincent Cheval , Mahsa Shirmohammadi , and James Worrell 
(University of Oxford, UK; CNRS - IRIF, Paris, France)

Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions
Jianan Yao , Runzhou Tao , Ronghui Gu , and Jason Nieh 
(Columbia University, USA)

Published Artifact Artifacts Available

Efficient CHAD
Tom J. Smeding  and Matthijs I. L. Vákár 
(Utrecht University, Netherlands)

Published Artifact Artifacts Available

Positive Almost-Sure Termination: Complexity and Proof Rules
Rupak Majumdar  and V. R. Sathiyanarayana 
(MPI-SWS, Germany)

Automatic Parallelism Management
Sam Westrick , Matthew Fluet , Mike Rainey , and Umut A. Acar 
(Carnegie Mellon University, USA; Rochester Institute of Technology, USA)

Orthologic with Axioms
Simon Guilloud  and Viktor Kunčak 
(EPFL, Switzerland)

Polymorphic Type Inference for Dynamic Languages
Giuseppe Castagna , Mickaël Laurent , and Kim Nguyen 
(CNRS - Université Paris Cité, France; Université Paris Cité, France; Université Paris-Saclay, France)

Published Artifact Archive submitted (1.1 MB) Artifacts Available

Fusing Direct Manipulations into Functional Programs
Xing Zhang , Ruifeng Xie , Guanchen Guo , Xiao He , Tao Zan , and Zhenjiang Hu 
(Peking University, China; University of Science and Technology Beijing, China; Longyan University, China)

Published Artifact Video Artifacts Available

On-the-Fly Static Analysis via Dynamic Bidirected Dyck Reachability
Shankara Narayanan Krishna , Aniket Lal , Andreas Pavlogiannis , and Omkar Tuppe 
(IIT Bombay, India; Aarhus University, Denmark)

Quantum Bisimilarity via Barbs and Contexts: Curbing the Power of Non-deterministic Observers
Lorenzo Ceragioli , Fabio Gadducci , Giuseppe Lomurno , and Gabriele Tedeschi 
(IMT School for Advanced Studies Lucca, Italy; University of Pisa, Italy)

Internalizing Indistinguishability with Dependent Types
Yiyun Liu , Jonathan Chan , Jessica Shi , and Stephanie Weirich 
(University of Pennsylvania, USA)

Published Artifact Artifacts Available

Polyregular Functions on Unordered Trees of Bounded Height
Mikołaj Bojańczyk  and Bartek Klin 
(University of Warsaw, Poland; University of Oxford, UK)

The Complex(ity) Landscape of Checking Infinite Descent
Liron Cohen , Adham Jabarin , Andrei Popescu , and Reuben N. S. Rowe 
(Ben-Gurion University of the Negev, Israel; University of Sheffield, UK; Royal Holloway University of London, UK)

Published Artifact Archive submitted (300 kB)

Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing
Jules Jacobs , Jonas Kastberg Hinrichsen , and Robbert Krebbers 
(Radboud University Nijmegen, Netherlands; Aarhus University, Denmark)

Published Artifact Artifacts Available

When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class Polymorphism
Lionel Parreaux , Aleksander Boruch-Gruszecki , Andong Fan , and Chun Yin Chau 
(Hong Kong University of Science and Technology, China; EPFL, Switzerland)

Validation of Modern JSON Schema: Formalization and Complexity
Lyes Attouche , Mohamed-Amine Baazizi , Dario Colazzo , Giorgio Ghelli , Carlo Sartiani , and Stefanie Scherzinger 
(Université Paris-Dauphine - PSL, France; Sorbonne University, France; University of Pisa, Italy; University of Basilicata, Italy; University of Passau, Germany)

Published Artifact Artifacts Available

Thunks and Debits in Separation Logic with Time Credits
François Pottier , Armaël Guéneau , Jacques-Henri Jourdan , and Glen Mével 
(Inria, France; Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria - Laboratoire Méthodes Formelles, Gif-sur-Yvette, France; Université Paris-Saclay - CNRS - ENS Paris-Saclay - Laboratoire Méthodes Formelles, Gif-sur-Yvette, France)

Published Artifact Info Artifacts Available

Unboxed Data Constructors: Or, How cpp Decides a Halting Problem
Nicolas Chataing , Stephen Dolan , Gabriel Scherer , and Jeremy Yallop 
(ENS Paris, France; Jane Street, n.n.; Inria, France; University of Cambridge, UK)

Efficient Bottom-Up Synthesis for Programs with Local Variables
Xiang Li , Xiangyu Zhou , Rui Dong , Yihong Zhang , and Xinyu Wang 
(University of Michigan, USA; University of Washington, USA)

Published Artifact Artifacts Available

Disentanglement with Futures, State, and Interaction
Jatin Arora , Stefan K. Muller , and Umut A. Acar 
(Carnegie Mellon University, USA; Illinois Institute of Technology, USA)

Soundly Handling Linearity
Wenhao Tang , Daniel Hillerström , Sam Lindley , and J. Garrett Morris 
(University of Edinburgh, UK; Huawei Zurich Research Center, Switzerland; University of Iowa, USA)

Published Artifact Artifacts Available

Monotonicity and the Precision of Program Analysis
Marco Campion , Mila Dalla Preda , Roberto Giacobazzi , and Caterina Urban 
(Inria - ENS - Université PSL, Paris, France; University of Verona, Italy; University of Arizona, Tucson, USA)

Algebraic Effects Meet Hoare Logic in Cubical Agda
Donnacha Oisín Kidney , Zhixuan Yang , and Nicolas Wu 
(Imperial College London, UK)

Published Artifact Artifacts Available

Solving Infinite-State Games via Acceleration
Philippe Heim  and Rayna Dimitrova 
(CISPA Helmholtz Center for Information Security, Germany)

Published Artifact Artifacts Available

Guided Equality Saturation
Thomas Koehler , Andrés Goens , Siddharth Bhat , Tobias Grosser , Phil Trinder , and Michel Steuwer 
(Inria, France; ICube lab - Université de Strasbourg - CNRS, France; University of Amsterdam, Netherlands; University of Edinburgh, UK; University of Cambridge, UK; University of Glasgow, UK; TU Berlin, Germany)

A Case for Synthesis of Recursive Quantum Unitary Programs
Haowei Deng , Runzhou Tao , Yuxiang Peng , and Xiaodi Wu 
(University of Maryland, College Park, USA; Columbia University, USA; University of Maryland, USA)

Published Artifact Artifacts Available

A Formalization of Core Why3 in Coq
Joshua M. Cohen  and Philip Johnson-Freyd 
(Princeton University, USA; Sandia National Laboratories, USA)

Published Artifact Artifacts Available

Probabilistic Programming Interfaces for Random Graphs: Markov Categories, Graphons, and Nominal Sets
Nate Ackerman , Cameron E. Freer , Younesse Kaddar , Jacek Karwowski , Sean Moss , Daniel Roy , Sam Staton , and Hongseok Yang 
(Harvard University, USA; Massachusetts Institute of Technology, USA; University of Oxford, UK; University of Birmingham, UK; University of Toronto, Canada; KAIST, South Korea)

API-Driven Program Synthesis for Testing Static Typing Implementations
Thodoris Sotiropoulos , Stefanos Chaliasos , and Zhendong Su 
(ETH Zurich, Switzerland; Imperial College London, UK)

Published Artifact Artifacts Available

Inference of Probabilistic Programs with Moment-Matching Gaussian Mixtures
Francesca Randone , Luca Bortolussi , Emilio Incerto , and Mirco Tribastone 
(IMT School for Advanced Studies Lucca, Italy; University of Trieste, Italy)

Published Artifact Artifacts Available

Decision and Complexity of Dolev-Yao Hyperproperties
Itsaka Rakotonirina , Gilles Barthe , and Clara Schneidewind 
(MPI-SP, Germany; IMDEA Software Institute, Spain)

Parikh’s Theorem Made Symbolic
Matthew Hague , Artur Jeż , and Anthony W. Lin 
(Royal Holloway University of London, UK; University of Wrocław, Poland; University of Kaiserslautern-Landau, Germany; MPI-SWS, Germany)

Published Artifact Artifacts Available

How Hard Is Weak-Memory Testing?
Soham Chakraborty , Shankara Narayanan Krishna , Umang Mathur , and Andreas Pavlogiannis 
(TU Delft, Netherlands; IIT Bombay, India; National University of Singapore, Singapore; Aarhus University, Denmark)

Ill-Typed Programs Don’t Evaluate
Steven Ramsay  and Charlie Walpole 
(University of Bristol, UK)

Total Type Error Localization and Recovery with Holes
Eric Zhao , Raef Maroof , Anand Dukkipati , Andrew Blinn , Zhiyi Pan , and Cyrus Omar 
(University of Michigan, USA)

Published Artifact Artifacts Available

VST-A: A Foundationally Sound Annotation Verifier
Litao Zhou , Jianxing Qin , Qinshi Wang , Andrew W. Appel , and Qinxiang Cao 
(Shanghai Jiao Tong University, China; University of Hong Kong, China; Princeton University, USA)

Published Artifact Artifacts Available

Mechanizing Refinement Types
Michael H. Borkowski , Niki Vazou , and Ranjit Jhala 
(University of California, San Diego, USA; IMDEA Software Institute, Spain)

Published Artifact

Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipulations
Yuantian Ding  and Xiaokang Qiu 
(Purdue University, USA)

Published Artifact Artifacts Available

Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules
Ling Zhang , Yuting Wang , Jinhua Wu , Jérémie Koenig , and Zhong Shao 
(Shanghai Jiao Tong University, China; Yale University, USA)

Published Artifact Artifacts Available

Predictive Monitoring against Pattern Regular Languages
Zhendong Ang  and Umang Mathur 
(National University of Singapore, Singapore)

Published Artifact Artifacts Available

Securing Verified IO Programs Against Unverified Code in F*
Cezar-Constantin Andrici , Ștefan Ciobâcă , Cătălin Hriţcu , Guido Martínez , Exequiel Rivas , Éric Tanter , and Théo Winterhalter 
(MPI-SP, Germany; Alexandru Ioan Cuza University, Iași, Romania; Microsoft Research, USA; Tallinn University of Technology, Estonia; University of Chile, Chile; Inria - Saclay, France)

Published Artifact Artifacts Available

ReLU Hull Approximation
Zhongkui Ma , Jiaying Li , and Guangdong Bai 
(University of Queensland, Australia; Microsoft, China)

Polynomial Time and Dependent Types
Robert Atkey 
(University of Strathclyde, UK)

Published Artifact

Generating Well-Typed Terms That Are Not “Useless”
Justin Frank , Benjamin Quiring , and Leonidas Lampropoulos 
(University of Maryland, College Park, USA)

Published Artifact Artifacts Available

Internal Parametricity, without an Interval
Thorsten Altenkirch , Yorgo Chamoun , Ambrus Kaposi , and Michael Shulman 
(University of Nottingham, UK; École Polytechnique, France; Eötvös Loránd University, Hungary; University of San Diego, USA)

Explicit Effects and Effect Constraints in ReML
Martin Elsman 
(University of Copenhagen, Denmark)

Published Artifact Artifacts Available

Indexed Types for a Statically Safe WebAssembly
Adam T. Geller , Justin Frank , and William J. Bowman 
(University of British Columbia, Canada; University of Maryland, USA)

Published Artifact

SimuQ: A Framework for Programming Quantum Hamiltonian Simulation with Analog Compilation
Yuxiang Peng , Jacob Young , Pengyu Liu , and Xiaodi Wu 
(University of Maryland, USA; Carnegie Mellon University, USA)

Published Artifact Info Artifacts Available

A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability
Prasad Jayanti, Siddhartha Jayanti, Ugur Y. Yavuz, and Lizzie Hernandez
(Dartmouth College, USA; Google Research, USA; Boston University, USA; Microsoft, USA)

Published Artifact

Commutativity Simplifies Proofs of Parameterized Programs
Azadeh Farzan , Dominik Klumpp , and Andreas Podelski 
(University of Toronto, Canada; University of Freiburg, Germany)

Published Artifact Artifacts Available

Higher Order Bayesian Networks, Exactly
Claudia Faggian , Daniele Pautasso , and Gabriele Vanoni 
(IRIF - CNRS - Université Paris Cité, France; University of Turin, Italy)

Sound Gradual Verification with Symbolic Execution
Conrad Zimmerman , Jenna DiVincenzo , and Jonathan Aldrich 
(Brown University, USA; Purdue University, USA; Carnegie Mellon University, USA)

Info

Flan: An Expressive and Efficient Datalog Compiler for Program Analysis
Supun Abeysinghe , Anxhelo Xhebraj , and Tiark Rompf 
(Purdue University, USA)

On Model-Checking Higher-Order Effectful Programs
Ugo Dal Lago  and Alexis Ghyselen 
(University of Bologna, Italy; Inria, France)

Effectful Software Contracts
Cameron Moy , Christos Dimoulas , and Matthias Felleisen 
(PLT at Northeastern University, USA; PLT at Northwestern University, USA)

Published Artifact Artifacts Available

Type-Based Gradual Typing Performance Optimization
John Peter Campora , Mohammad Wahiduzzaman Khan , and Sheng Chen 
(Quantinuum, USA; University of Louisiana, Lafayette, USA)

Parametric Subtyping for Structural Parametric Polymorphism
Henry DeYoung , Andreia Mordido , Frank Pfenning , and Ankush Das 
(Carnegie Mellon University, USA; Universidade de Lisboa, Portugal; Amazon, USA)

Published Artifact Info Artifacts Available

Inference of Robust Reachability Constraints
Yanis Sellami , Guillaume Girol , Frédéric Recoules , Damien Couroussé , and Sébastien Bardin 
(Université Grenoble-Alpes - CEA - List, France; Université Paris-Saclay - CEA - List, France)

Published Artifact Artifacts Available

Efficient Matching of Regular Expressions with Lookaround Assertions
Konstantinos Mamouras  and Agnishom Chattopadhyay 
(Rice University, USA)

Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs
Kevin Batz , Tom Jannik Biskup , Joost-Pieter Katoen , and Tobias Winkler 
(RWTH Aachen University, Germany)