POPL 2024 – Author Index

A B C D E F G H I J K L M N O P Q R S T U V W X Y Z

	Abeysinghe, Supun	Proc. ACM Program. Lang., vol. 8, issue POPL: "Flan: An Expressive and Efficient ..." 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
	Acar, Umut A.	Proc. ACM Program. Lang., vol. 8, issue POPL: "Automatic Parallelism Management ..." 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 Proc. ACM Program. Lang., vol. 8, issue POPL: "Disentanglement with Futures, ..." 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
	Ackerman, Nate	Proc. ACM Program. Lang., vol. 8, issue POPL: "Probabilistic Programming ..." 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
	Aguirre, Alejandro	Proc. ACM Program. Lang., vol. 8, issue POPL: "Asynchronous Probabilistic ..." 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
	Aldrich, Jonathan	Proc. ACM Program. Lang., vol. 8, issue POPL: "Sound Gradual Verification ..." 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
	Altenkirch, Thorsten	Proc. ACM Program. Lang., vol. 8, issue POPL: "Internal Parametricity, without ..." 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
	Andrici, Cezar-Constantin	Proc. ACM Program. Lang., vol. 8, issue POPL: "Securing Verified IO Programs ..." 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
	Ang, Zhendong	Proc. ACM Program. Lang., vol. 8, issue POPL: "Predictive Monitoring against ..." 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
	Appel, Andrew W.	Proc. ACM Program. Lang., vol. 8, issue POPL: "VST-A: A Foundationally Sound ..." 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
	Arora, Jatin	Proc. ACM Program. Lang., vol. 8, issue POPL: "Disentanglement with Futures, ..." 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
	Asada, Kazuyuki	Proc. ACM Program. Lang., vol. 8, issue POPL: "Enriched Presheaf Model of ..." 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
	Atkey, Robert	Proc. ACM Program. Lang., vol. 8, issue POPL: "Polynomial Time and Dependent ..." 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
	Attouche, Lyes	Proc. ACM Program. Lang., vol. 8, issue POPL: "Validation of Modern JSON ..." 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
	Azevedo de Amorim, Arthur	Proc. ACM Program. Lang., vol. 8, issue POPL: "Pipelines and Beyond: Graph ..." 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
	Baazizi, Mohamed-Amine	Proc. ACM Program. Lang., vol. 8, issue POPL: "Validation of Modern JSON ..." 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
	Bai, Guangdong	Proc. ACM Program. Lang., vol. 8, issue POPL: "ReLU Hull Approximation ..." 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
	Balasubramanian, A. R.	Proc. ACM Program. Lang., vol. 8, issue POPL: "Reachability in Continuous ..." 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
	Balzer, Stephanie	Proc. ACM Program. Lang., vol. 8, issue POPL: "DisLog: A Separation Logic ..." 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
	Bao, Yuyan	Proc. ACM Program. Lang., vol. 8, issue POPL: "Polymorphic Reachability Types: ..." 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
	Bardin, Sébastien	Proc. ACM Program. Lang., vol. 8, issue POPL: "Inference of Robust Reachability ..." 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
	Barthe, Gilles	Proc. ACM Program. Lang., vol. 8, issue POPL: "Decision and Complexity of ..." 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
	Bastani, Osbert	Proc. ACM Program. Lang., vol. 8, issue POPL: "Optimal Program Synthesis ..." 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
	Batz, Kevin	Proc. ACM Program. Lang., vol. 8, issue POPL: "Programmatic Strategy Synthesis: ..." 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
	Bergsträßer, Pascal	Proc. ACM Program. Lang., vol. 8, issue POPL: "Ramsey Quantifiers in Linear ..." 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
	Bhat, Siddharth	Proc. ACM Program. Lang., vol. 8, issue POPL: "Guided Equality Saturation ..." 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
	Birkedal, Lars	Proc. ACM Program. Lang., vol. 8, issue POPL: "Modular Denotational Semantics ..." 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 Proc. ACM Program. Lang., vol. 8, issue POPL: "The Logical Essence of Well-Bracketed ..." 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 Proc. ACM Program. Lang., vol. 8, issue POPL: "An Axiomatic Basis for Computer ..." 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 Proc. ACM Program. Lang., vol. 8, issue POPL: "The Essence of Generalized ..." 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 Proc. ACM Program. Lang., vol. 8, issue POPL: "Asynchronous Probabilistic ..." 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 Proc. ACM Program. Lang., vol. 8, issue POPL: "Trillium: Higher-Order Concurrent ..." 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
	Biskup, Tom Jannik	Proc. ACM Program. Lang., vol. 8, issue POPL: "Programmatic Strategy Synthesis: ..." 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
	Biswas, Joydeep	Proc. ACM Program. Lang., vol. 8, issue POPL: "Programming-by-Demonstration ..." 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
	Blinn, Andrew	Proc. ACM Program. Lang., vol. 8, issue POPL: "Total Type Error Localization ..." 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
	Bojańczyk, Mikołaj	Proc. ACM Program. Lang., vol. 8, issue POPL: "Polyregular Functions on Unordered ..." 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
	Borkowski, Michael H.	Proc. ACM Program. Lang., vol. 8, issue POPL: "Mechanizing Refinement Types ..." 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
	Bortolussi, Luca	Proc. ACM Program. Lang., vol. 8, issue POPL: "Inference of Probabilistic ..." 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
	Boruch-Gruszecki, Aleksander	Proc. ACM Program. Lang., vol. 8, issue POPL: "When Subtyping Constraints ..." 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
	Bowman, William J.	Proc. ACM Program. Lang., vol. 8, issue POPL: "Indexed Types for a Statically ..." 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
	Bračevac, Oliver	Proc. ACM Program. Lang., vol. 8, issue POPL: "Polymorphic Reachability Types: ..." 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
	Briggs, Ian	Proc. ACM Program. Lang., vol. 8, issue POPL: "Implementation and Synthesis ..." 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
	Buna-Marginean, Alex	Proc. ACM Program. Lang., vol. 8, issue POPL: "On Learning Polynomial Recursive ..." 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
	Campion, Marco	Proc. ACM Program. Lang., vol. 8, issue POPL: "Monotonicity and the Precision ..." 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
	Campora, John Peter	Proc. ACM Program. Lang., vol. 8, issue POPL: "Type-Based Gradual Typing ..." 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
	Cao, Qinxiang	Proc. ACM Program. Lang., vol. 8, issue POPL: "VST-A: A Foundationally Sound ..." 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
	Carette, Jacques	Proc. ACM Program. Lang., vol. 8, issue POPL: "With a Few Square Roots, Quantum ..." 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
	Castagna, Giuseppe	Proc. ACM Program. Lang., vol. 8, issue POPL: "Polymorphic Type Inference ..." 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
	Ceragioli, Lorenzo	Proc. ACM Program. Lang., vol. 8, issue POPL: "Quantum Bisimilarity via Barbs ..." 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
	Chakraborty, Soham	Proc. ACM Program. Lang., vol. 8, issue POPL: "How Hard Is Weak-Memory Testing? ..." 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
	Chaliasos, Stefanos	Proc. ACM Program. Lang., vol. 8, issue POPL: "API-Driven Program Synthesis ..." 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
	Chamoun, Yorgo	Proc. ACM Program. Lang., vol. 8, issue POPL: "Internal Parametricity, without ..." 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
	Chan, Jonathan	Proc. ACM Program. Lang., vol. 8, issue POPL: "Internalizing Indistinguishability ..." 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
	Chataing, Nicolas	Proc. ACM Program. Lang., vol. 8, issue POPL: "Unboxed Data Constructors: ..." 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
	Chattopadhyay, Agnishom	Proc. ACM Program. Lang., vol. 8, issue POPL: "Efficient Matching of Regular ..." 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
	Chau, Chun Yin	Proc. ACM Program. Lang., vol. 8, issue POPL: "When Subtyping Constraints ..." 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
	Chen, Sheng	Proc. ACM Program. Lang., vol. 8, issue POPL: "Type-Based Gradual Typing ..." 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
	Chen, Taolue	Proc. ACM Program. Lang., vol. 8, issue POPL: "EasyBC: A Cryptography-Specific ..." 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
	Chen, Yuqi	Proc. ACM Program. Lang., vol. 8, issue POPL: "EasyBC: A Cryptography-Specific ..." 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
	Cheval, Vincent	Proc. ACM Program. Lang., vol. 8, issue POPL: "On Learning Polynomial Recursive ..." 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
	Ciobâcă, Ștefan	Proc. ACM Program. Lang., vol. 8, issue POPL: "Securing Verified IO Programs ..." 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
	Cohen, Joshua M.	Proc. ACM Program. Lang., vol. 8, issue POPL: "A Formalization of Core Why3 ..." 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
	Cohen, Liron	Proc. ACM Program. Lang., vol. 8, issue POPL: "The Complex(ity) Landscape ..." 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
	Colazzo, Dario	Proc. ACM Program. Lang., vol. 8, issue POPL: "Validation of Modern JSON ..." 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
	Couroussé, Damien	Proc. ACM Program. Lang., vol. 8, issue POPL: "Inference of Robust Reachability ..." 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
	Cousot, Patrick	Proc. ACM Program. Lang., vol. 8, issue POPL: "Calculational Design of [In]Correctness ..." 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
	Crichton, Will	Proc. ACM Program. Lang., vol. 8, issue POPL: "A Core Calculus for Documents: ..." 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
	Cyphert, John	Proc. ACM Program. Lang., vol. 8, issue POPL: "Solvable Polynomial Ideals: ..." 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
	Dal Lago, Ugo	Proc. ACM Program. Lang., vol. 8, issue POPL: "On Model-Checking Higher-Order ..." 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
	Dalla Preda, Mila	Proc. ACM Program. Lang., vol. 8, issue POPL: "Monotonicity and the Precision ..." 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
	Das, Ankush	Proc. ACM Program. Lang., vol. 8, issue POPL: "Parametric Subtyping for Structural ..." 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
	Deng, Haowei	Proc. ACM Program. Lang., vol. 8, issue POPL: "A Case for Synthesis of Recursive ..." 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
	Devriese, Dominique	Proc. ACM Program. Lang., vol. 8, issue POPL: "Internal and Observational ..." 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
	DeYoung, Henry	Proc. ACM Program. Lang., vol. 8, issue POPL: "Parametric Subtyping for Structural ..." 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
	Dillig, Işıl	Proc. ACM Program. Lang., vol. 8, issue POPL: "Programming-by-Demonstration ..." 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 Proc. ACM Program. Lang., vol. 8, issue POPL: "Semantic Code Refactoring ..." 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
	Dimitrova, Rayna	Proc. ACM Program. Lang., vol. 8, issue POPL: "Solving Infinite-State Games ..." 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
	Dimoulas, Christos	Proc. ACM Program. Lang., vol. 8, issue POPL: "Effectful Software Contracts ..." 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
	Ding, Yuantian	Proc. ACM Program. Lang., vol. 8, issue POPL: "Enhanced Enumeration Techniques ..." 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
	DiVincenzo, Jenna	Proc. ACM Program. Lang., vol. 8, issue POPL: "Sound Gradual Verification ..." 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
	Dolan, Stephen	Proc. ACM Program. Lang., vol. 8, issue POPL: "Unboxed Data Constructors: ..." 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
	Dong, Rui	Proc. ACM Program. Lang., vol. 8, issue POPL: "Efficient Bottom-Up Synthesis ..." 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
	Du, Ke	Proc. ACM Program. Lang., vol. 8, issue POPL: "An Iris Instance for Verifying ..." 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
	Dukkipati, Anand	Proc. ACM Program. Lang., vol. 8, issue POPL: "Total Type Error Localization ..." 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
	Elad, Neta	Proc. ACM Program. Lang., vol. 8, issue POPL: "An Infinite Needle in a Finite ..." 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
	Elsman, Martin	Proc. ACM Program. Lang., vol. 8, issue POPL: "Explicit Effects and Effect ..." 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
	Faggian, Claudia	Proc. ACM Program. Lang., vol. 8, issue POPL: "Higher Order Bayesian Networks, ..." 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
	Fan, Andong	Proc. ACM Program. Lang., vol. 8, issue POPL: "When Subtyping Constraints ..." 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
	Farzan, Azadeh	Proc. ACM Program. Lang., vol. 8, issue POPL: "Coarser Equivalences for Causal ..." 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 Proc. ACM Program. Lang., vol. 8, issue POPL: "Commutativity Simplifies Proofs ..." 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
	Felleisen, Matthias	Proc. ACM Program. Lang., vol. 8, issue POPL: "Effectful Software Contracts ..." 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
	Fluet, Matthew	Proc. ACM Program. Lang., vol. 8, issue POPL: "Automatic Parallelism Management ..." 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
	Frank, Justin	Proc. ACM Program. Lang., vol. 8, issue POPL: "Generating Well-Typed Terms ..." 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 Proc. ACM Program. Lang., vol. 8, issue POPL: "Indexed Types for a Statically ..." 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
	Freer, Cameron E.	Proc. ACM Program. Lang., vol. 8, issue POPL: "Probabilistic Programming ..." 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
	Frumin, Dan	Proc. ACM Program. Lang., vol. 8, issue POPL: "Modular Denotational Semantics ..." 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
	Gadducci, Fabio	Proc. ACM Program. Lang., vol. 8, issue POPL: "Quantum Bisimilarity via Barbs ..." 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
	Ganardi, Moses	Proc. ACM Program. Lang., vol. 8, issue POPL: "Ramsey Quantifiers in Linear ..." 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
	Geller, Adam T.	Proc. ACM Program. Lang., vol. 8, issue POPL: "Indexed Types for a Statically ..." 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
	Ghelli, Giorgio	Proc. ACM Program. Lang., vol. 8, issue POPL: "Validation of Modern JSON ..." 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
	Ghyselen, Alexis	Proc. ACM Program. Lang., vol. 8, issue POPL: "On Model-Checking Higher-Order ..." 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
	Giacobazzi, Roberto	Proc. ACM Program. Lang., vol. 8, issue POPL: "Monotonicity and the Precision ..." 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
	Girol, Guillaume	Proc. ACM Program. Lang., vol. 8, issue POPL: "Inference of Robust Reachability ..." 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
	Goens, Andrés	Proc. ACM Program. Lang., vol. 8, issue POPL: "Guided Equality Saturation ..." 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
	Gondelman, Léon	Proc. ACM Program. Lang., vol. 8, issue POPL: "Trillium: Higher-Order Concurrent ..." 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
	Gregersen, Simon Oddershede	Proc. ACM Program. Lang., vol. 8, issue POPL: "Asynchronous Probabilistic ..." 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 Proc. ACM Program. Lang., vol. 8, issue POPL: "Trillium: Higher-Order Concurrent ..." 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
	Grodin, Harrison	Proc. ACM Program. Lang., vol. 8, issue POPL: "Decalf: A Directed, Effectful ..." 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
	Grosser, Tobias	Proc. ACM Program. Lang., vol. 8, issue POPL: "Guided Equality Saturation ..." 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
	Gu, Ronghui	Proc. ACM Program. Lang., vol. 8, issue POPL: "Mostly Automated Verification ..." 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
	Guéneau, Armaël	Proc. ACM Program. Lang., vol. 8, issue POPL: "The Logical Essence of Well-Bracketed ..." 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 Proc. ACM Program. Lang., vol. 8, issue POPL: "Thunks and Debits in Separation ..." 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
	Guilloud, Simon	Proc. ACM Program. Lang., vol. 8, issue POPL: "Orthologic with Axioms ..." 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
	Guo, Guanchen	Proc. ACM Program. Lang., vol. 8, issue POPL: "Fusing Direct Manipulations ..." 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
	Gutsfeld, Jens Oliver	Proc. ACM Program. Lang., vol. 8, issue POPL: "Deciding Asynchronous Hyperproperties ..." 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
	Hague, Matthew	Proc. ACM Program. Lang., vol. 8, issue POPL: "Parikh’s Theorem Made Symbolic ..." 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
	Hammond, Angus	Proc. ACM Program. Lang., vol. 8, issue POPL: "An Axiomatic Basis for Computer ..." 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
	Harper, Robert	Proc. ACM Program. Lang., vol. 8, issue POPL: "Decalf: A Directed, Effectful ..." 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
	Haselwarter, Philipp G.	Proc. ACM Program. Lang., vol. 8, issue POPL: "Asynchronous Probabilistic ..." 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
	He, Xiao	Proc. ACM Program. Lang., vol. 8, issue POPL: "Fusing Direct Manipulations ..." 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
	Heim, Philippe	Proc. ACM Program. Lang., vol. 8, issue POPL: "Solving Infinite-State Games ..." 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
	Hernandez, Lizzie	Proc. ACM Program. Lang., vol. 8, issue POPL: "A Universal, Sound, and Complete ..." 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
	Heunen, Chris	Proc. ACM Program. Lang., vol. 8, issue POPL: "With a Few Square Roots, Quantum ..." 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
	Hewer, Brandon	Proc. ACM Program. Lang., vol. 8, issue POPL: "Quotient Haskell: Lightweight ..." 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
	Hillerström, Daniel	Proc. ACM Program. Lang., vol. 8, issue POPL: "Soundly Handling Linearity ..." 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
	Hinrichsen, Jonas Kastberg	Proc. ACM Program. Lang., vol. 8, issue POPL: "Deadlock-Free Separation Logic: ..." 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 Proc. ACM Program. Lang., vol. 8, issue POPL: "Trillium: Higher-Order Concurrent ..." 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
	Höfner, Peter	Proc. ACM Program. Lang., vol. 8, issue POPL: "Shoggoth: A Formal Foundation ..." 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
	Hong, Chih-Duo	Proc. ACM Program. Lang., vol. 8, issue POPL: "Regular Abstractions for Array ..." 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
	Hriţcu, Cătălin	Proc. ACM Program. Lang., vol. 8, issue POPL: "Securing Verified IO Programs ..." 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
	Hu, Zhenjiang	Proc. ACM Program. Lang., vol. 8, issue POPL: "Fusing Direct Manipulations ..." 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
	Hutton, Graham	Proc. ACM Program. Lang., vol. 8, issue POPL: "Quotient Haskell: Lightweight ..." 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
	Incerto, Emilio	Proc. ACM Program. Lang., vol. 8, issue POPL: "Inference of Probabilistic ..." 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
	Jabarin, Adham	Proc. ACM Program. Lang., vol. 8, issue POPL: "The Complex(ity) Landscape ..." 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
	Jacobs, Jules	Proc. ACM Program. Lang., vol. 8, issue POPL: "Deadlock-Free Separation Logic: ..." 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
	Jayanti, Prasad	Proc. ACM Program. Lang., vol. 8, issue POPL: "A Universal, Sound, and Complete ..." 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
	Jayanti, Siddhartha	Proc. ACM Program. Lang., vol. 8, issue POPL: "A Universal, Sound, and Complete ..." 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
	Jeż, Artur	Proc. ACM Program. Lang., vol. 8, issue POPL: "Parikh’s Theorem Made Symbolic ..." 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
	Jhala, Ranjit	Proc. ACM Program. Lang., vol. 8, issue POPL: "Mechanizing Refinement Types ..." 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
	Jia, Songlin	Proc. ACM Program. Lang., vol. 8, issue POPL: "Polymorphic Reachability Types: ..." 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
	Johnson-Freyd, Philip	Proc. ACM Program. Lang., vol. 8, issue POPL: "A Formalization of Core Why3 ..." 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
	Jourdan, Jacques-Henri	Proc. ACM Program. Lang., vol. 8, issue POPL: "Thunks and Debits in Separation ..." 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
	Kaarsgaard, Robin	Proc. ACM Program. Lang., vol. 8, issue POPL: "With a Few Square Roots, Quantum ..." 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
	Kaddar, Younesse	Proc. ACM Program. Lang., vol. 8, issue POPL: "Probabilistic Programming ..." 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
	Kammar, Ohad	Proc. ACM Program. Lang., vol. 8, issue POPL: "Shoggoth: A Formal Foundation ..." 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
	Kaposi, Ambrus	Proc. ACM Program. Lang., vol. 8, issue POPL: "Internal Parametricity, without ..." 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
	Karwowski, Jacek	Proc. ACM Program. Lang., vol. 8, issue POPL: "Probabilistic Programming ..." 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
	Katoen, Joost-Pieter	Proc. ACM Program. Lang., vol. 8, issue POPL: "Programmatic Strategy Synthesis: ..." 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
	Kawamata, Fuga	Proc. ACM Program. Lang., vol. 8, issue POPL: "Answer Refinement Modification: ..." 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
	Khan, Mohammad Wahiduzzaman	Proc. ACM Program. Lang., vol. 8, issue POPL: "Type-Based Gradual Typing ..." 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
	Kidney, Donnacha Oisín	Proc. ACM Program. Lang., vol. 8, issue POPL: "Algebraic Effects Meet Hoare ..." 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
	Kincaid, Zachary	Proc. ACM Program. Lang., vol. 8, issue POPL: "Solvable Polynomial Ideals: ..." 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
	Klin, Bartek	Proc. ACM Program. Lang., vol. 8, issue POPL: "Polyregular Functions on Unordered ..." 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
	Klumpp, Dominik	Proc. ACM Program. Lang., vol. 8, issue POPL: "Commutativity Simplifies Proofs ..." 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
	Kœhler, Thomas	Proc. ACM Program. Lang., vol. 8, issue POPL: "Guided Equality Saturation ..." 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
	Koenig, Jérémie	Proc. ACM Program. Lang., vol. 8, issue POPL: "Fully Composable and Adequate ..." 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
	Kovács, Laura	Proc. ACM Program. Lang., vol. 8, issue POPL: "Strong Invariants Are Hard: ..." 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
	Krebbers, Robbert	Proc. ACM Program. Lang., vol. 8, issue POPL: "Deadlock-Free Separation Logic: ..." 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
	Krishna, Shankara Narayanan	Proc. ACM Program. Lang., vol. 8, issue POPL: "How Hard Is Weak-Memory Testing? ..." 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
	Krishna, Shankaranarayanan	Proc. ACM Program. Lang., vol. 8, issue POPL: "On-the-Fly Static Analysis ..." 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
	Krishnamurthi, Shriram	Proc. ACM Program. Lang., vol. 8, issue POPL: "A Core Calculus for Documents: ..." 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
	Kunčak, Viktor	Proc. ACM Program. Lang., vol. 8, issue POPL: "Orthologic with Axioms ..." 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
	Lad, Yash	Proc. ACM Program. Lang., vol. 8, issue POPL: "Implementation and Synthesis ..." 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
	Lal, Aniket	Proc. ACM Program. Lang., vol. 8, issue POPL: "On-the-Fly Static Analysis ..." 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
	Lampropoulos, Leonidas	Proc. ACM Program. Lang., vol. 8, issue POPL: "Generating Well-Typed Terms ..." 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
	Laurent, Mickaël	Proc. ACM Program. Lang., vol. 8, issue POPL: "Polymorphic Type Inference ..." 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
	Li, Jiaying	Proc. ACM Program. Lang., vol. 8, issue POPL: "ReLU Hull Approximation ..." 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
	Li, Xiang	Proc. ACM Program. Lang., vol. 8, issue POPL: "Efficient Bottom-Up Synthesis ..." 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
	Lin, Anthony W.	Proc. ACM Program. Lang., vol. 8, issue POPL: "Ramsey Quantifiers in Linear ..." 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 Proc. ACM Program. Lang., vol. 8, issue POPL: "Regular Abstractions for Array ..." 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 Proc. ACM Program. Lang., vol. 8, issue POPL: "Parikh’s Theorem Made Symbolic ..." 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
	Lindley, Sam	Proc. ACM Program. Lang., vol. 8, issue POPL: "Soundly Handling Linearity ..." 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
	Liu, Pengyu	Proc. ACM Program. Lang., vol. 8, issue POPL: "SimuQ: A Framework for Programming ..." 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
	Liu, Yiyun	Proc. ACM Program. Lang., vol. 8, issue POPL: "Internalizing Indistinguishability ..." 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
	Liu, Zongyuan	Proc. ACM Program. Lang., vol. 8, issue POPL: "An Axiomatic Basis for Computer ..." 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
	Lomurno, Giuseppe	Proc. ACM Program. Lang., vol. 8, issue POPL: "Quantum Bisimilarity via Barbs ..." 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
	Ma, Zhongkui	Proc. ACM Program. Lang., vol. 8, issue POPL: "ReLU Hull Approximation ..." 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
	Majumdar, Rupak	Proc. ACM Program. Lang., vol. 8, issue POPL: "Positive Almost-Sure Termination: ..." 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 Proc. ACM Program. Lang., vol. 8, issue POPL: "Reachability in Continuous ..." 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
	Mamouras, Konstantinos	Proc. ACM Program. Lang., vol. 8, issue POPL: "Efficient Matching of Regular ..." 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
	Mansky, William	Proc. ACM Program. Lang., vol. 8, issue POPL: "An Iris Instance for Verifying ..." 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
	Maroof, Raef	Proc. ACM Program. Lang., vol. 8, issue POPL: "Total Type Error Localization ..." 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
	Martínez, Guido	Proc. ACM Program. Lang., vol. 8, issue POPL: "Securing Verified IO Programs ..." 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
	Mathur, Umang	Proc. ACM Program. Lang., vol. 8, issue POPL: "Coarser Equivalences for Causal ..." 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 Proc. ACM Program. Lang., vol. 8, issue POPL: "How Hard Is Weak-Memory Testing? ..." 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 Proc. ACM Program. Lang., vol. 8, issue POPL: "Predictive Monitoring against ..." 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
	Mell, Stephen	Proc. ACM Program. Lang., vol. 8, issue POPL: "Optimal Program Synthesis ..." 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
	Mével, Glen	Proc. ACM Program. Lang., vol. 8, issue POPL: "Thunks and Debits in Separation ..." 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
	Missula, Meghana	Proc. ACM Program. Lang., vol. 8, issue POPL: "Programming-by-Demonstration ..." 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
	Moine, Alexandre	Proc. ACM Program. Lang., vol. 8, issue POPL: "DisLog: A Separation Logic ..." 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
	Moosbrugger, Marcel	Proc. ACM Program. Lang., vol. 8, issue POPL: "Strong Invariants Are Hard: ..." 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
	Mordido, Andreia	Proc. ACM Program. Lang., vol. 8, issue POPL: "Parametric Subtyping for Structural ..." 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
	Morris, J. Garrett	Proc. ACM Program. Lang., vol. 8, issue POPL: "Soundly Handling Linearity ..." 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
	Moss, Sean	Proc. ACM Program. Lang., vol. 8, issue POPL: "Probabilistic Programming ..." 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
	Moy, Cameron	Proc. ACM Program. Lang., vol. 8, issue POPL: "Effectful Software Contracts ..." 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
	Muller, Stefan K.	Proc. ACM Program. Lang., vol. 8, issue POPL: "Pipelines and Beyond: Graph ..." 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 Proc. ACM Program. Lang., vol. 8, issue POPL: "Disentanglement with Futures, ..." 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
	Müller-Olm, Markus	Proc. ACM Program. Lang., vol. 8, issue POPL: "Deciding Asynchronous Hyperproperties ..." 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
	Müllner, Julian	Proc. ACM Program. Lang., vol. 8, issue POPL: "Strong Invariants Are Hard: ..." 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
	Nguyễn, Kim	Proc. ACM Program. Lang., vol. 8, issue POPL: "Polymorphic Type Inference ..." 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
	Nieh, Jason	Proc. ACM Program. Lang., vol. 8, issue POPL: "Mostly Automated Verification ..." 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
	Nieto, Abel	Proc. ACM Program. Lang., vol. 8, issue POPL: "Trillium: Higher-Order Concurrent ..." 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
	Niu, Yue	Proc. ACM Program. Lang., vol. 8, issue POPL: "Decalf: A Directed, Effectful ..." 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
	Nuyts, Andreas	Proc. ACM Program. Lang., vol. 8, issue POPL: "Internal and Observational ..." 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
	O’Connor, Liam	Proc. ACM Program. Lang., vol. 8, issue POPL: "Shoggoth: A Formal Foundation ..." 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
	Ohrem, Christoph	Proc. ACM Program. Lang., vol. 8, issue POPL: "Deciding Asynchronous Hyperproperties ..." 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
	Omar, Cyrus	Proc. ACM Program. Lang., vol. 8, issue POPL: "Total Type Error Localization ..." 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
	Padon, Oded	Proc. ACM Program. Lang., vol. 8, issue POPL: "An Infinite Needle in a Finite ..." 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
	Pailoor, Shankara	Proc. ACM Program. Lang., vol. 8, issue POPL: "Semantic Code Refactoring ..." 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
	Pan, Zhiyi	Proc. ACM Program. Lang., vol. 8, issue POPL: "Total Type Error Localization ..." 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
	Panchekha, Pavel	Proc. ACM Program. Lang., vol. 8, issue POPL: "Implementation and Synthesis ..." 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
	Parreaux, Lionel	Proc. ACM Program. Lang., vol. 8, issue POPL: "When Subtyping Constraints ..." 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
	Patton, Noah	Proc. ACM Program. Lang., vol. 8, issue POPL: "Programming-by-Demonstration ..." 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
	Pautasso, Daniele	Proc. ACM Program. Lang., vol. 8, issue POPL: "Higher Order Bayesian Networks, ..." 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
	Pavlogiannis, Andreas	Proc. ACM Program. Lang., vol. 8, issue POPL: "On-the-Fly Static Analysis ..." 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 Proc. ACM Program. Lang., vol. 8, issue POPL: "How Hard Is Weak-Memory Testing? ..." 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
	Peng, Yuxiang	Proc. ACM Program. Lang., vol. 8, issue POPL: "A Case for Synthesis of Recursive ..." 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 Proc. ACM Program. Lang., vol. 8, issue POPL: "SimuQ: A Framework for Programming ..." 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
	Pérami, Thibaut	Proc. ACM Program. Lang., vol. 8, issue POPL: "An Axiomatic Basis for Computer ..." 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
	Pfenning, Frank	Proc. ACM Program. Lang., vol. 8, issue POPL: "Parametric Subtyping for Structural ..." 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
	Pichon-Pharabod, Jean	Proc. ACM Program. Lang., vol. 8, issue POPL: "An Axiomatic Basis for Computer ..." 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
	Podelski, Andreas	Proc. ACM Program. Lang., vol. 8, issue POPL: "Commutativity Simplifies Proofs ..." 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
	Popescu, Andrei	Proc. ACM Program. Lang., vol. 8, issue POPL: "Nominal Recursors as Epi-Recursors ..." 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 Proc. ACM Program. Lang., vol. 8, issue POPL: "The Complex(ity) Landscape ..." 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
	Pottier, François	Proc. ACM Program. Lang., vol. 8, issue POPL: "Thunks and Debits in Separation ..." 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
	Qin, Jianxing	Proc. ACM Program. Lang., vol. 8, issue POPL: "VST-A: A Foundationally Sound ..." 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
	Qin, Xueying	Proc. ACM Program. Lang., vol. 8, issue POPL: "Shoggoth: A Formal Foundation ..." 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
	Qiu, Xiaokang	Proc. ACM Program. Lang., vol. 8, issue POPL: "Enhanced Enumeration Techniques ..." 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
	Quiring, Benjamin	Proc. ACM Program. Lang., vol. 8, issue POPL: "Generating Well-Typed Terms ..." 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
	Rahmani, Kia	Proc. ACM Program. Lang., vol. 8, issue POPL: "Programming-by-Demonstration ..." 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
	Rainey, Mike	Proc. ACM Program. Lang., vol. 8, issue POPL: "Automatic Parallelism Management ..." 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
	Rakotonirina, Itsaka	Proc. ACM Program. Lang., vol. 8, issue POPL: "Decision and Complexity of ..." 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
	Ramsay, Steven	Proc. ACM Program. Lang., vol. 8, issue POPL: "Ill-Typed Programs Don’t ..." 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
	Randone, Francesca	Proc. ACM Program. Lang., vol. 8, issue POPL: "Inference of Probabilistic ..." 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
	Recoules, Frédéric	Proc. ACM Program. Lang., vol. 8, issue POPL: "Inference of Robust Reachability ..." 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
	Rinaldi, Francis	Proc. ACM Program. Lang., vol. 8, issue POPL: "Pipelines and Beyond: Graph ..." 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
	Rivas, Exequiel	Proc. ACM Program. Lang., vol. 8, issue POPL: "Securing Verified IO Programs ..." 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
	Rompf, Tiark	Proc. ACM Program. Lang., vol. 8, issue POPL: "Polymorphic Reachability Types: ..." 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 Proc. ACM Program. Lang., vol. 8, issue POPL: "Flan: An Expressive and Efficient ..." 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
	Rowe, Reuben N. S.	Proc. ACM Program. Lang., vol. 8, issue POPL: "The Complex(ity) Landscape ..." 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
	Roy, Daniel	Proc. ACM Program. Lang., vol. 8, issue POPL: "Probabilistic Programming ..." 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
	Sabry, Amr	Proc. ACM Program. Lang., vol. 8, issue POPL: "With a Few Square Roots, Quantum ..." 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
	Sartiani, Carlo	Proc. ACM Program. Lang., vol. 8, issue POPL: "Validation of Modern JSON ..." 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
	Sathiyanarayana, V. R.	Proc. ACM Program. Lang., vol. 8, issue POPL: "Positive Almost-Sure Termination: ..." 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
	Scherer, Gabriel	Proc. ACM Program. Lang., vol. 8, issue POPL: "Unboxed Data Constructors: ..." 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
	Scherzinger, Stefanie	Proc. ACM Program. Lang., vol. 8, issue POPL: "Validation of Modern JSON ..." 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
	Schneidewind, Clara	Proc. ACM Program. Lang., vol. 8, issue POPL: "Decision and Complexity of ..." 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
	Sekiyama, Taro	Proc. ACM Program. Lang., vol. 8, issue POPL: "Answer Refinement Modification: ..." 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
	Sellami, Yanis	Proc. ACM Program. Lang., vol. 8, issue POPL: "Inference of Robust Reachability ..." 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
	Sewell, Peter	Proc. ACM Program. Lang., vol. 8, issue POPL: "An Axiomatic Basis for Computer ..." 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
	Shao, Zhong	Proc. ACM Program. Lang., vol. 8, issue POPL: "Fully Composable and Adequate ..." 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
	Shi, Jessica	Proc. ACM Program. Lang., vol. 8, issue POPL: "Internalizing Indistinguishability ..." 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
	Shirmohammadi, Mahsa	Proc. ACM Program. Lang., vol. 8, issue POPL: "On Learning Polynomial Recursive ..." 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
	Shoham, Sharon	Proc. ACM Program. Lang., vol. 8, issue POPL: "An Infinite Needle in a Finite ..." 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
	Shulman, Michael	Proc. ACM Program. Lang., vol. 8, issue POPL: "Internal Parametricity, without ..." 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
	Sieczkowski, Filip	Proc. ACM Program. Lang., vol. 8, issue POPL: "The Essence of Generalized ..." 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
	Smeding, Tom J.	Proc. ACM Program. Lang., vol. 8, issue POPL: "Efficient CHAD ..." 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
	Song, Fu	Proc. ACM Program. Lang., vol. 8, issue POPL: "EasyBC: A Cryptography-Specific ..." 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
	Sotiropoulos, Thodoris	Proc. ACM Program. Lang., vol. 8, issue POPL: "API-Driven Program Synthesis ..." 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
	Staton, Sam	Proc. ACM Program. Lang., vol. 8, issue POPL: "Probabilistic Programming ..." 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
	Stefanesco, Léo	Proc. ACM Program. Lang., vol. 8, issue POPL: "Trillium: Higher-Order Concurrent ..." 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
	Stepanenko, Sergei	Proc. ACM Program. Lang., vol. 8, issue POPL: "The Essence of Generalized ..." 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
	Sterling, Jonathan	Proc. ACM Program. Lang., vol. 8, issue POPL: "Decalf: A Directed, Effectful ..." 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 Proc. ACM Program. Lang., vol. 8, issue POPL: "The Essence of Generalized ..." 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
	Steuwer, Michel	Proc. ACM Program. Lang., vol. 8, issue POPL: "Shoggoth: A Formal Foundation ..." 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 Proc. ACM Program. Lang., vol. 8, issue POPL: "Guided Equality Saturation ..." 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
	Su, Zhendong	Proc. ACM Program. Lang., vol. 8, issue POPL: "API-Driven Program Synthesis ..." 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
	Sun, Pu	Proc. ACM Program. Lang., vol. 8, issue POPL: "EasyBC: A Cryptography-Specific ..." 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
	Tang, Wenhao	Proc. ACM Program. Lang., vol. 8, issue POPL: "Soundly Handling Linearity ..." 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
	Tanter, Éric	Proc. ACM Program. Lang., vol. 8, issue POPL: "Securing Verified IO Programs ..." 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
	Tao, Runzhou	Proc. ACM Program. Lang., vol. 8, issue POPL: "Mostly Automated Verification ..." 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 Proc. ACM Program. Lang., vol. 8, issue POPL: "A Case for Synthesis of Recursive ..." 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
	Tassarotti, Joseph	Proc. ACM Program. Lang., vol. 8, issue POPL: "Asynchronous Probabilistic ..." 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
	Tedeschi, Gabriele	Proc. ACM Program. Lang., vol. 8, issue POPL: "Quantum Bisimilarity via Barbs ..." 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
	Terauchi, Tachio	Proc. ACM Program. Lang., vol. 8, issue POPL: "Answer Refinement Modification: ..." 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
	Thinniyam, Ramanathan S.	Proc. ACM Program. Lang., vol. 8, issue POPL: "Reachability in Continuous ..." 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
	Timany, Amin	Proc. ACM Program. Lang., vol. 8, issue POPL: "Modular Denotational Semantics ..." 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 Proc. ACM Program. Lang., vol. 8, issue POPL: "The Logical Essence of Well-Bracketed ..." 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 Proc. ACM Program. Lang., vol. 8, issue POPL: "Trillium: Higher-Order Concurrent ..." 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
	Tribastone, Mirco	Proc. ACM Program. Lang., vol. 8, issue POPL: "Inference of Probabilistic ..." 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
	Trinder, Phil	Proc. ACM Program. Lang., vol. 8, issue POPL: "Guided Equality Saturation ..." 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
	Tsukada, Takeshi	Proc. ACM Program. Lang., vol. 8, issue POPL: "Enriched Presheaf Model of ..." 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
	Tuppe, Omkar	Proc. ACM Program. Lang., vol. 8, issue POPL: "On-the-Fly Static Analysis ..." 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
	Unno, Hiroshi	Proc. ACM Program. Lang., vol. 8, issue POPL: "Answer Refinement Modification: ..." 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
	Urban, Caterina	Proc. ACM Program. Lang., vol. 8, issue POPL: "Monotonicity and the Precision ..." 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
	Vákár, Matthijs I. L.	Proc. ACM Program. Lang., vol. 8, issue POPL: "Efficient CHAD ..." 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
	Van Glabbeek, Rob	Proc. ACM Program. Lang., vol. 8, issue POPL: "Shoggoth: A Formal Foundation ..." 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
	Van Muylder, Antoine	Proc. ACM Program. Lang., vol. 8, issue POPL: "Internal and Observational ..." 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
	Vanoni, Gabriele	Proc. ACM Program. Lang., vol. 8, issue POPL: "Higher Order Bayesian Networks, ..." 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
	Vazou, Niki	Proc. ACM Program. Lang., vol. 8, issue POPL: "Mechanizing Refinement Types ..." 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
	Walpole, Charlie	Proc. ACM Program. Lang., vol. 8, issue POPL: "Ill-Typed Programs Don’t ..." 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
	Wang, Qinshi	Proc. ACM Program. Lang., vol. 8, issue POPL: "VST-A: A Foundationally Sound ..." 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
	Wang, Xinyu	Proc. ACM Program. Lang., vol. 8, issue POPL: "Efficient Bottom-Up Synthesis ..." 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
	Wang, Yuepeng	Proc. ACM Program. Lang., vol. 8, issue POPL: "Semantic Code Refactoring ..." 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
	Wang, Yuting	Proc. ACM Program. Lang., vol. 8, issue POPL: "Fully Composable and Adequate ..." 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
	Wei, Guannan	Proc. ACM Program. Lang., vol. 8, issue POPL: "Polymorphic Reachability Types: ..." 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
	Weirich, Stephanie	Proc. ACM Program. Lang., vol. 8, issue POPL: "Internalizing Indistinguishability ..." 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
	Westrick, Sam	Proc. ACM Program. Lang., vol. 8, issue POPL: "DisLog: A Separation Logic ..." 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 Proc. ACM Program. Lang., vol. 8, issue POPL: "Automatic Parallelism Management ..." 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
	Winkler, Tobias	Proc. ACM Program. Lang., vol. 8, issue POPL: "Programmatic Strategy Synthesis: ..." 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
	Winterhalter, Théo	Proc. ACM Program. Lang., vol. 8, issue POPL: "Securing Verified IO Programs ..." 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
	Worrell, James	Proc. ACM Program. Lang., vol. 8, issue POPL: "On Learning Polynomial Recursive ..." 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
	Wu, Jinhua	Proc. ACM Program. Lang., vol. 8, issue POPL: "Fully Composable and Adequate ..." 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
	Wu, Nicolas	Proc. ACM Program. Lang., vol. 8, issue POPL: "Algebraic Effects Meet Hoare ..." 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
	Wu, Xiaodi	Proc. ACM Program. Lang., vol. 8, issue POPL: "A Case for Synthesis of Recursive ..." 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 Proc. ACM Program. Lang., vol. 8, issue POPL: "SimuQ: A Framework for Programming ..." 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
	Wunder, june	Proc. ACM Program. Lang., vol. 8, issue POPL: "Pipelines and Beyond: Graph ..." 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
	Xhebraj, Anxhelo	Proc. ACM Program. Lang., vol. 8, issue POPL: "Flan: An Expressive and Efficient ..." 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
	Xie, Ruifeng	Proc. ACM Program. Lang., vol. 8, issue POPL: "Fusing Direct Manipulations ..." 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
	Yallop, Jeremy	Proc. ACM Program. Lang., vol. 8, issue POPL: "Unboxed Data Constructors: ..." 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
	Yang, Hongseok	Proc. ACM Program. Lang., vol. 8, issue POPL: "Probabilistic Programming ..." 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
	Yang, Zhixuan	Proc. ACM Program. Lang., vol. 8, issue POPL: "Algebraic Effects Meet Hoare ..." 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
	Yao, Jianan	Proc. ACM Program. Lang., vol. 8, issue POPL: "Mostly Automated Verification ..." 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
	Yavuz, Ugur Y.	Proc. ACM Program. Lang., vol. 8, issue POPL: "A Universal, Sound, and Complete ..." 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
	Young, Jacob	Proc. ACM Program. Lang., vol. 8, issue POPL: "SimuQ: A Framework for Programming ..." 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
	Zan, Tao	Proc. ACM Program. Lang., vol. 8, issue POPL: "Fusing Direct Manipulations ..." 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
	Zdancewic, Steve	Proc. ACM Program. Lang., vol. 8, issue POPL: "Optimal Program Synthesis ..." 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
	Zetzsche, Georg	Proc. ACM Program. Lang., vol. 8, issue POPL: "Ramsey Quantifiers in Linear ..." 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 Proc. ACM Program. Lang., vol. 8, issue POPL: "Reachability in Continuous ..." 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
	Zhang, Ling	Proc. ACM Program. Lang., vol. 8, issue POPL: "Fully Composable and Adequate ..." 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
	Zhang, Xing	Proc. ACM Program. Lang., vol. 8, issue POPL: "Fusing Direct Manipulations ..." 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
	Zhang, Yihong	Proc. ACM Program. Lang., vol. 8, issue POPL: "Efficient Bottom-Up Synthesis ..." 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
	Zhao, Eric	Proc. ACM Program. Lang., vol. 8, issue POPL: "Total Type Error Localization ..." 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
	Zhou, Litao	Proc. ACM Program. Lang., vol. 8, issue POPL: "VST-A: A Foundationally Sound ..." 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
	Zhou, Xiangyu	Proc. ACM Program. Lang., vol. 8, issue POPL: "Efficient Bottom-Up Synthesis ..." 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
	Zimmerman, Conrad	Proc. ACM Program. Lang., vol. 8, issue POPL: "Sound Gradual Verification ..." 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