POPL 2022 – Author Index

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

	Aiken, Alex	Proc. ACM Program. Lang., vol. 6, issue POPL: "Induction Duality: Primal-Dual ..." Induction Duality: Primal-Dual Search for Invariants Oded Padon, James R. Wilcox, Jason R. Koenig, Kenneth L. McMillan, and Alex Aiken (VMware Research, USA; Stanford University, USA; Certora, USA; University of Texas at Austin, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Functional
	Albarghouthi, Aws	Proc. ACM Program. Lang., vol. 6, issue POPL: "Interval Universal Approximation ..." Interval Universal Approximation for Neural Networks Zi Wang, Aws Albarghouthi, Gautam Prakriya, and Somesh Jha (University of Wisconsin-Madison, USA; Chinese University of Hong Kong, China; University of Wisconsin, USA) Publisher's Version Archive submitted (830 kB)
	Amin, Nada	Proc. ACM Program. Lang., vol. 6, issue POPL: "Reasoning about “Reasoning ..." Reasoning about “Reasoning about Reasoning”: Semantics and Contextual Equivalence for Probabilistic Programs with Nested Queries and Recursion Yizhou Zhang and Nada Amin (University of Waterloo, Canada; Harvard University, USA) Publisher's Version
	Balzer, Stephanie	Proc. ACM Program. Lang., vol. 6, issue POPL: "Connectivity Graphs: A Method ..." Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation Logic Jules Jacobs, Stephanie Balzer, and Robbert Krebbers (Radboud University Nijmegen, Netherlands; Carnegie Mellon University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Bao, Jialu	Proc. ACM Program. Lang., vol. 6, issue POPL: "A Separation Logic for Negative ..." A Separation Logic for Negative Dependence Jialu Bao, Marco Gaboardi, Justin Hsu, and Joseph Tassarotti (Cornell University, USA; Boston University, USA; Boston College, USA) Publisher's Version
	Batty, Mark	Proc. ACM Program. Lang., vol. 6, issue POPL: "The Leaky Semicolon: Compositional ..." The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Concurrency Alan Jeffrey, James Riely, Mark Batty, Simon Cooksey, Ilya Kaysin, and Anton Podkopaev (Roblox, USA; DePaul University, USA; University of Kent, UK; JetBrains Research, Russia; University of Cambridge, UK; HSE University, Russia) Publisher's Version Published Artifact Artifacts Available
	Baumann, Pascal	Proc. ACM Program. Lang., vol. 6, issue POPL: "Context-Bounded Verification ..." Context-Bounded Verification of Thread Pools Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche (MPI-SWS, Germany) Publisher's Version
	Berdine, Josh	Proc. ACM Program. Lang., vol. 6, issue POPL: "Concurrent Incorrectness Separation ..." Concurrent Incorrectness Separation Logic Azalea Raad, Josh Berdine, Derek Dreyer, and Peter W. O'Hearn (Imperial College London, UK; Meta, UK; MPI-SWS, Germany; University College London, UK) Publisher's Version
	Bernstein, Gilbert Louis	Proc. ACM Program. Lang., vol. 6, issue POPL: "Verified Tensor-Program Optimization ..." Verified Tensor-Program Optimization Via High-Level Scheduling Rewrites Amanda Liu, Gilbert Louis Bernstein, Adam Chlipala, and Jonathan Ragan-Kelley (Massachusetts Institute of Technology, USA; University of California at Berkeley, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Blanvillain, Olivier	Proc. ACM Program. Lang., vol. 6, issue POPL: "Type-Level Programming with ..." Type-Level Programming with Match Types Olivier Blanvillain, Jonathan Immanuel Brachthäuser, Maxime Kjaer, and Martin Odersky (EPFL, Switzerland; University of Tübingen, Germany) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Brachthäuser, Jonathan Immanuel	Proc. ACM Program. Lang., vol. 6, issue POPL: "Type-Level Programming with ..." Type-Level Programming with Match Types Olivier Blanvillain, Jonathan Immanuel Brachthäuser, Maxime Kjaer, and Martin Odersky (EPFL, Switzerland; University of Tübingen, Germany) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Brendel, Ana	Proc. ACM Program. Lang., vol. 6, issue POPL: "Bottom-Up Synthesis of Recursive ..." Bottom-Up Synthesis of Recursive Functional Programs using Angelic Execution Anders Miltner, Adrian Trejo Nuñez, Ana Brendel, Swarat Chaudhuri, and Isil Dillig (University of Texas at Austin, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Campbell, Eric Hayden	Proc. ACM Program. Lang., vol. 6, issue POPL: "Dependently-Typed Data Plane ..." Dependently-Typed Data Plane Programming Matthias Eichholz, Eric Hayden Campbell, Matthias Krebs, Nate Foster, and Mira Mezini (TU Darmstadt, Germany; Cornell University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Functional
	Campion, Marco	Proc. ACM Program. Lang., vol. 6, issue POPL: "Partial (In)Completeness in ..." Partial (In)Completeness in Abstract Interpretation: Limiting the Imprecision in Program Analysis Marco Campion, Mila Dalla Preda, and Roberto Giacobazzi (University of Verona, Italy) Publisher's Version
	Carbin, Michael	Proc. ACM Program. Lang., vol. 6, issue POPL: "Twist: Sound Reasoning for ..." Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs Charles Yuan, Christopher McNally, and Michael Carbin (Massachusetts Institute of Technology, USA) Publisher's Version Published Artifact Archive submitted (690 kB) Artifacts Available Artifacts Reusable
	Castagna, Giuseppe	Proc. ACM Program. Lang., vol. 6, issue POPL: "On Type-Cases, Union Elimination, ..." On Type-Cases, Union Elimination, and Occurrence Typing Giuseppe Castagna, Mickaël Laurent, Kim Nguyễn, and Matthew Lutze (CNRS, France; Université de Paris, France; Université Paris-Saclay, France) Publisher's Version Published Artifact Archive submitted (1.1 MB) Artifacts Available Artifacts Reusable
	Chaudhuri, Swarat	Proc. ACM Program. Lang., vol. 6, issue POPL: "Bottom-Up Synthesis of Recursive ..." Bottom-Up Synthesis of Recursive Functional Programs using Angelic Execution Anders Miltner, Adrian Trejo Nuñez, Ana Brendel, Swarat Chaudhuri, and Isil Dillig (University of Texas at Austin, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Chen, Taolue	Proc. ACM Program. Lang., vol. 6, issue POPL: "Solving String Constraints ..." Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables Taolue Chen, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu (Birkbeck University of London, UK; Royal Holloway University of London, UK; Tsinghua University, China; Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; TU Kaiserslautern, Germany; MPI-SWS, Germany; Uppsala University, Sweden) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Chistikov, Dmitry	Proc. ACM Program. Lang., vol. 6, issue POPL: "Subcubic Certificates for ..." Subcubic Certificates for CFL Reachability Dmitry Chistikov, Rupak Majumdar, and Philipp Schepper (University of Warwick, UK; MPI-SWS, Germany; CISPA, Germany) Publisher's Version
	Chlipala, Adam	Proc. ACM Program. Lang., vol. 6, issue POPL: "Certifying Derivation of State ..." Certifying Derivation of State Machines from Coroutines Mirai Ikebuchi, Andres Erbsen, and Adam Chlipala (National Institute of Informatics, Japan; Massachusetts Institute of Technology, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Proc. ACM Program. Lang., vol. 6, issue POPL: "Verified Tensor-Program Optimization ..." Verified Tensor-Program Optimization Via High-Level Scheduling Rewrites Amanda Liu, Gilbert Louis Bernstein, Adam Chlipala, and Jonathan Ragan-Kelley (Massachusetts Institute of Technology, USA; University of California at Berkeley, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Choudhury, Vikraman	Proc. ACM Program. Lang., vol. 6, issue POPL: "Symmetries in Reversible Programming: ..." Symmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible Programming Languages Vikraman Choudhury, Jacek Karwowski, and Amr Sabry (Indiana University, USA; University of Cambridge, UK; University of Warsaw, Poland) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Ciccone, Luca	Proc. ACM Program. Lang., vol. 6, issue POPL: "Fair Termination of Binary ..." Fair Termination of Binary Sessions Luca Ciccone and Luca Padovani (University of Turin, Italy) Publisher's Version Published Artifact Archive submitted (600 kB) Artifacts Available Artifacts Reusable
	Cooksey, Simon	Proc. ACM Program. Lang., vol. 6, issue POPL: "The Leaky Semicolon: Compositional ..." The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Concurrency Alan Jeffrey, James Riely, Mark Batty, Simon Cooksey, Ilya Kaysin, and Anton Podkopaev (Roblox, USA; DePaul University, USA; University of Kent, UK; JetBrains Research, Russia; University of Cambridge, UK; HSE University, Russia) Publisher's Version Published Artifact Artifacts Available
	Dal Lago, Ugo	Proc. ACM Program. Lang., vol. 6, issue POPL: "Effectful Program Distancing ..." Effectful Program Distancing Ugo Dal Lago and Francesco Gavazzo (University of Bologna, Italy; Inria, France) Publisher's Version Proc. ACM Program. Lang., vol. 6, issue POPL: "A Relational Theory of Effects ..." A Relational Theory of Effects and Coeffects Ugo Dal Lago and Francesco Gavazzo (University of Bologna, Italy; Inria, France) Publisher's Version
	Dalla Preda, Mila	Proc. ACM Program. Lang., vol. 6, issue POPL: "Partial (In)Completeness in ..." Partial (In)Completeness in Abstract Interpretation: Limiting the Imprecision in Program Analysis Marco Campion, Mila Dalla Preda, and Roberto Giacobazzi (University of Verona, Italy) Publisher's Version
	Dang, Hoang-Hai	Proc. ACM Program. Lang., vol. 6, issue POPL: "Simuliris: A Separation Logic ..." Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, and Derek Dreyer (MPI-SWS, Germany; Radboud University Nijmegen, Netherlands; KAIST, South Korea) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	De Amorim, Arthur Azevedo	Proc. ACM Program. Lang., vol. 6, issue POPL: "On Incorrectness Logic and ..." On Incorrectness Logic and Kleene Algebra with Top and Tests Cheng Zhang, Arthur Azevedo de Amorim, and Marco Gaboardi (Boston University, USA) Publisher's Version
	Delaware, Benjamin	Proc. ACM Program. Lang., vol. 6, issue POPL: "Oblivious Algebraic Data Types ..." Oblivious Algebraic Data Types Qianchuan Ye and Benjamin Delaware (Purdue University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Dillig, Isil	Proc. ACM Program. Lang., vol. 6, issue POPL: "Bottom-Up Synthesis of Recursive ..." Bottom-Up Synthesis of Recursive Functional Programs using Angelic Execution Anders Miltner, Adrian Trejo Nuñez, Ana Brendel, Swarat Chaudhuri, and Isil Dillig (University of Texas at Austin, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Proc. ACM Program. Lang., vol. 6, issue POPL: "SolType: Refinement Types ..." SolType: Refinement Types for Arithmetic Overflow in Solidity Bryan Tan, Benjamin Mariano, Shuvendu K. Lahiri, Isil Dillig, and Yu Feng (University of California at Santa Barbara, USA; University of Texas at Austin, USA; Microsoft Research, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Dreyer, Derek	Proc. ACM Program. Lang., vol. 6, issue POPL: "VIP: Verifying Real-World ..." VIP: Verifying Real-World C Idioms with Integer-Pointer Casts Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, and Peter Sewell (MPI-SWS, Germany; University of Cambridge, UK; Radboud University Nijmegen, Netherlands) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Proc. ACM Program. Lang., vol. 6, issue POPL: "Simuliris: A Separation Logic ..." Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, and Derek Dreyer (MPI-SWS, Germany; Radboud University Nijmegen, Netherlands; KAIST, South Korea) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Proc. ACM Program. Lang., vol. 6, issue POPL: "Concurrent Incorrectness Separation ..." Concurrent Incorrectness Separation Logic Azalea Raad, Josh Berdine, Derek Dreyer, and Peter W. O'Hearn (Imperial College London, UK; Meta, UK; MPI-SWS, Germany; University College London, UK) Publisher's Version
	Eichholz, Matthias	Proc. ACM Program. Lang., vol. 6, issue POPL: "Dependently-Typed Data Plane ..." Dependently-Typed Data Plane Programming Matthias Eichholz, Eric Hayden Campbell, Matthias Krebs, Nate Foster, and Mira Mezini (TU Darmstadt, Germany; Cornell University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Functional
	Eisenberg, Richard A.	Proc. ACM Program. Lang., vol. 6, issue POPL: "Provably Correct, Asymptotically ..." Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic Differentiation Faustyna Krawiec, Simon Peyton Jones, Neel Krishnaswami, Tom Ellis, Richard A. Eisenberg, and Andrew Fitzgibbon (University of Cambridge, UK; Microsoft Research, UK; Tweag, France) Publisher's Version
	Ellis, Tom	Proc. ACM Program. Lang., vol. 6, issue POPL: "Provably Correct, Asymptotically ..." Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic Differentiation Faustyna Krawiec, Simon Peyton Jones, Neel Krishnaswami, Tom Ellis, Richard A. Eisenberg, and Andrew Fitzgibbon (University of Cambridge, UK; Microsoft Research, UK; Tweag, France) Publisher's Version
	Erbsen, Andres	Proc. ACM Program. Lang., vol. 6, issue POPL: "Certifying Derivation of State ..." Certifying Derivation of State Machines from Coroutines Mirai Ikebuchi, Andres Erbsen, and Adam Chlipala (National Institute of Informatics, Japan; Massachusetts Institute of Technology, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Feldman, Yotam M. Y.	Proc. ACM Program. Lang., vol. 6, issue POPL: "Property-Directed Reachability ..." Property-Directed Reachability as Abstract Interpretation in the Monotone Theory Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, and James R. Wilcox (Tel Aviv University, Israel; Certora, USA) Publisher's Version
	Feng, Yu	Proc. ACM Program. Lang., vol. 6, issue POPL: "SolType: Refinement Types ..." SolType: Refinement Types for Arithmetic Overflow in Solidity Bryan Tan, Benjamin Mariano, Shuvendu K. Lahiri, Isil Dillig, and Yu Feng (University of California at Santa Barbara, USA; University of Texas at Austin, USA; Microsoft Research, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Fiore, Marcelo	Proc. ACM Program. Lang., vol. 6, issue POPL: "Formal Metatheory of Second-Order ..." Formal Metatheory of Second-Order Abstract Syntax Marcelo Fiore and Dmitrij Szamozvancev (University of Cambridge, UK) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Fitzgibbon, Andrew	Proc. ACM Program. Lang., vol. 6, issue POPL: "Provably Correct, Asymptotically ..." Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic Differentiation Faustyna Krawiec, Simon Peyton Jones, Neel Krishnaswami, Tom Ellis, Richard A. Eisenberg, and Andrew Fitzgibbon (University of Cambridge, UK; Microsoft Research, UK; Tweag, France) Publisher's Version
	Flores-Lamas, Alejandro	Proc. ACM Program. Lang., vol. 6, issue POPL: "Solving String Constraints ..." Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables Taolue Chen, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu (Birkbeck University of London, UK; Royal Holloway University of London, UK; Tsinghua University, China; Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; TU Kaiserslautern, Germany; MPI-SWS, Germany; Uppsala University, Sweden) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Foster, Nate	Proc. ACM Program. Lang., vol. 6, issue POPL: "Dependently-Typed Data Plane ..." Dependently-Typed Data Plane Programming Matthias Eichholz, Eric Hayden Campbell, Matthias Krebs, Nate Foster, and Mira Mezini (TU Darmstadt, Germany; Cornell University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Functional
	Gaboardi, Marco	Proc. ACM Program. Lang., vol. 6, issue POPL: "On Incorrectness Logic and ..." On Incorrectness Logic and Kleene Algebra with Top and Tests Cheng Zhang, Arthur Azevedo de Amorim, and Marco Gaboardi (Boston University, USA) Publisher's Version Proc. ACM Program. Lang., vol. 6, issue POPL: "A Separation Logic for Negative ..." A Separation Logic for Negative Dependence Jialu Bao, Marco Gaboardi, Justin Hsu, and Joseph Tassarotti (Cornell University, USA; Boston University, USA; Boston College, USA) Publisher's Version
	Gäher, Lennard	Proc. ACM Program. Lang., vol. 6, issue POPL: "Simuliris: A Separation Logic ..." Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, and Derek Dreyer (MPI-SWS, Germany; Radboud University Nijmegen, Netherlands; KAIST, South Korea) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Garg, Deepak	Proc. ACM Program. Lang., vol. 6, issue POPL: "Pirouette: Higher-Order Typed ..." Pirouette: Higher-Order Typed Functional Choreographies Andrew K. Hirsch and Deepak Garg (MPI-SWS, Germany) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Proc. ACM Program. Lang., vol. 6, issue POPL: "Isolation without Taxation: ..." Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFI Matthew Kolosick, Shravan Narayan, Evan Johnson, Conrad Watt, Michael LeMay, Deepak Garg, Ranjit Jhala, and Deian Stefan (University of California at San Diego, USA; University of Cambridge, UK; Intel Labs, USA; MPI-SWS, Germany) Publisher's Version
	Gavazzo, Francesco	Proc. ACM Program. Lang., vol. 6, issue POPL: "Effectful Program Distancing ..." Effectful Program Distancing Ugo Dal Lago and Francesco Gavazzo (University of Bologna, Italy; Inria, France) Publisher's Version Proc. ACM Program. Lang., vol. 6, issue POPL: "A Relational Theory of Effects ..." A Relational Theory of Effects and Coeffects Ugo Dal Lago and Francesco Gavazzo (University of Bologna, Italy; Inria, France) Publisher's Version
	Gélineau, Samuel	Proc. ACM Program. Lang., vol. 6, issue POPL: "Mœbius: Metaprogramming using ..." Mœbius: Metaprogramming using Contextual Types: The Stage Where System F Can Pattern Match on Itself Junyoung Jang, Samuel Gélineau, Stefan Monnier, and Brigitte Pientka (McGill University, Canada; SimSpace, Canada; Université de Montréal, Canada) Publisher's Version
	Giacobazzi, Roberto	Proc. ACM Program. Lang., vol. 6, issue POPL: "Partial (In)Completeness in ..." Partial (In)Completeness in Abstract Interpretation: Limiting the Imprecision in Program Analysis Marco Campion, Mila Dalla Preda, and Roberto Giacobazzi (University of Verona, Italy) Publisher's Version
	Gladstein, Vladimir	Proc. ACM Program. Lang., vol. 6, issue POPL: "Truly Stateless, Optimal Dynamic ..." Truly Stateless, Optimal Dynamic Partial Order Reduction Michalis Kokologiannakis, Iason Marmanis, Vladimir Gladstein, and Viktor Vafeiadis (MPI-SWS, Germany; St. Petersburg University, Russia; JetBrains Research, Russia) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Grodin, Harrison	Proc. ACM Program. Lang., vol. 6, issue POPL: "A Cost-Aware Logical Framework ..." A Cost-Aware Logical Framework Yue Niu, Jonathan Sterling, Harrison Grodin, and Robert Harper (Carnegie Mellon University, USA; Aarhus University, Denmark) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Gurfinkel, Arie	Proc. ACM Program. Lang., vol. 6, issue POPL: "Solving Constrained Horn Clauses ..." Solving Constrained Horn Clauses Modulo Algebraic Data Types and Recursive Functions Hari Govind V K, Sharon Shoham, and Arie Gurfinkel (University of Waterloo, Canada; Tel Aviv University, Israel) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Hague, Matthew	Proc. ACM Program. Lang., vol. 6, issue POPL: "Solving String Constraints ..." Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables Taolue Chen, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu (Birkbeck University of London, UK; Royal Holloway University of London, UK; Tsinghua University, China; Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; TU Kaiserslautern, Germany; MPI-SWS, Germany; Uppsala University, Sweden) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Han, Zhilei	Proc. ACM Program. Lang., vol. 6, issue POPL: "Solving String Constraints ..." Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables Taolue Chen, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu (Birkbeck University of London, UK; Royal Holloway University of London, UK; Tsinghua University, China; Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; TU Kaiserslautern, Germany; MPI-SWS, Germany; Uppsala University, Sweden) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Harper, Robert	Proc. ACM Program. Lang., vol. 6, issue POPL: "A Cost-Aware Logical Framework ..." A Cost-Aware Logical Framework Yue Niu, Jonathan Sterling, Harrison Grodin, and Robert Harper (Carnegie Mellon University, USA; Aarhus University, Denmark) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	He, Wenlei	Proc. ACM Program. Lang., vol. 6, issue POPL: "Profile Inference Revisited ..." Profile Inference Revisited Wenlei He, Julián Mestre, Sergey Pupyrev, Lei Wang, and Hongtao Yu (Facebook, USA; University of Sydney, Australia) Publisher's Version
	Heunen, Chris	Proc. ACM Program. Lang., vol. 6, issue POPL: "Quantum Information Effects ..." Quantum Information Effects Chris Heunen and Robin Kaarsgaard (University of Edinburgh, UK) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Hirsch, Andrew K.	Proc. ACM Program. Lang., vol. 6, issue POPL: "Pirouette: Higher-Order Typed ..." Pirouette: Higher-Order Typed Functional Choreographies Andrew K. Hirsch and Deepak Garg (MPI-SWS, Germany) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Hou (Favonia), Kuen-Bang	Proc. ACM Program. Lang., vol. 6, issue POPL: "Logarithm and Program Testing ..." Logarithm and Program Testing Kuen-Bang Hou (Favonia) and Zhuyang Wang (University of Minnesota, USA) Publisher's Version Published Artifact Archive submitted (540 kB) Artifacts Available Artifacts Reusable
	Hsu, Justin	Proc. ACM Program. Lang., vol. 6, issue POPL: "A Separation Logic for Negative ..." A Separation Logic for Negative Dependence Jialu Bao, Marco Gaboardi, Justin Hsu, and Joseph Tassarotti (Cornell University, USA; Boston University, USA; Boston College, USA) Publisher's Version
	Hu, Denghang	Proc. ACM Program. Lang., vol. 6, issue POPL: "Solving String Constraints ..." Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables Taolue Chen, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu (Birkbeck University of London, UK; Royal Holloway University of London, UK; Tsinghua University, China; Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; TU Kaiserslautern, Germany; MPI-SWS, Germany; Uppsala University, Sweden) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Ikebuchi, Mirai	Proc. ACM Program. Lang., vol. 6, issue POPL: "Certifying Derivation of State ..." Certifying Derivation of State Machines from Coroutines Mirai Ikebuchi, Andres Erbsen, and Adam Chlipala (National Institute of Informatics, Japan; Massachusetts Institute of Technology, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Jacobs, Jules	Proc. ACM Program. Lang., vol. 6, issue POPL: "Connectivity Graphs: A Method ..." Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation Logic Jules Jacobs, Stephanie Balzer, and Robbert Krebbers (Radboud University Nijmegen, Netherlands; Carnegie Mellon University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Jang, Junyoung	Proc. ACM Program. Lang., vol. 6, issue POPL: "Mœbius: Metaprogramming using ..." Mœbius: Metaprogramming using Contextual Types: The Stage Where System F Can Pattern Match on Itself Junyoung Jang, Samuel Gélineau, Stefan Monnier, and Brigitte Pientka (McGill University, Canada; SimSpace, Canada; Université de Montréal, Canada) Publisher's Version
	Jeffrey, Alan	Proc. ACM Program. Lang., vol. 6, issue POPL: "The Leaky Semicolon: Compositional ..." The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Concurrency Alan Jeffrey, James Riely, Mark Batty, Simon Cooksey, Ilya Kaysin, and Anton Podkopaev (Roblox, USA; DePaul University, USA; University of Kent, UK; JetBrains Research, Russia; University of Cambridge, UK; HSE University, Russia) Publisher's Version Published Artifact Artifacts Available
	Jeon, Minseok	Proc. ACM Program. Lang., vol. 6, issue POPL: "Return of CFA: Call-Site Sensitivity ..." Return of CFA: Call-Site Sensitivity Can Be Superior to Object Sensitivity Even for Object-Oriented Programs Minseok Jeon and Hakjoo Oh (Korea University, South Korea) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Jha, Somesh	Proc. ACM Program. Lang., vol. 6, issue POPL: "Interval Universal Approximation ..." Interval Universal Approximation for Neural Networks Zi Wang, Aws Albarghouthi, Gautam Prakriya, and Somesh Jha (University of Wisconsin-Madison, USA; Chinese University of Hong Kong, China; University of Wisconsin, USA) Publisher's Version Archive submitted (830 kB)
	Jhala, Ranjit	Proc. ACM Program. Lang., vol. 6, issue POPL: "Isolation without Taxation: ..." Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFI Matthew Kolosick, Shravan Narayan, Evan Johnson, Conrad Watt, Michael LeMay, Deepak Garg, Ranjit Jhala, and Deian Stefan (University of California at San Diego, USA; University of Cambridge, UK; Intel Labs, USA; MPI-SWS, Germany) Publisher's Version
	Jia, Xiaodong	Proc. ACM Program. Lang., vol. 6, issue POPL: "Semantics for Variational ..." Semantics for Variational Quantum Programming Xiaodong Jia, Andre Kornell, Bert Lindenhovius, Michael Mislove, and Vladimir Zamdzhiev (Hunan University, China; Tulane University, USA; JKU Linz, Austria; Inria, France) Publisher's Version
	Johnson, Evan	Proc. ACM Program. Lang., vol. 6, issue POPL: "Isolation without Taxation: ..." Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFI Matthew Kolosick, Shravan Narayan, Evan Johnson, Conrad Watt, Michael LeMay, Deepak Garg, Ranjit Jhala, and Deian Stefan (University of California at San Diego, USA; University of Cambridge, UK; Intel Labs, USA; MPI-SWS, Germany) Publisher's Version
	Jung, Ralf	Proc. ACM Program. Lang., vol. 6, issue POPL: "Simuliris: A Separation Logic ..." Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, and Derek Dreyer (MPI-SWS, Germany; Radboud University Nijmegen, Netherlands; KAIST, South Korea) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	K, Hari Govind V	Proc. ACM Program. Lang., vol. 6, issue POPL: "Solving Constrained Horn Clauses ..." Solving Constrained Horn Clauses Modulo Algebraic Data Types and Recursive Functions Hari Govind V K, Sharon Shoham, and Arie Gurfinkel (University of Waterloo, Canada; Tel Aviv University, Israel) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Kaarsgaard, Robin	Proc. ACM Program. Lang., vol. 6, issue POPL: "Quantum Information Effects ..." Quantum Information Effects Chris Heunen and Robin Kaarsgaard (University of Edinburgh, UK) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Kammar, Ohad	Proc. ACM Program. Lang., vol. 6, issue POPL: "Fully Abstract Models for ..." Fully Abstract Models for Effectful λ-Calculi via Category-Theoretic Logical Relations Ohad Kammar, Shin-ya Katsumata, and Philip Saville (University of Edinburgh, UK; National Institute of Informatics, Japan; University of Oxford, UK) Publisher's Version
	Kan, Shuanglong	Proc. ACM Program. Lang., vol. 6, issue POPL: "Solving String Constraints ..." Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables Taolue Chen, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu (Birkbeck University of London, UK; Royal Holloway University of London, UK; Tsinghua University, China; Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; TU Kaiserslautern, Germany; MPI-SWS, Germany; Uppsala University, Sweden) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Kang, Jeehoon	Proc. ACM Program. Lang., vol. 6, issue POPL: "Simuliris: A Separation Logic ..." Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, and Derek Dreyer (MPI-SWS, Germany; Radboud University Nijmegen, Netherlands; KAIST, South Korea) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Karimov, Toghrul	Proc. ACM Program. Lang., vol. 6, issue POPL: "What’s Decidable about Linear ..." What’s Decidable about Linear Loops? Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, David Purser, Anton Varonka, Markus A. Whiteland, and James Worrell (MPI-SWS, Germany; University of Oxford, UK) Publisher's Version
	Karwowski, Jacek	Proc. ACM Program. Lang., vol. 6, issue POPL: "Symmetries in Reversible Programming: ..." Symmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible Programming Languages Vikraman Choudhury, Jacek Karwowski, and Amr Sabry (Indiana University, USA; University of Cambridge, UK; University of Warsaw, Poland) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Katsumata, Shin-ya	Proc. ACM Program. Lang., vol. 6, issue POPL: "Fully Abstract Models for ..." Fully Abstract Models for Effectful λ-Calculi via Category-Theoretic Logical Relations Ohad Kammar, Shin-ya Katsumata, and Philip Saville (University of Edinburgh, UK; National Institute of Informatics, Japan; University of Oxford, UK) Publisher's Version
	Kaysin, Ilya	Proc. ACM Program. Lang., vol. 6, issue POPL: "The Leaky Semicolon: Compositional ..." The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Concurrency Alan Jeffrey, James Riely, Mark Batty, Simon Cooksey, Ilya Kaysin, and Anton Podkopaev (Roblox, USA; DePaul University, USA; University of Kent, UK; JetBrains Research, Russia; University of Cambridge, UK; HSE University, Russia) Publisher's Version Published Artifact Artifacts Available
	Kesner, Delia	Proc. ACM Program. Lang., vol. 6, issue POPL: "A Fine-Grained Computational ..." A Fine-Grained Computational Interpretation of Girard’s Intuitionistic Proof-Nets Delia Kesner (Université de Paris, France; CNRS, France; IRIF, France; Institut Universitaire de France, France) Publisher's Version
	Kjaer, Maxime	Proc. ACM Program. Lang., vol. 6, issue POPL: "Type-Level Programming with ..." Type-Level Programming with Match Types Olivier Blanvillain, Jonathan Immanuel Brachthäuser, Maxime Kjaer, and Martin Odersky (EPFL, Switzerland; University of Tübingen, Germany) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Kjelstrøm, Adam Husted	Proc. ACM Program. Lang., vol. 6, issue POPL: "The Decidability and Complexity ..." The Decidability and Complexity of Interleaved Bidirected Dyck Reachability Adam Husted Kjelstrøm and Andreas Pavlogiannis (Aarhus University, Denmark) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Koenig, Jason R.	Proc. ACM Program. Lang., vol. 6, issue POPL: "Induction Duality: Primal-Dual ..." Induction Duality: Primal-Dual Search for Invariants Oded Padon, James R. Wilcox, Jason R. Koenig, Kenneth L. McMillan, and Alex Aiken (VMware Research, USA; Stanford University, USA; Certora, USA; University of Texas at Austin, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Functional
	Koenig, Jérémie	Proc. ACM Program. Lang., vol. 6, issue POPL: "Verified Compilation of C ..." Verified Compilation of C Programs with a Nominal Memory Model Yuting Wang, Ling Zhang, Zhong Shao, and Jérémie Koenig (Shanghai Jiao Tong University, China; Yale University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Proc. ACM Program. Lang., vol. 6, issue POPL: "Layered and Object-Based Game ..." Layered and Object-Based Game Semantics Arthur Oliveira Vale, Paul-André Melliès, Zhong Shao, Jérémie Koenig, and Léo Stefanesco (Yale University, USA; CNRS, France; Université de Paris, France; MPI-SWS, Germany) Publisher's Version
	Kokologiannakis, Michalis	Proc. ACM Program. Lang., vol. 6, issue POPL: "Truly Stateless, Optimal Dynamic ..." Truly Stateless, Optimal Dynamic Partial Order Reduction Michalis Kokologiannakis, Iason Marmanis, Vladimir Gladstein, and Viktor Vafeiadis (MPI-SWS, Germany; St. Petersburg University, Russia; JetBrains Research, Russia) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Kolosick, Matthew	Proc. ACM Program. Lang., vol. 6, issue POPL: "Isolation without Taxation: ..." Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFI Matthew Kolosick, Shravan Narayan, Evan Johnson, Conrad Watt, Michael LeMay, Deepak Garg, Ranjit Jhala, and Deian Stefan (University of California at San Diego, USA; University of Cambridge, UK; Intel Labs, USA; MPI-SWS, Germany) Publisher's Version
	Kornell, Andre	Proc. ACM Program. Lang., vol. 6, issue POPL: "Semantics for Variational ..." Semantics for Variational Quantum Programming Xiaodong Jia, Andre Kornell, Bert Lindenhovius, Michael Mislove, and Vladimir Zamdzhiev (Hunan University, China; Tulane University, USA; JKU Linz, Austria; Inria, France) Publisher's Version
	Krawiec, Faustyna	Proc. ACM Program. Lang., vol. 6, issue POPL: "Provably Correct, Asymptotically ..." Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic Differentiation Faustyna Krawiec, Simon Peyton Jones, Neel Krishnaswami, Tom Ellis, Richard A. Eisenberg, and Andrew Fitzgibbon (University of Cambridge, UK; Microsoft Research, UK; Tweag, France) Publisher's Version
	Krebbers, Robbert	Proc. ACM Program. Lang., vol. 6, issue POPL: "Connectivity Graphs: A Method ..." Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation Logic Jules Jacobs, Stephanie Balzer, and Robbert Krebbers (Radboud University Nijmegen, Netherlands; Carnegie Mellon University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Proc. ACM Program. Lang., vol. 6, issue POPL: "VIP: Verifying Real-World ..." VIP: Verifying Real-World C Idioms with Integer-Pointer Casts Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, and Peter Sewell (MPI-SWS, Germany; University of Cambridge, UK; Radboud University Nijmegen, Netherlands) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Proc. ACM Program. Lang., vol. 6, issue POPL: "Simuliris: A Separation Logic ..." Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, and Derek Dreyer (MPI-SWS, Germany; Radboud University Nijmegen, Netherlands; KAIST, South Korea) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Krebs, Matthias	Proc. ACM Program. Lang., vol. 6, issue POPL: "Dependently-Typed Data Plane ..." Dependently-Typed Data Plane Programming Matthias Eichholz, Eric Hayden Campbell, Matthias Krebs, Nate Foster, and Mira Mezini (TU Darmstadt, Germany; Cornell University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Functional
	Krishnaswami, Neel	Proc. ACM Program. Lang., vol. 6, issue POPL: "Provably Correct, Asymptotically ..." Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic Differentiation Faustyna Krawiec, Simon Peyton Jones, Neel Krishnaswami, Tom Ellis, Richard A. Eisenberg, and Andrew Fitzgibbon (University of Cambridge, UK; Microsoft Research, UK; Tweag, France) Publisher's Version
	Krogmeier, Paul	Proc. ACM Program. Lang., vol. 6, issue POPL: "Learning Formulas in Finite ..." Learning Formulas in Finite Variable Logics Paul Krogmeier and P. Madhusudan (University of Illinois at Urbana-Champaign, USA) Publisher's Version
	Lahiri, Shuvendu K.	Proc. ACM Program. Lang., vol. 6, issue POPL: "SolType: Refinement Types ..." SolType: Refinement Types for Arithmetic Overflow in Solidity Bryan Tan, Benjamin Mariano, Shuvendu K. Lahiri, Isil Dillig, and Yu Feng (University of California at Santa Barbara, USA; University of Texas at Austin, USA; Microsoft Research, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Laurel, Jacob	Proc. ACM Program. Lang., vol. 6, issue POPL: "A Dual Number Abstraction ..." A Dual Number Abstraction for Static Analysis of Clarke Jacobians Jacob Laurel, Rem Yang, Gagandeep Singh, and Sasa Misailovic (University of Illinois at Urbana-Champaign, USA; VMware, USA) Publisher's Version
	Laurent, Mickaël	Proc. ACM Program. Lang., vol. 6, issue POPL: "On Type-Cases, Union Elimination, ..." On Type-Cases, Union Elimination, and Occurrence Typing Giuseppe Castagna, Mickaël Laurent, Kim Nguyễn, and Matthew Lutze (CNRS, France; Université de Paris, France; Université Paris-Saclay, France) Publisher's Version Published Artifact Archive submitted (1.1 MB) Artifacts Available Artifacts Reusable
	Le, Xuan-Bach	Proc. ACM Program. Lang., vol. 6, issue POPL: "A Quantum Interpretation of ..." A Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantum Programs Based on Separation Logic Xuan-Bach Le, Shang-Wei Lin, Jun Sun, and David Sanan (Nanyang Technological University, Singapore; Singapore Management University, Singapore) Publisher's Version
	Lefaucheux, Engel	Proc. ACM Program. Lang., vol. 6, issue POPL: "What’s Decidable about Linear ..." What’s Decidable about Linear Loops? Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, David Purser, Anton Varonka, Markus A. Whiteland, and James Worrell (MPI-SWS, Germany; University of Oxford, UK) Publisher's Version
	LeMay, Michael	Proc. ACM Program. Lang., vol. 6, issue POPL: "Isolation without Taxation: ..." Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFI Matthew Kolosick, Shravan Narayan, Evan Johnson, Conrad Watt, Michael LeMay, Deepak Garg, Ranjit Jhala, and Deian Stefan (University of California at San Diego, USA; University of Cambridge, UK; Intel Labs, USA; MPI-SWS, Germany) Publisher's Version
	Lepigre, Rodolphe	Proc. ACM Program. Lang., vol. 6, issue POPL: "VIP: Verifying Real-World ..." VIP: Verifying Real-World C Idioms with Integer-Pointer Casts Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, and Peter Sewell (MPI-SWS, Germany; University of Cambridge, UK; Radboud University Nijmegen, Netherlands) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Li, Yuanbo	Proc. ACM Program. Lang., vol. 6, issue POPL: "Efficient Algorithms for Dynamic ..." Efficient Algorithms for Dynamic Bidirected Dyck-Reachability Yuanbo Li, Kris Satya, and Qirun Zhang (Georgia Institute of Technology, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Lim, Jay P.	Proc. ACM Program. Lang., vol. 6, issue POPL: "One Polynomial Approximation ..." One Polynomial Approximation to Produce Correctly Rounded Results of an Elementary Function for Multiple Representations and Rounding Modes Jay P. Lim and Santosh Nagarakatte (Rutgers University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Lin, Anthony W.	Proc. ACM Program. Lang., vol. 6, issue POPL: "Solving String Constraints ..." Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables Taolue Chen, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu (Birkbeck University of London, UK; Royal Holloway University of London, UK; Tsinghua University, China; Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; TU Kaiserslautern, Germany; MPI-SWS, Germany; Uppsala University, Sweden) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Lin, Shang-Wei	Proc. ACM Program. Lang., vol. 6, issue POPL: "A Quantum Interpretation of ..." A Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantum Programs Based on Separation Logic Xuan-Bach Le, Shang-Wei Lin, Jun Sun, and David Sanan (Nanyang Technological University, Singapore; Singapore Management University, Singapore) Publisher's Version
	Lindenhovius, Bert	Proc. ACM Program. Lang., vol. 6, issue POPL: "Semantics for Variational ..." Semantics for Variational Quantum Programming Xiaodong Jia, Andre Kornell, Bert Lindenhovius, Michael Mislove, and Vladimir Zamdzhiev (Hunan University, China; Tulane University, USA; JKU Linz, Austria; Inria, France) Publisher's Version
	Liu, Amanda	Proc. ACM Program. Lang., vol. 6, issue POPL: "Verified Tensor-Program Optimization ..." Verified Tensor-Program Optimization Via High-Level Scheduling Rewrites Amanda Liu, Gilbert Louis Bernstein, Adam Chlipala, and Jonathan Ragan-Kelley (Massachusetts Institute of Technology, USA; University of California at Berkeley, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Loehr, Devon	Proc. ACM Program. Lang., vol. 6, issue POPL: "Safe, Modular Packet Pipeline ..." Safe, Modular Packet Pipeline Programming Devon Loehr and David Walker (Princeton University, USA) Publisher's Version Published Artifact Archive submitted (760 kB) Artifacts Available Artifacts Reusable
	Löh, Andres	Proc. ACM Program. Lang., vol. 6, issue POPL: "Staging with Class: A Specification ..." Staging with Class: A Specification for Typed Template Haskell Ningning Xie, Matthew Pickering, Andres Löh, Nicolas Wu, Jeremy Yallop, and Meng Wang (University of Cambridge, UK; Well-Typed LLP, UK; Imperial College London, UK; University of Bristol, UK) Publisher's Version
	Lutze, Matthew	Proc. ACM Program. Lang., vol. 6, issue POPL: "On Type-Cases, Union Elimination, ..." On Type-Cases, Union Elimination, and Occurrence Typing Giuseppe Castagna, Mickaël Laurent, Kim Nguyễn, and Matthew Lutze (CNRS, France; Université de Paris, France; Université Paris-Saclay, France) Publisher's Version Published Artifact Archive submitted (1.1 MB) Artifacts Available Artifacts Reusable
	Madhusudan, P.	Proc. ACM Program. Lang., vol. 6, issue POPL: "Learning Formulas in Finite ..." Learning Formulas in Finite Variable Logics Paul Krogmeier and P. Madhusudan (University of Illinois at Urbana-Champaign, USA) Publisher's Version
	Madiot, Jean-Marie	Proc. ACM Program. Lang., vol. 6, issue POPL: "A Separation Logic for Heap ..." A Separation Logic for Heap Space under Garbage Collection Jean-Marie Madiot and François Pottier (Inria, France) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Majumdar, Rupak	Proc. ACM Program. Lang., vol. 6, issue POPL: "Context-Bounded Verification ..." Context-Bounded Verification of Thread Pools Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche (MPI-SWS, Germany) Publisher's Version Proc. ACM Program. Lang., vol. 6, issue POPL: "Subcubic Certificates for ..." Subcubic Certificates for CFL Reachability Dmitry Chistikov, Rupak Majumdar, and Philipp Schepper (University of Warwick, UK; MPI-SWS, Germany; CISPA, Germany) Publisher's Version
	Makarchuk, Gleb	Proc. ACM Program. Lang., vol. 6, issue POPL: "PRIMA: General and Precise ..." PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations Mark Niklas Müller, Gleb Makarchuk, Gagandeep Singh, Markus Püschel, and Martin Vechev (ETH Zurich, Switzerland; VMware Research, USA; University of Illinois at Urbana-Champaign, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Maranget, Luc	Proc. ACM Program. Lang., vol. 6, issue POPL: "Extending Intel-x86 Consistency ..." Extending Intel-x86 Consistency and Persistency: Formalising the Semantics of Intel-x86 Memory Types and Non-temporal Stores Azalea Raad, Luc Maranget, and Viktor Vafeiadis (Imperial College London, UK; Inria, France; MPI-SWS, Germany) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Mariano, Benjamin	Proc. ACM Program. Lang., vol. 6, issue POPL: "SolType: Refinement Types ..." SolType: Refinement Types for Arithmetic Overflow in Solidity Bryan Tan, Benjamin Mariano, Shuvendu K. Lahiri, Isil Dillig, and Yu Feng (University of California at Santa Barbara, USA; University of Texas at Austin, USA; Microsoft Research, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Marmanis, Iason	Proc. ACM Program. Lang., vol. 6, issue POPL: "Truly Stateless, Optimal Dynamic ..." Truly Stateless, Optimal Dynamic Partial Order Reduction Michalis Kokologiannakis, Iason Marmanis, Vladimir Gladstein, and Viktor Vafeiadis (MPI-SWS, Germany; St. Petersburg University, Russia; JetBrains Research, Russia) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	McMillan, Kenneth L.	Proc. ACM Program. Lang., vol. 6, issue POPL: "Induction Duality: Primal-Dual ..." Induction Duality: Primal-Dual Search for Invariants Oded Padon, James R. Wilcox, Jason R. Koenig, Kenneth L. McMillan, and Alex Aiken (VMware Research, USA; Stanford University, USA; Certora, USA; University of Texas at Austin, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Functional
	McNally, Christopher	Proc. ACM Program. Lang., vol. 6, issue POPL: "Twist: Sound Reasoning for ..." Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs Charles Yuan, Christopher McNally, and Michael Carbin (Massachusetts Institute of Technology, USA) Publisher's Version Published Artifact Archive submitted (690 kB) Artifacts Available Artifacts Reusable
	Melliès, Paul-André	Proc. ACM Program. Lang., vol. 6, issue POPL: "Layered and Object-Based Game ..." Layered and Object-Based Game Semantics Arthur Oliveira Vale, Paul-André Melliès, Zhong Shao, Jérémie Koenig, and Léo Stefanesco (Yale University, USA; CNRS, France; Université de Paris, France; MPI-SWS, Germany) Publisher's Version
	Memarian, Kayvan	Proc. ACM Program. Lang., vol. 6, issue POPL: "VIP: Verifying Real-World ..." VIP: Verifying Real-World C Idioms with Integer-Pointer Casts Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, and Peter Sewell (MPI-SWS, Germany; University of Cambridge, UK; Radboud University Nijmegen, Netherlands) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Mestre, Julián	Proc. ACM Program. Lang., vol. 6, issue POPL: "Profile Inference Revisited ..." Profile Inference Revisited Wenlei He, Julián Mestre, Sergey Pupyrev, Lei Wang, and Hongtao Yu (Facebook, USA; University of Sydney, Australia) Publisher's Version
	Mezini, Mira	Proc. ACM Program. Lang., vol. 6, issue POPL: "Dependently-Typed Data Plane ..." Dependently-Typed Data Plane Programming Matthias Eichholz, Eric Hayden Campbell, Matthias Krebs, Nate Foster, and Mira Mezini (TU Darmstadt, Germany; Cornell University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Functional
	Miltner, Anders	Proc. ACM Program. Lang., vol. 6, issue POPL: "Bottom-Up Synthesis of Recursive ..." Bottom-Up Synthesis of Recursive Functional Programs using Angelic Execution Anders Miltner, Adrian Trejo Nuñez, Ana Brendel, Swarat Chaudhuri, and Isil Dillig (University of Texas at Austin, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Misailovic, Sasa	Proc. ACM Program. Lang., vol. 6, issue POPL: "A Dual Number Abstraction ..." A Dual Number Abstraction for Static Analysis of Clarke Jacobians Jacob Laurel, Rem Yang, Gagandeep Singh, and Sasa Misailovic (University of Illinois at Urbana-Champaign, USA; VMware, USA) Publisher's Version
	Mislove, Michael	Proc. ACM Program. Lang., vol. 6, issue POPL: "Semantics for Variational ..." Semantics for Variational Quantum Programming Xiaodong Jia, Andre Kornell, Bert Lindenhovius, Michael Mislove, and Vladimir Zamdzhiev (Hunan University, China; Tulane University, USA; JKU Linz, Austria; Inria, France) Publisher's Version
	Monnier, Stefan	Proc. ACM Program. Lang., vol. 6, issue POPL: "Mœbius: Metaprogramming using ..." Mœbius: Metaprogramming using Contextual Types: The Stage Where System F Can Pattern Match on Itself Junyoung Jang, Samuel Gélineau, Stefan Monnier, and Brigitte Pientka (McGill University, Canada; SimSpace, Canada; Université de Montréal, Canada) Publisher's Version
	Müller, Mark Niklas	Proc. ACM Program. Lang., vol. 6, issue POPL: "PRIMA: General and Precise ..." PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations Mark Niklas Müller, Gleb Makarchuk, Gagandeep Singh, Markus Püschel, and Martin Vechev (ETH Zurich, Switzerland; VMware Research, USA; University of Illinois at Urbana-Champaign, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Muller, Stefan K.	Proc. ACM Program. Lang., vol. 6, issue POPL: "Static Prediction of Parallel ..." Static Prediction of Parallel Computation Graphs Stefan K. Muller (Illinois Institute of Technology, USA) Publisher's Version Archive submitted (900 kB)
	Nagarakatte, Santosh	Proc. ACM Program. Lang., vol. 6, issue POPL: "One Polynomial Approximation ..." One Polynomial Approximation to Produce Correctly Rounded Results of an Elementary Function for Multiple Representations and Rounding Modes Jay P. Lim and Santosh Nagarakatte (Rutgers University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Nanevski, Aleksandar	Proc. ACM Program. Lang., vol. 6, issue POPL: "Visibility Reasoning for Concurrent ..." Visibility Reasoning for Concurrent Snapshot Algorithms Joakim Öhman and Aleksandar Nanevski (IMDEA Software Institute, Spain; Universidad Politécnica de Madrid, Spain) Publisher's Version Archive submitted (530 kB)
	Narayan, Shravan	Proc. ACM Program. Lang., vol. 6, issue POPL: "Isolation without Taxation: ..." Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFI Matthew Kolosick, Shravan Narayan, Evan Johnson, Conrad Watt, Michael LeMay, Deepak Garg, Ranjit Jhala, and Deian Stefan (University of California at San Diego, USA; University of Cambridge, UK; Intel Labs, USA; MPI-SWS, Germany) Publisher's Version
	Nelson, Luke	Proc. ACM Program. Lang., vol. 6, issue POPL: "A Formal Foundation for Symbolic ..." A Formal Foundation for Symbolic Evaluation with Merging Sorawee Porncharoenwase, Luke Nelson, Xi Wang, and Emina Torlak (University of Washington, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Nguyen, Minh	Proc. ACM Program. Lang., vol. 6, issue POPL: "Linked Visualisations via ..." Linked Visualisations via Galois Dependencies Roly Perera, Minh Nguyen, Tomas Petricek, and Meng Wang (Alan Turing Institute, UK; University of Bristol, UK; University of Kent, UK) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Nguyễn, Kim	Proc. ACM Program. Lang., vol. 6, issue POPL: "On Type-Cases, Union Elimination, ..." On Type-Cases, Union Elimination, and Occurrence Typing Giuseppe Castagna, Mickaël Laurent, Kim Nguyễn, and Matthew Lutze (CNRS, France; Université de Paris, France; Université Paris-Saclay, France) Publisher's Version Published Artifact Archive submitted (1.1 MB) Artifacts Available Artifacts Reusable
	Niu, Yue	Proc. ACM Program. Lang., vol. 6, issue POPL: "A Cost-Aware Logical Framework ..." A Cost-Aware Logical Framework Yue Niu, Jonathan Sterling, Harrison Grodin, and Robert Harper (Carnegie Mellon University, USA; Aarhus University, Denmark) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Nuñez, Adrian Trejo	Proc. ACM Program. Lang., vol. 6, issue POPL: "Bottom-Up Synthesis of Recursive ..." Bottom-Up Synthesis of Recursive Functional Programs using Angelic Execution Anders Miltner, Adrian Trejo Nuñez, Ana Brendel, Swarat Chaudhuri, and Isil Dillig (University of Texas at Austin, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Odersky, Martin	Proc. ACM Program. Lang., vol. 6, issue POPL: "Type-Level Programming with ..." Type-Level Programming with Match Types Olivier Blanvillain, Jonathan Immanuel Brachthäuser, Maxime Kjaer, and Martin Odersky (EPFL, Switzerland; University of Tübingen, Germany) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Oh, Hakjoo	Proc. ACM Program. Lang., vol. 6, issue POPL: "Return of CFA: Call-Site Sensitivity ..." Return of CFA: Call-Site Sensitivity Can Be Superior to Object Sensitivity Even for Object-Oriented Programs Minseok Jeon and Hakjoo Oh (Korea University, South Korea) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	O'Hearn, Peter W.	Proc. ACM Program. Lang., vol. 6, issue POPL: "Concurrent Incorrectness Separation ..." Concurrent Incorrectness Separation Logic Azalea Raad, Josh Berdine, Derek Dreyer, and Peter W. O'Hearn (Imperial College London, UK; Meta, UK; MPI-SWS, Germany; University College London, UK) Publisher's Version
	Öhman, Joakim	Proc. ACM Program. Lang., vol. 6, issue POPL: "Visibility Reasoning for Concurrent ..." Visibility Reasoning for Concurrent Snapshot Algorithms Joakim Öhman and Aleksandar Nanevski (IMDEA Software Institute, Spain; Universidad Politécnica de Madrid, Spain) Publisher's Version Archive submitted (530 kB)
	Oliveira Vale, Arthur	Proc. ACM Program. Lang., vol. 6, issue POPL: "Layered and Object-Based Game ..." Layered and Object-Based Game Semantics Arthur Oliveira Vale, Paul-André Melliès, Zhong Shao, Jérémie Koenig, and Léo Stefanesco (Yale University, USA; CNRS, France; Université de Paris, France; MPI-SWS, Germany) Publisher's Version
	Ouaknine, Joël	Proc. ACM Program. Lang., vol. 6, issue POPL: "What’s Decidable about Linear ..." What’s Decidable about Linear Loops? Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, David Purser, Anton Varonka, Markus A. Whiteland, and James Worrell (MPI-SWS, Germany; University of Oxford, UK) Publisher's Version
	Padon, Oded	Proc. ACM Program. Lang., vol. 6, issue POPL: "Induction Duality: Primal-Dual ..." Induction Duality: Primal-Dual Search for Invariants Oded Padon, James R. Wilcox, Jason R. Koenig, Kenneth L. McMillan, and Alex Aiken (VMware Research, USA; Stanford University, USA; Certora, USA; University of Texas at Austin, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Functional
	Padovani, Luca	Proc. ACM Program. Lang., vol. 6, issue POPL: "Fair Termination of Binary ..." Fair Termination of Binary Sessions Luca Ciccone and Luca Padovani (University of Turin, Italy) Publisher's Version Published Artifact Archive submitted (600 kB) Artifacts Available Artifacts Reusable
	Pavlogiannis, Andreas	Proc. ACM Program. Lang., vol. 6, issue POPL: "The Decidability and Complexity ..." The Decidability and Complexity of Interleaved Bidirected Dyck Reachability Adam Husted Kjelstrøm and Andreas Pavlogiannis (Aarhus University, Denmark) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Perera, Roly	Proc. ACM Program. Lang., vol. 6, issue POPL: "Linked Visualisations via ..." Linked Visualisations via Galois Dependencies Roly Perera, Minh Nguyen, Tomas Petricek, and Meng Wang (Alan Turing Institute, UK; University of Bristol, UK; University of Kent, UK) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Petricek, Tomas	Proc. ACM Program. Lang., vol. 6, issue POPL: "Linked Visualisations via ..." Linked Visualisations via Galois Dependencies Roly Perera, Minh Nguyen, Tomas Petricek, and Meng Wang (Alan Turing Institute, UK; University of Bristol, UK; University of Kent, UK) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Peyton Jones, Simon	Proc. ACM Program. Lang., vol. 6, issue POPL: "Provably Correct, Asymptotically ..." Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic Differentiation Faustyna Krawiec, Simon Peyton Jones, Neel Krishnaswami, Tom Ellis, Richard A. Eisenberg, and Andrew Fitzgibbon (University of Cambridge, UK; Microsoft Research, UK; Tweag, France) Publisher's Version
	Pickering, Matthew	Proc. ACM Program. Lang., vol. 6, issue POPL: "Staging with Class: A Specification ..." Staging with Class: A Specification for Typed Template Haskell Ningning Xie, Matthew Pickering, Andres Löh, Nicolas Wu, Jeremy Yallop, and Meng Wang (University of Cambridge, UK; Well-Typed LLP, UK; Imperial College London, UK; University of Bristol, UK) Publisher's Version
	Pientka, Brigitte	Proc. ACM Program. Lang., vol. 6, issue POPL: "Mœbius: Metaprogramming using ..." Mœbius: Metaprogramming using Contextual Types: The Stage Where System F Can Pattern Match on Itself Junyoung Jang, Samuel Gélineau, Stefan Monnier, and Brigitte Pientka (McGill University, Canada; SimSpace, Canada; Université de Montréal, Canada) Publisher's Version
	Podkopaev, Anton	Proc. ACM Program. Lang., vol. 6, issue POPL: "The Leaky Semicolon: Compositional ..." The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Concurrency Alan Jeffrey, James Riely, Mark Batty, Simon Cooksey, Ilya Kaysin, and Anton Podkopaev (Roblox, USA; DePaul University, USA; University of Kent, UK; JetBrains Research, Russia; University of Cambridge, UK; HSE University, Russia) Publisher's Version Published Artifact Artifacts Available
	Porncharoenwase, Sorawee	Proc. ACM Program. Lang., vol. 6, issue POPL: "A Formal Foundation for Symbolic ..." A Formal Foundation for Symbolic Evaluation with Merging Sorawee Porncharoenwase, Luke Nelson, Xi Wang, and Emina Torlak (University of Washington, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Pottier, François	Proc. ACM Program. Lang., vol. 6, issue POPL: "A Separation Logic for Heap ..." A Separation Logic for Heap Space under Garbage Collection Jean-Marie Madiot and François Pottier (Inria, France) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Prakriya, Gautam	Proc. ACM Program. Lang., vol. 6, issue POPL: "Interval Universal Approximation ..." Interval Universal Approximation for Neural Networks Zi Wang, Aws Albarghouthi, Gautam Prakriya, and Somesh Jha (University of Wisconsin-Madison, USA; Chinese University of Hong Kong, China; University of Wisconsin, USA) Publisher's Version Archive submitted (830 kB)
	Pujet, Loïc	Proc. ACM Program. Lang., vol. 6, issue POPL: "Observational Equality: Now ..." Observational Equality: Now for Good Loïc Pujet and Nicolas Tabareau (Inria, France) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Pupyrev, Sergey	Proc. ACM Program. Lang., vol. 6, issue POPL: "Profile Inference Revisited ..." Profile Inference Revisited Wenlei He, Julián Mestre, Sergey Pupyrev, Lei Wang, and Hongtao Yu (Facebook, USA; University of Sydney, Australia) Publisher's Version
	Purser, David	Proc. ACM Program. Lang., vol. 6, issue POPL: "What’s Decidable about Linear ..." What’s Decidable about Linear Loops? Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, David Purser, Anton Varonka, Markus A. Whiteland, and James Worrell (MPI-SWS, Germany; University of Oxford, UK) Publisher's Version
	Püschel, Markus	Proc. ACM Program. Lang., vol. 6, issue POPL: "PRIMA: General and Precise ..." PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations Mark Niklas Müller, Gleb Makarchuk, Gagandeep Singh, Markus Püschel, and Martin Vechev (ETH Zurich, Switzerland; VMware Research, USA; University of Illinois at Urbana-Champaign, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Raad, Azalea	Proc. ACM Program. Lang., vol. 6, issue POPL: "Extending Intel-x86 Consistency ..." Extending Intel-x86 Consistency and Persistency: Formalising the Semantics of Intel-x86 Memory Types and Non-temporal Stores Azalea Raad, Luc Maranget, and Viktor Vafeiadis (Imperial College London, UK; Inria, France; MPI-SWS, Germany) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Proc. ACM Program. Lang., vol. 6, issue POPL: "Concurrent Incorrectness Separation ..." Concurrent Incorrectness Separation Logic Azalea Raad, Josh Berdine, Derek Dreyer, and Peter W. O'Hearn (Imperial College London, UK; Meta, UK; MPI-SWS, Germany; University College London, UK) Publisher's Version
	Ragan-Kelley, Jonathan	Proc. ACM Program. Lang., vol. 6, issue POPL: "Verified Tensor-Program Optimization ..." Verified Tensor-Program Optimization Via High-Level Scheduling Rewrites Amanda Liu, Gilbert Louis Bernstein, Adam Chlipala, and Jonathan Ragan-Kelley (Massachusetts Institute of Technology, USA; University of California at Berkeley, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Riely, James	Proc. ACM Program. Lang., vol. 6, issue POPL: "The Leaky Semicolon: Compositional ..." The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Concurrency Alan Jeffrey, James Riely, Mark Batty, Simon Cooksey, Ilya Kaysin, and Anton Podkopaev (Roblox, USA; DePaul University, USA; University of Kent, UK; JetBrains Research, Russia; University of Cambridge, UK; HSE University, Russia) Publisher's Version Published Artifact Artifacts Available
	Rümmer, Philipp	Proc. ACM Program. Lang., vol. 6, issue POPL: "Solving String Constraints ..." Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables Taolue Chen, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu (Birkbeck University of London, UK; Royal Holloway University of London, UK; Tsinghua University, China; Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; TU Kaiserslautern, Germany; MPI-SWS, Germany; Uppsala University, Sweden) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Sabry, Amr	Proc. ACM Program. Lang., vol. 6, issue POPL: "Symmetries in Reversible Programming: ..." Symmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible Programming Languages Vikraman Choudhury, Jacek Karwowski, and Amr Sabry (Indiana University, USA; University of Cambridge, UK; University of Warsaw, Poland) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Sagiv, Mooly	Proc. ACM Program. Lang., vol. 6, issue POPL: "Property-Directed Reachability ..." Property-Directed Reachability as Abstract Interpretation in the Monotone Theory Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, and James R. Wilcox (Tel Aviv University, Israel; Certora, USA) Publisher's Version
	Sammler, Michael	Proc. ACM Program. Lang., vol. 6, issue POPL: "VIP: Verifying Real-World ..." VIP: Verifying Real-World C Idioms with Integer-Pointer Casts Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, and Peter Sewell (MPI-SWS, Germany; University of Cambridge, UK; Radboud University Nijmegen, Netherlands) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Proc. ACM Program. Lang., vol. 6, issue POPL: "Simuliris: A Separation Logic ..." Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, and Derek Dreyer (MPI-SWS, Germany; Radboud University Nijmegen, Netherlands; KAIST, South Korea) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Sanan, David	Proc. ACM Program. Lang., vol. 6, issue POPL: "A Quantum Interpretation of ..." A Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantum Programs Based on Separation Logic Xuan-Bach Le, Shang-Wei Lin, Jun Sun, and David Sanan (Nanyang Technological University, Singapore; Singapore Management University, Singapore) Publisher's Version
	Sangiorgi, Davide	Proc. ACM Program. Lang., vol. 6, issue POPL: "From Enhanced Coinduction ..." From Enhanced Coinduction towards Enhanced Induction Davide Sangiorgi (University of Bologna, Italy; Inria, France) Publisher's Version Archive submitted (300 kB)
	Satya, Kris	Proc. ACM Program. Lang., vol. 6, issue POPL: "Efficient Algorithms for Dynamic ..." Efficient Algorithms for Dynamic Bidirected Dyck-Reachability Yuanbo Li, Kris Satya, and Qirun Zhang (Georgia Institute of Technology, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Saville, Philip	Proc. ACM Program. Lang., vol. 6, issue POPL: "Fully Abstract Models for ..." Fully Abstract Models for Effectful λ-Calculi via Category-Theoretic Logical Relations Ohad Kammar, Shin-ya Katsumata, and Philip Saville (University of Edinburgh, UK; National Institute of Informatics, Japan; University of Oxford, UK) Publisher's Version
	Schepper, Philipp	Proc. ACM Program. Lang., vol. 6, issue POPL: "Subcubic Certificates for ..." Subcubic Certificates for CFL Reachability Dmitry Chistikov, Rupak Majumdar, and Philipp Schepper (University of Warwick, UK; MPI-SWS, Germany; CISPA, Germany) Publisher's Version
	Sewell, Peter	Proc. ACM Program. Lang., vol. 6, issue POPL: "VIP: Verifying Real-World ..." VIP: Verifying Real-World C Idioms with Integer-Pointer Casts Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, and Peter Sewell (MPI-SWS, Germany; University of Cambridge, UK; Radboud University Nijmegen, Netherlands) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Shao, Zhong	Proc. ACM Program. Lang., vol. 6, issue POPL: "Verified Compilation of C ..." Verified Compilation of C Programs with a Nominal Memory Model Yuting Wang, Ling Zhang, Zhong Shao, and Jérémie Koenig (Shanghai Jiao Tong University, China; Yale University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Proc. ACM Program. Lang., vol. 6, issue POPL: "Layered and Object-Based Game ..." Layered and Object-Based Game Semantics Arthur Oliveira Vale, Paul-André Melliès, Zhong Shao, Jérémie Koenig, and Léo Stefanesco (Yale University, USA; CNRS, France; Université de Paris, France; MPI-SWS, Germany) Publisher's Version
	Shoham, Sharon	Proc. ACM Program. Lang., vol. 6, issue POPL: "Property-Directed Reachability ..." Property-Directed Reachability as Abstract Interpretation in the Monotone Theory Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, and James R. Wilcox (Tel Aviv University, Israel; Certora, USA) Publisher's Version Proc. ACM Program. Lang., vol. 6, issue POPL: "Solving Constrained Horn Clauses ..." Solving Constrained Horn Clauses Modulo Algebraic Data Types and Recursive Functions Hari Govind V K, Sharon Shoham, and Arie Gurfinkel (University of Waterloo, Canada; Tel Aviv University, Israel) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Singh, Gagandeep	Proc. ACM Program. Lang., vol. 6, issue POPL: "PRIMA: General and Precise ..." PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations Mark Niklas Müller, Gleb Makarchuk, Gagandeep Singh, Markus Püschel, and Martin Vechev (ETH Zurich, Switzerland; VMware Research, USA; University of Illinois at Urbana-Champaign, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Proc. ACM Program. Lang., vol. 6, issue POPL: "A Dual Number Abstraction ..." A Dual Number Abstraction for Static Analysis of Clarke Jacobians Jacob Laurel, Rem Yang, Gagandeep Singh, and Sasa Misailovic (University of Illinois at Urbana-Champaign, USA; VMware, USA) Publisher's Version
	Spies, Simon	Proc. ACM Program. Lang., vol. 6, issue POPL: "Simuliris: A Separation Logic ..." Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, and Derek Dreyer (MPI-SWS, Germany; Radboud University Nijmegen, Netherlands; KAIST, South Korea) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Stefan, Deian	Proc. ACM Program. Lang., vol. 6, issue POPL: "Isolation without Taxation: ..." Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFI Matthew Kolosick, Shravan Narayan, Evan Johnson, Conrad Watt, Michael LeMay, Deepak Garg, Ranjit Jhala, and Deian Stefan (University of California at San Diego, USA; University of Cambridge, UK; Intel Labs, USA; MPI-SWS, Germany) Publisher's Version
	Stefanesco, Léo	Proc. ACM Program. Lang., vol. 6, issue POPL: "Layered and Object-Based Game ..." Layered and Object-Based Game Semantics Arthur Oliveira Vale, Paul-André Melliès, Zhong Shao, Jérémie Koenig, and Léo Stefanesco (Yale University, USA; CNRS, France; Université de Paris, France; MPI-SWS, Germany) Publisher's Version
	Sterling, Jonathan	Proc. ACM Program. Lang., vol. 6, issue POPL: "A Cost-Aware Logical Framework ..." A Cost-Aware Logical Framework Yue Niu, Jonathan Sterling, Harrison Grodin, and Robert Harper (Carnegie Mellon University, USA; Aarhus University, Denmark) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Sun, Jun	Proc. ACM Program. Lang., vol. 6, issue POPL: "A Quantum Interpretation of ..." A Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantum Programs Based on Separation Logic Xuan-Bach Le, Shang-Wei Lin, Jun Sun, and David Sanan (Nanyang Technological University, Singapore; Singapore Management University, Singapore) Publisher's Version
	Szamozvancev, Dmitrij	Proc. ACM Program. Lang., vol. 6, issue POPL: "Formal Metatheory of Second-Order ..." Formal Metatheory of Second-Order Abstract Syntax Marcelo Fiore and Dmitrij Szamozvancev (University of Cambridge, UK) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Tabareau, Nicolas	Proc. ACM Program. Lang., vol. 6, issue POPL: "Observational Equality: Now ..." Observational Equality: Now for Good Loïc Pujet and Nicolas Tabareau (Inria, France) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Tan, Bryan	Proc. ACM Program. Lang., vol. 6, issue POPL: "SolType: Refinement Types ..." SolType: Refinement Types for Arithmetic Overflow in Solidity Bryan Tan, Benjamin Mariano, Shuvendu K. Lahiri, Isil Dillig, and Yu Feng (University of California at Santa Barbara, USA; University of Texas at Austin, USA; Microsoft Research, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Tassarotti, Joseph	Proc. ACM Program. Lang., vol. 6, issue POPL: "A Separation Logic for Negative ..." A Separation Logic for Negative Dependence Jialu Bao, Marco Gaboardi, Justin Hsu, and Joseph Tassarotti (Cornell University, USA; Boston University, USA; Boston College, USA) Publisher's Version
	Tatlock, Zachary	Proc. ACM Program. Lang., vol. 6, issue POPL: "Relational E-matching ..." Relational E-matching Yihong Zhang, Yisu Remy Wang, Max Willsey, and Zachary Tatlock (University of Washington, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Thinniyam, Ramanathan S.	Proc. ACM Program. Lang., vol. 6, issue POPL: "Context-Bounded Verification ..." Context-Bounded Verification of Thread Pools Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche (MPI-SWS, Germany) Publisher's Version
	Torlak, Emina	Proc. ACM Program. Lang., vol. 6, issue POPL: "A Formal Foundation for Symbolic ..." A Formal Foundation for Symbolic Evaluation with Merging Sorawee Porncharoenwase, Luke Nelson, Xi Wang, and Emina Torlak (University of Washington, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Tsukada, Takeshi	Proc. ACM Program. Lang., vol. 6, issue POPL: "Software Model-Checking as ..." Software Model-Checking as Cyclic-Proof Search Takeshi Tsukada and Hiroshi Unno (Chiba University, Japan; University of Tsukuba, Japan; RIKEN AIP, Japan) Publisher's Version
	Unno, Hiroshi	Proc. ACM Program. Lang., vol. 6, issue POPL: "Software Model-Checking as ..." Software Model-Checking as Cyclic-Proof Search Takeshi Tsukada and Hiroshi Unno (Chiba University, Japan; University of Tsukuba, Japan; RIKEN AIP, Japan) Publisher's Version
	Vafeiadis, Viktor	Proc. ACM Program. Lang., vol. 6, issue POPL: "Extending Intel-x86 Consistency ..." Extending Intel-x86 Consistency and Persistency: Formalising the Semantics of Intel-x86 Memory Types and Non-temporal Stores Azalea Raad, Luc Maranget, and Viktor Vafeiadis (Imperial College London, UK; Inria, France; MPI-SWS, Germany) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Proc. ACM Program. Lang., vol. 6, issue POPL: "Truly Stateless, Optimal Dynamic ..." Truly Stateless, Optimal Dynamic Partial Order Reduction Michalis Kokologiannakis, Iason Marmanis, Vladimir Gladstein, and Viktor Vafeiadis (MPI-SWS, Germany; St. Petersburg University, Russia; JetBrains Research, Russia) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Varonka, Anton	Proc. ACM Program. Lang., vol. 6, issue POPL: "What’s Decidable about Linear ..." What’s Decidable about Linear Loops? Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, David Purser, Anton Varonka, Markus A. Whiteland, and James Worrell (MPI-SWS, Germany; University of Oxford, UK) Publisher's Version
	Vechev, Martin	Proc. ACM Program. Lang., vol. 6, issue POPL: "PRIMA: General and Precise ..." PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations Mark Niklas Müller, Gleb Makarchuk, Gagandeep Singh, Markus Püschel, and Martin Vechev (ETH Zurich, Switzerland; VMware Research, USA; University of Illinois at Urbana-Champaign, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Walker, David	Proc. ACM Program. Lang., vol. 6, issue POPL: "Safe, Modular Packet Pipeline ..." Safe, Modular Packet Pipeline Programming Devon Loehr and David Walker (Princeton University, USA) Publisher's Version Published Artifact Archive submitted (760 kB) Artifacts Available Artifacts Reusable
	Wang, Lei	Proc. ACM Program. Lang., vol. 6, issue POPL: "Profile Inference Revisited ..." Profile Inference Revisited Wenlei He, Julián Mestre, Sergey Pupyrev, Lei Wang, and Hongtao Yu (Facebook, USA; University of Sydney, Australia) Publisher's Version
	Wang, Meng	Proc. ACM Program. Lang., vol. 6, issue POPL: "Staging with Class: A Specification ..." Staging with Class: A Specification for Typed Template Haskell Ningning Xie, Matthew Pickering, Andres Löh, Nicolas Wu, Jeremy Yallop, and Meng Wang (University of Cambridge, UK; Well-Typed LLP, UK; Imperial College London, UK; University of Bristol, UK) Publisher's Version Proc. ACM Program. Lang., vol. 6, issue POPL: "Linked Visualisations via ..." Linked Visualisations via Galois Dependencies Roly Perera, Minh Nguyen, Tomas Petricek, and Meng Wang (Alan Turing Institute, UK; University of Bristol, UK; University of Kent, UK) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Wang, Xi	Proc. ACM Program. Lang., vol. 6, issue POPL: "A Formal Foundation for Symbolic ..." A Formal Foundation for Symbolic Evaluation with Merging Sorawee Porncharoenwase, Luke Nelson, Xi Wang, and Emina Torlak (University of Washington, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Wang, Yisu Remy	Proc. ACM Program. Lang., vol. 6, issue POPL: "Relational E-matching ..." Relational E-matching Yihong Zhang, Yisu Remy Wang, Max Willsey, and Zachary Tatlock (University of Washington, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Wang, Yuting	Proc. ACM Program. Lang., vol. 6, issue POPL: "Verified Compilation of C ..." Verified Compilation of C Programs with a Nominal Memory Model Yuting Wang, Ling Zhang, Zhong Shao, and Jérémie Koenig (Shanghai Jiao Tong University, China; Yale University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Wang, Zhuyang	Proc. ACM Program. Lang., vol. 6, issue POPL: "Logarithm and Program Testing ..." Logarithm and Program Testing Kuen-Bang Hou (Favonia) and Zhuyang Wang (University of Minnesota, USA) Publisher's Version Published Artifact Archive submitted (540 kB) Artifacts Available Artifacts Reusable
	Wang, Zi	Proc. ACM Program. Lang., vol. 6, issue POPL: "Interval Universal Approximation ..." Interval Universal Approximation for Neural Networks Zi Wang, Aws Albarghouthi, Gautam Prakriya, and Somesh Jha (University of Wisconsin-Madison, USA; Chinese University of Hong Kong, China; University of Wisconsin, USA) Publisher's Version Archive submitted (830 kB)
	Watt, Conrad	Proc. ACM Program. Lang., vol. 6, issue POPL: "Isolation without Taxation: ..." Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFI Matthew Kolosick, Shravan Narayan, Evan Johnson, Conrad Watt, Michael LeMay, Deepak Garg, Ranjit Jhala, and Deian Stefan (University of California at San Diego, USA; University of Cambridge, UK; Intel Labs, USA; MPI-SWS, Germany) Publisher's Version
	Whiteland, Markus A.	Proc. ACM Program. Lang., vol. 6, issue POPL: "What’s Decidable about Linear ..." What’s Decidable about Linear Loops? Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, David Purser, Anton Varonka, Markus A. Whiteland, and James Worrell (MPI-SWS, Germany; University of Oxford, UK) Publisher's Version
	Wilcox, James R.	Proc. ACM Program. Lang., vol. 6, issue POPL: "Property-Directed Reachability ..." Property-Directed Reachability as Abstract Interpretation in the Monotone Theory Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, and James R. Wilcox (Tel Aviv University, Israel; Certora, USA) Publisher's Version Proc. ACM Program. Lang., vol. 6, issue POPL: "Induction Duality: Primal-Dual ..." Induction Duality: Primal-Dual Search for Invariants Oded Padon, James R. Wilcox, Jason R. Koenig, Kenneth L. McMillan, and Alex Aiken (VMware Research, USA; Stanford University, USA; Certora, USA; University of Texas at Austin, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Functional
	Willsey, Max	Proc. ACM Program. Lang., vol. 6, issue POPL: "Relational E-matching ..." Relational E-matching Yihong Zhang, Yisu Remy Wang, Max Willsey, and Zachary Tatlock (University of Washington, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Worrell, James	Proc. ACM Program. Lang., vol. 6, issue POPL: "What’s Decidable about Linear ..." What’s Decidable about Linear Loops? Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, David Purser, Anton Varonka, Markus A. Whiteland, and James Worrell (MPI-SWS, Germany; University of Oxford, UK) Publisher's Version
	Wu, Nicolas	Proc. ACM Program. Lang., vol. 6, issue POPL: "Staging with Class: A Specification ..." Staging with Class: A Specification for Typed Template Haskell Ningning Xie, Matthew Pickering, Andres Löh, Nicolas Wu, Jeremy Yallop, and Meng Wang (University of Cambridge, UK; Well-Typed LLP, UK; Imperial College London, UK; University of Bristol, UK) Publisher's Version
	Wu, Zhilin	Proc. ACM Program. Lang., vol. 6, issue POPL: "Solving String Constraints ..." Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables Taolue Chen, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu (Birkbeck University of London, UK; Royal Holloway University of London, UK; Tsinghua University, China; Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; TU Kaiserslautern, Germany; MPI-SWS, Germany; Uppsala University, Sweden) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Xie, Ningning	Proc. ACM Program. Lang., vol. 6, issue POPL: "Staging with Class: A Specification ..." Staging with Class: A Specification for Typed Template Haskell Ningning Xie, Matthew Pickering, Andres Löh, Nicolas Wu, Jeremy Yallop, and Meng Wang (University of Cambridge, UK; Well-Typed LLP, UK; Imperial College London, UK; University of Bristol, UK) Publisher's Version
	Yallop, Jeremy	Proc. ACM Program. Lang., vol. 6, issue POPL: "Staging with Class: A Specification ..." Staging with Class: A Specification for Typed Template Haskell Ningning Xie, Matthew Pickering, Andres Löh, Nicolas Wu, Jeremy Yallop, and Meng Wang (University of Cambridge, UK; Well-Typed LLP, UK; Imperial College London, UK; University of Bristol, UK) Publisher's Version
	Yang, Rem	Proc. ACM Program. Lang., vol. 6, issue POPL: "A Dual Number Abstraction ..." A Dual Number Abstraction for Static Analysis of Clarke Jacobians Jacob Laurel, Rem Yang, Gagandeep Singh, and Sasa Misailovic (University of Illinois at Urbana-Champaign, USA; VMware, USA) Publisher's Version
	Ye, Qianchuan	Proc. ACM Program. Lang., vol. 6, issue POPL: "Oblivious Algebraic Data Types ..." Oblivious Algebraic Data Types Qianchuan Ye and Benjamin Delaware (Purdue University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Yu, Hongtao	Proc. ACM Program. Lang., vol. 6, issue POPL: "Profile Inference Revisited ..." Profile Inference Revisited Wenlei He, Julián Mestre, Sergey Pupyrev, Lei Wang, and Hongtao Yu (Facebook, USA; University of Sydney, Australia) Publisher's Version
	Yuan, Charles	Proc. ACM Program. Lang., vol. 6, issue POPL: "Twist: Sound Reasoning for ..." Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs Charles Yuan, Christopher McNally, and Michael Carbin (Massachusetts Institute of Technology, USA) Publisher's Version Published Artifact Archive submitted (690 kB) Artifacts Available Artifacts Reusable
	Zamdzhiev, Vladimir	Proc. ACM Program. Lang., vol. 6, issue POPL: "Semantics for Variational ..." Semantics for Variational Quantum Programming Xiaodong Jia, Andre Kornell, Bert Lindenhovius, Michael Mislove, and Vladimir Zamdzhiev (Hunan University, China; Tulane University, USA; JKU Linz, Austria; Inria, France) Publisher's Version
	Zetzsche, Georg	Proc. ACM Program. Lang., vol. 6, issue POPL: "Context-Bounded Verification ..." Context-Bounded Verification of Thread Pools Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche (MPI-SWS, Germany) Publisher's Version
	Zhang, Cheng	Proc. ACM Program. Lang., vol. 6, issue POPL: "On Incorrectness Logic and ..." On Incorrectness Logic and Kleene Algebra with Top and Tests Cheng Zhang, Arthur Azevedo de Amorim, and Marco Gaboardi (Boston University, USA) Publisher's Version
	Zhang, Ling	Proc. ACM Program. Lang., vol. 6, issue POPL: "Verified Compilation of C ..." Verified Compilation of C Programs with a Nominal Memory Model Yuting Wang, Ling Zhang, Zhong Shao, and Jérémie Koenig (Shanghai Jiao Tong University, China; Yale University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Zhang, Qirun	Proc. ACM Program. Lang., vol. 6, issue POPL: "Efficient Algorithms for Dynamic ..." Efficient Algorithms for Dynamic Bidirected Dyck-Reachability Yuanbo Li, Kris Satya, and Qirun Zhang (Georgia Institute of Technology, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Zhang, Yihong	Proc. ACM Program. Lang., vol. 6, issue POPL: "Relational E-matching ..." Relational E-matching Yihong Zhang, Yisu Remy Wang, Max Willsey, and Zachary Tatlock (University of Washington, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
	Zhang, Yizhou	Proc. ACM Program. Lang., vol. 6, issue POPL: "Reasoning about “Reasoning ..." Reasoning about “Reasoning about Reasoning”: Semantics and Contextual Equivalence for Probabilistic Programs with Nested Queries and Recursion Yizhou Zhang and Nada Amin (University of Waterloo, Canada; Harvard University, USA) Publisher's Version