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

Title Page

Article: popl24foreword-fm000-p (type: Frontmatter) doi:

Editorial Message

Article: popl24foreword-fm001-p (type: Frontmatter) doi:

POPL 2024 Sponsors and Supporters

Article: popl24foreword-fm003-p (type: Frontmatter) doi:

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

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p3-p (type: Full Paper) doi:10.1145/3632843

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

Publisher's Version Article: popl24main-p10-p (type: Full Paper) doi:10.1145/3632844

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)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p17-p (type: Full Paper) doi:10.1145/3633211

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

Publisher's Version Article: popl24main-p18-p (type: Full Paper) doi:10.1145/3633279

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)

Publisher's Version Artifacts Reusable Article: popl24main-p20-p (type: Full Paper) doi:10.1145/3633280

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

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p41-p (type: Full Paper) doi:10.1145/3632848

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

Publisher's Version Archive submitted (1.7 MB) Article: popl24main-p43-p (type: Full Paper) doi:10.1145/3632849

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

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p48-p (type: Full Paper) doi:10.1145/3632850

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)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p52-p (type: Full Paper) doi:10.1145/3632851

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)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p54-p (type: Full Paper) doi:10.1145/3632852

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

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p55-p (type: Full Paper) doi:10.1145/3632853

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

Publisher's Version Artifacts Reusable Article: popl24main-p66-p (type: Full Paper) doi:10.1145/3632854

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

Publisher's Version Article: popl24main-p70-p (type: Full Paper) doi:10.1145/3632855

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)

Publisher's Version Article: popl24main-p73-p (type: Full Paper) doi:10.1145/3632856

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

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p76-p (type: Full Paper) doi:10.1145/3632857

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

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p80-p (type: Full Paper) doi:10.1145/3632858

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)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p82-p (type: Full Paper) doi:10.1145/3632859

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)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p83-p (type: Full Paper) doi:10.1145/3632860

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)

Publisher's Version Article: popl24main-p89-p (type: Full Paper) doi:10.1145/3632861

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 - LMF, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p92-p (type: Full Paper) doi:10.1145/3632862

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)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p98-p (type: Full Paper) doi:10.1145/3632863

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

Publisher's Version Article: popl24main-p99-p (type: Full Paper) doi:10.1145/3632864

A Core Calculus for Documents: Or, Lambda: The Ultimate Document
Will Crichton and Shriram Krishnamurthi
(Brown University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p107-p (type: Full Paper) doi:10.1145/3632865

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)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p110-p (type: Full Paper) doi:10.1145/3632866

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

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p122-p (type: Full Paper) doi:10.1145/3632867

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)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p129-p (type: Full Paper) doi:10.1145/3632868

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

Publisher's Version Article: popl24main-p136-p (type: Full Paper) doi:10.1145/3632869

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

Publisher's Version Article: popl24main-p145-p (type: Full Paper) doi:10.1145/3632870

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)

Publisher's Version Article: popl24main-p146-p (type: Full Paper) doi:10.1145/3632871

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)

Publisher's Version Article: popl24main-p151-p (type: Full Paper) doi:10.1145/3632872

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

Publisher's Version Article: popl24main-p160-p (type: Full Paper) doi:10.1145/3632873

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

Publisher's Version Article: popl24main-p164-p (type: Full Paper) doi:10.1145/3632874

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)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p166-p (type: Full Paper) doi:10.1145/3632875

Corrigendum: Corrigendum to "An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification" by Elad et al., Proceedings of the ACM on Programming Languages, Volume 8, Issue POPL (PACMPL 8:POPL).

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

Publisher's Version Article: popl24main-p168-p (type: Full Paper) doi:10.1145/3632876

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

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p170-p (type: Full Paper) doi:10.1145/3632877

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

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p178-p (type: Full Paper) doi:10.1145/3632878

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

Publisher's Version Article: popl24main-p180-p (type: Full Paper) doi:10.1145/3632879

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

Publisher's Version Article: popl24main-p181-p (type: Full Paper) doi:10.1145/3632880

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

Publisher's Version Article: popl24main-p183-p (type: Full Paper) doi:10.1145/3632881

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

Publisher's Version Published Artifact Archive submitted (1.1 MB) Artifacts Available Artifacts Reusable Article: popl24main-p201-p (type: Full Paper) doi:10.1145/3632882

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)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p213-p (type: Full Paper) doi:10.1145/3632883

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

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p214-p (type: Full Paper) doi:10.1145/3632884

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)

Publisher's Version Article: popl24main-p216-p (type: Full Paper) doi:10.1145/3632885

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

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p229-p (type: Full Paper) doi:10.1145/3632886

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

