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 Article: popl22main-p428-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498712
	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) Article: popl22main-p61-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498675
	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 Article: popl22main-p66-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498677
	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 Article: popl22main-p6-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498662
	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 Article: popl22main-p550-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498719
	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 Article: popl22main-p459-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498716
	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 Article: popl22main-p90-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498678
	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 Article: popl22main-p233-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498695
	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 Article: popl22main-p523-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498717
	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 Article: popl22main-p258-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498698
	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 Article: popl22main-p258-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498698
	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 Article: popl22main-p124-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498682
	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 Article: popl22main-p311-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498701
	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 Article: popl22main-p597-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498721
	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 Article: popl22main-p167-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498691
	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 Article: popl22main-p58-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498674
	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 Article: popl22main-p124-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498682
	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 Article: popl22main-p350-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498707
	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 Article: popl22main-p322-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498702
	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 Article: popl22main-p137-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498685 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 Article: popl22main-p523-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498717
	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 Article: popl22main-p31-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498667
	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 Article: popl22main-p30-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498666
	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 Article: popl22main-p459-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498716
	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 Article: popl22main-p94-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498680 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 Article: popl22main-p168-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498692
	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 Article: popl22main-p597-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498721
	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 Article: popl22main-p158-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498689
	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 Article: popl22main-p160-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498690
	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 Article: popl22main-p429-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498713
	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 Article: popl22main-p124-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498682 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 Article: popl22main-p27-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498665
	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 Article: popl22main-p95-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498681 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 Article: popl22main-p158-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498689 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 Article: popl22main-p233-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498695
	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 Article: popl22main-p311-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498701
	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 Article: popl22main-p397-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498710
	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 Article: popl22main-p397-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498710
	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 Article: popl22main-p137-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498685
	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 Article: popl22main-p65-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498676
	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 Article: popl22main-p27-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498665
	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 Article: popl22main-p437-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498715
	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 Article: popl22main-p397-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498710
	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 Article: popl22main-p350-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498707
	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 Article: popl22main-p311-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498701
	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 Article: popl22main-p160-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498690 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 Article: popl22main-p550-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498719
	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 Article: popl22main-p158-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498689
	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 Article: popl22main-p131-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498684 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 Article: popl22main-p151-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498688
	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 Article: popl22main-p94-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498680 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 Article: popl22main-p168-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498692
	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 Article: popl22main-p294-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498700
	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 Article: popl22main-p597-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498721
	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 Article: popl22main-p424-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498711
	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 Article: popl22main-p47-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498670
	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 Article: popl22main-p629-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498722
	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 Article: popl22main-p350-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498707
	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 Article: popl22main-p350-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498707
	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 Article: popl22main-p47-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498670
	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 Article: popl22main-p431-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498714
	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 Article: popl22main-p9-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498663
	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 Article: popl22main-p131-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498684
	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 Article: popl22main-p764-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498726
	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 Article: popl22main-p550-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498719
	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 Article: popl22main-p350-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498707
	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 Article: popl22main-p137-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498685
	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 Article: popl22main-p6-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498662
	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 Article: popl22main-p294-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498700
	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 Article: popl22main-p459-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498716
	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 Article: popl22main-p586-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498720
	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) Article: popl22main-p61-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498675
	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 Article: popl22main-p151-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498688
	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 Article: popl22main-p149-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498687
	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 Article: popl22main-p151-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498688
	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 Article: popl22main-p158-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498689
	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 Article: popl22main-p629-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498722
	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 Article: popl22main-p9-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498663
	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 Article: popl22main-p331-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498705
	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 Article: popl22main-p350-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498707
	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 Article: popl22main-p158-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498689
	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 Article: popl22main-p767-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498727
	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 Article: popl22main-p31-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498667
	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 Article: popl22main-p331-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498705
	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 Article: popl22main-p459-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498716
	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 Article: popl22main-p42-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498669
	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 Article: popl22main-p258-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498698
	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 Article: popl22main-p55-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498673
	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 Article: popl22main-p428-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498712
	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 Article: popl22main-p143-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498686 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 Article: popl22main-p327-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498703
	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 Article: popl22main-p424-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498711
	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 Article: popl22main-p151-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498688
	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 Article: popl22main-p149-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498687
	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 Article: popl22main-p397-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498710
	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 Article: popl22main-p6-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498662 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 Article: popl22main-p95-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498681 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 Article: popl22main-p158-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498689
	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 Article: popl22main-p311-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498701
	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 Article: popl22main-p397-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498710
	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 Article: popl22main-p48-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498671
	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 Article: popl22main-p27-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498665
	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 Article: popl22main-p542-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498718
	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 Article: popl22main-p58-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498674
	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 Article: popl22main-p247-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498697
	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 Article: popl22main-p767-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498727
	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 Article: popl22main-p151-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498688
	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 Article: popl22main-p95-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498681
	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 Article: popl22main-p725-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498724
	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 Article: popl22main-p25-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498664
	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 Article: popl22main-p350-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498707
	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 Article: popl22main-p247-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498697
	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 Article: popl22main-p149-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498687
	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 Article: popl22main-p523-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498717
	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 Article: popl22main-p275-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498699
	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 Article: popl22main-p706-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498723
	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 Article: popl22main-p58-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498674
	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 Article: popl22main-p48-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498671
	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 Article: popl22main-p49-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498672
	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 Article: popl22main-p90-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498678 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 Article: popl22main-p322-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498702
	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 Article: popl22main-p329-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498704
	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 Article: popl22main-p126-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498683
	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 Article: popl22main-p27-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498665
	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 Article: popl22main-p424-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498711
	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 Article: popl22main-p428-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498712
	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 Article: popl22main-p167-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498691
	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 Article: popl22main-p327-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498703
	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 Article: popl22main-p95-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498681
	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 Article: popl22main-p431-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498714
	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 Article: popl22main-p311-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498701
	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 Article: popl22main-p124-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498682
	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 Article: popl22main-p542-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498718
	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 Article: popl22main-p149-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498687
	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 Article: popl22main-p294-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498700
	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 Article: popl22main-p329-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498704
	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) Article: popl22main-p383-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498708
	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 Article: popl22main-p25-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498664
	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) Article: popl22main-p206-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498694
	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 Article: popl22main-p151-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498688
	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 Article: popl22main-p390-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498709
	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 Article: popl22main-p34-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498668
	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 Article: popl22main-p58-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498674
	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 Article: popl22main-p47-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498670
	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 Article: popl22main-p124-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498682
	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 Article: popl22main-p258-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498698
	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 Article: popl22main-p586-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498720
	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 Article: popl22main-p233-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498695
	Ö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) Article: popl22main-p206-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498694
	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 Article: popl22main-p327-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498703
	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 Article: popl22main-p767-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498727
	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 Article: popl22main-p428-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498712
	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 Article: popl22main-p30-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498666
	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 Article: popl22main-p55-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498673
	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 Article: popl22main-p34-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498668
	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 Article: popl22main-p34-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498668
	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 Article: popl22main-p397-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498710
	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 Article: popl22main-p706-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498723
	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 Article: popl22main-p294-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498700
	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 Article: popl22main-p459-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498716
	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 Article: popl22main-p390-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498709
	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 Article: popl22main-p49-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498672
	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) Article: popl22main-p61-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498675
	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 Article: popl22main-p191-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498693
	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 Article: popl22main-p431-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498714
	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 Article: popl22main-p767-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498727
	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 Article: popl22main-p329-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498704
	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 Article: popl22main-p126-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498683 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 Article: popl22main-p233-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498695
	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 Article: popl22main-p523-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498717
	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 Article: popl22main-p459-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498716
	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 Article: popl22main-p350-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498707
	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 Article: popl22main-p31-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498667
	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 Article: popl22main-p65-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498676
	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 Article: popl22main-p95-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498681 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 Article: popl22main-p158-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498689
	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 Article: popl22main-p247-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498697
	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) Article: popl22main-p93-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498679
	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 Article: popl22main-p725-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498724
	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 Article: popl22main-p331-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498705
	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 Article: popl22main-p322-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498702
	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 Article: popl22main-p95-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498681
	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 Article: popl22main-p143-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498686 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 Article: popl22main-p327-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498703
	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 Article: popl22main-p65-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498676 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 Article: popl22main-p629-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498722
	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 Article: popl22main-p329-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498704 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 Article: popl22main-p542-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498718
	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 Article: popl22main-p158-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498689
	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 Article: popl22main-p151-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498688
	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 Article: popl22main-p327-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498703
	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 Article: popl22main-p47-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498670
	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 Article: popl22main-p247-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498697
	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 Article: popl22main-p437-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498715
	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 Article: popl22main-p191-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498693
	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 Article: popl22main-p27-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498665
	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 Article: popl22main-p550-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498719
	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 Article: popl22main-p244-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498696
	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 Article: popl22main-p90-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498678
	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 Article: popl22main-p390-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498709
	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 Article: popl22main-p736-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498725
	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 Article: popl22main-p736-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498725
	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 Article: popl22main-p126-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498683 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 Article: popl22main-p424-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498711
	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 Article: popl22main-p767-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498727
	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 Article: popl22main-p329-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498704
	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 Article: popl22main-p275-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498699
	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 Article: popl22main-p431-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498714
	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 Article: popl22main-p706-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498723 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 Article: popl22main-p34-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498668
	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 Article: popl22main-p390-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498709
	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 Article: popl22main-p244-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498696
	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 Article: popl22main-p143-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498686
	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 Article: popl22main-p764-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498726
	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) Article: popl22main-p61-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498675
	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 Article: popl22main-p151-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498688
	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 Article: popl22main-p767-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498727
	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 Article: popl22main-p65-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498676 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 Article: popl22main-p428-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498712
	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 Article: popl22main-p244-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498696
	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 Article: popl22main-p767-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498727
	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 Article: popl22main-p706-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498723
	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 Article: popl22main-p350-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498707
	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 Article: popl22main-p706-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498723
	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 Article: popl22main-p706-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498723
	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 Article: popl22main-p542-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498718
	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 Article: popl22main-p429-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498713
	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 Article: popl22main-p431-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498714
	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 Article: popl22main-p167-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498691
	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 Article: popl22main-p149-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498687
	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 Article: popl22main-p90-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498678
	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 Article: popl22main-p160-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498690
	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 Article: popl22main-p143-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498686
	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 Article: popl22main-p725-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498724
	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 Article: popl22main-p244-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498696
	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 Article: popl22main-p66-p (type: Full Paper (25 pages + up to 4 pages with charge + references)) doi:10.1145/3498677