Publisher's Version Article: popl24main-p231-p (type: Full Paper) doi:10.1145/3632887

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)

Publisher's Version Published Artifact Archive submitted (300 kB) Artifacts Available Artifacts Reusable Article: popl24main-p233-p (type: Full Paper) doi:10.1145/3632888

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)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p234-p (type: Full Paper) doi:10.1145/3632889

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, Hong Kong; EPFL, Switzerland)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p237-p (type: Full Paper) doi:10.1145/3632890

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)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl24main-p241-p (type: Full Paper) doi:10.1145/3632891

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 - LMF, France; Université Paris-Saclay - CNRS - ENS Paris-Saclay - LMF, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p245-p (type: Full Paper) doi:10.1145/3632892

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

Publisher's Version Article: popl24main-p252-p (type: Full Paper) doi:10.1145/3632893

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)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p254-p (type: Full Paper) doi:10.1145/3632894

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

Publisher's Version Article: popl24main-p260-p (type: Full Paper) doi:10.1145/3632895

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)

Publisher's Version Published Artifact Archive submitted (1.5 MB) Artifacts Available Artifacts Reusable Article: popl24main-p261-p (type: Full Paper) doi:10.1145/3632896

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)

Publisher's Version Article: popl24main-p262-p (type: Full Paper) doi:10.1145/3632897

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

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p271-p (type: Full Paper) doi:10.1145/3632898

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

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p273-p (type: Full Paper) doi:10.1145/3632899

Guided Equality Saturation
Thomas Kœhler, 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)

Publisher's Version Archive submitted (150 kB) Article: popl24main-p274-p (type: Full Paper) doi:10.1145/3632900

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)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p282-p (type: Full Paper) doi:10.1145/3632901

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

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p283-p (type: Full Paper) doi:10.1145/3632902

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)

Publisher's Version Article: popl24main-p293-p (type: Full Paper) doi:10.1145/3632903

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

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p302-p (type: Full Paper) doi:10.1145/3632904

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)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p312-p (type: Full Paper) doi:10.1145/3632905

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

Publisher's Version Article: popl24main-p331-p (type: Full Paper) doi:10.1145/3632906

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)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl24main-p332-p (type: Full Paper) doi:10.1145/3632907

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)

Publisher's Version Article: popl24main-p333-p (type: Full Paper) doi:10.1145/3632908

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

Publisher's Version Article: popl24main-p334-p (type: Full Paper) doi:10.1145/3632909

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)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p336-p (type: Full Paper) doi:10.1145/3632910

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)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p348-p (type: Full Paper) doi:10.1145/3632911

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

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p349-p (type: Full Paper) doi:10.1145/3632912

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

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p375-p (type: Full Paper) doi:10.1145/3632913

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)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p380-p (type: Full Paper) doi:10.1145/3632914

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

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p382-p (type: Full Paper) doi:10.1145/3632915

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, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p385-p (type: Full Paper) doi:10.1145/3632916

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

Publisher's Version Article: popl24main-p441-p (type: Full Paper) doi:10.1145/3632917

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

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl24main-p453-p (type: Full Paper) doi:10.1145/3632918

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

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p476-p (type: Full Paper) doi:10.1145/3632919

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)

Publisher's Version Article: popl24main-p508-p (type: Full Paper) doi:10.1145/3632920

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

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p536-p (type: Full Paper) doi:10.1145/3632921

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)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl24main-p538-p (type: Full Paper) doi:10.1145/3632922

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)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p544-p (type: Full Paper) doi:10.1145/3632923

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)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p557-p (type: Full Paper) doi:10.1145/3632924

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

Publisher's Version Published Artifact Artifacts Available Article: popl24main-p579-p (type: Full Paper) doi:10.1145/3632925

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

Publisher's Version Article: popl24main-p582-p (type: Full Paper) doi:10.1145/3632926

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

Publisher's Version Article: popl24main-p589-p (type: Full Paper) doi:10.1145/3632927

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

Publisher's Version Article: popl24main-p634-p (type: Full Paper) doi:10.1145/3632928

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

Publisher's Version Article: popl24main-p635-p (type: Full Paper) doi:10.1145/3632929

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

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p642-p (type: Full Paper) doi:10.1145/3632930

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

Publisher's Version Article: popl24main-p713-p (type: Full Paper) doi:10.1145/3632931

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)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p714-p (type: Full Paper) doi:10.1145/3632932

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)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl24main-p717-p (type: Full Paper) doi:10.1145/3632933

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

Publisher's Version Article: popl24main-p758-p (type: Full Paper) doi:10.1145/3632934

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

Publisher's Version Article: popl24main-p766-p (type: Full Paper) doi:10.1145/3632935