POPL 2023 – Author Index

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

	Abreu, Pedro	Proc. ACM Program. Lang., vol. 7, issue POPL: "A Type-Based Approach to Divide-and-Conquer ..." A Type-Based Approach to Divide-and-Conquer Recursion in Coq Pedro Abreu, Benjamin Delaware, Alex Hubers, Christa Jenkins, J. Garrett Morris, and Aaron Stump (Purdue University, USA; University of Iowa, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p17-p doi:10.1145/3571196
	Aguirre, Alejandro	Proc. ACM Program. Lang., vol. 7, issue POPL: "Step-Indexed Logical Relations ..." Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice Alejandro Aguirre and Lars Birkedal (Aarhus University, Denmark) Publisher's Version Article: popl23main-p3-p doi:10.1145/3571195
	Alur, Rajeev	Proc. ACM Program. Lang., vol. 7, issue POPL: "Executing Microservice Applications ..." Executing Microservice Applications on Serverless, Correctly Konstantinos Kallas, Haoran Zhang, Rajeev Alur, Sebastian Angel, and Vincent Liu (University of Pennsylvania, USA; Microsoft Research, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl23main-p93-p doi:10.1145/3571206 Proc. ACM Program. Lang., vol. 7, issue POPL: "A Robust Theory of Series ..." A Robust Theory of Series Parallel Graphs Rajeev Alur, Caleb Stanford, and Christopher Watson (University of Pennsylvania, USA; University of California at San Diego, USA; University of California at Davis, USA) Publisher's Version Article: popl23main-p256-p doi:10.1145/3571230
	Angel, Sebastian	Proc. ACM Program. Lang., vol. 7, issue POPL: "Executing Microservice Applications ..." Executing Microservice Applications on Serverless, Correctly Konstantinos Kallas, Haoran Zhang, Rajeev Alur, Sebastian Angel, and Vincent Liu (University of Pennsylvania, USA; Microsoft Research, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl23main-p93-p doi:10.1145/3571206
	Angiuli, Carlo	Proc. ACM Program. Lang., vol. 7, issue POPL: "An Order-Theoretic Analysis ..." An Order-Theoretic Analysis of Universe Polymorphism Kuen-Bang Hou (Favonia), Carlo Angiuli, and Reed Mullanix (University of Minnesota, USA; Carnegie Mellon University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p471-p doi:10.1145/3571250
	Antonopoulos, Timos	Proc. ACM Program. Lang., vol. 7, issue POPL: "An Algebra of Alignment for ..." An Algebra of Alignment for Relational Verification Timos Antonopoulos, Eric Koskinen, Ton Chanh Le, Ramana Nagasamudram, David A. Naumann, and Minh Ngo (Yale University, USA; Stevens Institute of Technology, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p114-p doi:10.1145/3571213
	Arrial, Victor	Proc. ACM Program. Lang., vol. 7, issue POPL: "Quantitative Inhabitation ..." Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework Victor Arrial, Giulio Guerrieri, and Delia Kesner (Université Paris Cité - CNRS - IRIF, France; Aix Marseille Université - CNRS - LIS, France; Edinburgh Research Centre - Central Software Institute - Huawei, UK; Institut Universitaire de France, France) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p365-p doi:10.1145/3571244
	Bach Poulsen, Casper	Proc. ACM Program. Lang., vol. 7, issue POPL: "Hefty Algebras: Modular Elaboration ..." Hefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects Casper Bach Poulsen and Cas van der Rest (Delft University of Technology, Netherlands) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p530-p doi:10.1145/3571255
	Baker, Alan	Proc. ACM Program. Lang., vol. 7, issue POPL: "Taking Back Control in an ..." Taking Back Control in an Intermediate Representation for GPU Computing Vasileios Klimis, Jack Clark, Alan Baker, David Neto, John Wickerson, and Alastair F. Donaldson (Imperial College London, UK; Google, Canada; Google, UK) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p511-p doi:10.1145/3571253
	Balzer, Stephanie	Proc. ACM Program. Lang., vol. 7, issue POPL: "Higher-Order Leak and Deadlock ..." Higher-Order Leak and Deadlock Free Locks Jules Jacobs and Stephanie Balzer (Radboud University Nijmegen, Netherlands; Carnegie Mellon University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p231-p doi:10.1145/3571229
	Barrière, Aurèle	Proc. ACM Program. Lang., vol. 7, issue POPL: "Formally Verified Native Code ..." Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler Aurèle Barrière, Sandrine Blazy, and David Pichardie (University of Rennes, France; Inria, France; CNRS, France; IRISA, France; Meta, France) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p72-p doi:10.1145/3571202
	Barthe, Gilles	Proc. ACM Program. Lang., vol. 7, issue POPL: "CoqQ: Foundational Verification ..." CoqQ: Foundational Verification of Quantum Programs Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, and Mingsheng Ying (MPI-SP, Germany; Institute of Software at Chinese Academy of Sciences, China; IMDEA Software Institute, Spain; Meta, France; University of Chinese Academy of Sciences, China; Tsinghua University, China) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p163-p doi:10.1145/3571222
	Batz, Kevin	Proc. ACM Program. Lang., vol. 7, issue POPL: "A Calculus for Amortized Expected ..." A Calculus for Amortized Expected Runtimes Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Lena Verscht (RWTH Aachen University, Germany; Saarland University, Germany; University College London, UK; DTU, Denmark) Publisher's Version Article: popl23main-p592-p doi:10.1145/3571260
	Baumann, Pascal	Proc. ACM Program. Lang., vol. 7, issue POPL: "Context-Bounded Verification ..." Context-Bounded Verification of Context-Free Specifications Pascal Baumann, Moses Ganardi, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche (MPI-SWS, Germany) Publisher's Version Article: popl23main-p699-p doi:10.1145/3571266
	Bembenek, Aaron	Proc. ACM Program. Lang., vol. 7, issue POPL: "From SMT to ASP: Solver-Based ..." From SMT to ASP: Solver-Based Approaches to Solving Datalog Synthesis-as-Rule-Selection Problems Aaron Bembenek, Michael Greenberg, and Stephen Chong (Harvard University, USA; Stevens Institute of Technology, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p63-p doi:10.1145/3571200
	Birkedal, Lars	Proc. ACM Program. Lang., vol. 7, issue POPL: "Step-Indexed Logical Relations ..." Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice Alejandro Aguirre and Lars Birkedal (Aarhus University, Denmark) Publisher's Version Article: popl23main-p3-p doi:10.1145/3571195
	Blazy, Sandrine	Proc. ACM Program. Lang., vol. 7, issue POPL: "Formally Verified Native Code ..." Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler Aurèle Barrière, Sandrine Blazy, and David Pichardie (University of Rennes, France; Inria, France; CNRS, France; IRISA, France; Meta, France) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p72-p doi:10.1145/3571202
	Bodík, Rastislav	Proc. ACM Program. Lang., vol. 7, issue POPL: "Grisette: Symbolic Compilation ..." Grisette: Symbolic Compilation as a Functional Programming Library Sirui Lu and Rastislav Bodík (University of Washington, USA; Google Research, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p97-p doi:10.1145/3571209
	Bonchi, Filippo	Proc. ACM Program. Lang., vol. 7, issue POPL: "Deconstructing the Calculus ..." Deconstructing the Calculus of Relations with Tape Diagrams Filippo Bonchi, Alessandro Di Giorgio, and Alessio Santamaria (University of Pisa, Italy; University of Sussex, UK) Publisher's Version Article: popl23main-p559-p doi:10.1145/3571257
	Bosamiya, Jay	Proc. ACM Program. Lang., vol. 7, issue POPL: "MSWasm: Soundly Enforcing ..." MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code Alexandra E. Michael, Anitha Gollamudi, Jay Bosamiya, Evan Johnson, Aidan Denlinger, Craig Disselkoen, Conrad Watt, Bryan Parno, Marco Patrignani, Marco Vassena, and Deian Stefan (University of California at San Diego, USA; University of Washington, USA; University of Massachusetts Lowell, USA; Carnegie Mellon University, USA; Arm, USA; University of Cambridge, UK; University of Trento, Italy; Utrecht University, Netherlands) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl23main-p96-p doi:10.1145/3571208
	Bowers, Matthew	Proc. ACM Program. Lang., vol. 7, issue POPL: "Top-Down Synthesis for Library ..." Top-Down Synthesis for Library Learning Matthew Bowers, Theo X. Olausson, Lionel Wong, Gabriel Grand, Joshua B. Tenenbaum, Kevin Ellis, and Armando Solar-Lezama (Massachusetts Institute of Technology, USA; Cornell University, USA) Publisher's Version Published Artifact Archive submitted (1.6 MB) Artifacts Available Artifacts Reusable Article: popl23main-p278-p doi:10.1145/3571234
	Broman, David	Proc. ACM Program. Lang., vol. 7, issue POPL: "Statically Resolvable Ambiguity ..." Statically Resolvable Ambiguity Viktor Palmkvist, Elias Castegren, Philipp Haller, and David Broman (KTH Royal Institute of Technology, Sweden; Uppsala University, Sweden) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p477-p doi:10.1145/3571251
	Cambronero, José	Proc. ACM Program. Lang., vol. 7, issue POPL: "FlashFill++: Scaling Programming ..." FlashFill++: Scaling Programming by Example by Cutting to the Chase José Cambronero, Sumit Gulwani, Vu Le, Daniel Perelman, Arjun Radhakrishna, Clint Simon, and Ashish Tiwari (Microsoft, USA) Publisher's Version Article: popl23main-p198-p doi:10.1145/3571226
	Cao, David	Proc. ACM Program. Lang., vol. 7, issue POPL: "babble: Learning Better Abstractions ..." babble: Learning Better Abstractions with E-Graphs and Anti-unification David Cao, Rose Kunkel, Chandrakana Nandi, Max Willsey, Zachary Tatlock, and Nadia Polikarpova (University of California at San Diego, USA; Certora, USA; University of Washington, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p94-p doi:10.1145/3571207
	Castegren, Elias	Proc. ACM Program. Lang., vol. 7, issue POPL: "Statically Resolvable Ambiguity ..." Statically Resolvable Ambiguity Viktor Palmkvist, Elias Castegren, Philipp Haller, and David Broman (KTH Royal Institute of Technology, Sweden; Uppsala University, Sweden) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p477-p doi:10.1145/3571251
	Castellan, Simon	Proc. ACM Program. Lang., vol. 7, issue POPL: "The Geometry of Causality: ..." The Geometry of Causality: Multi-token Geometry of Interaction and Its Causal Unfolding Simon Castellan and Pierre Clairambault (University of Rennes, France; Inria, France; CNRS, France; IRISA, France; Université Aix-Marseille, France; Université de Toulon, France; LIS, France) Publisher's Version Artifacts Functional Article: popl23main-p121-p doi:10.1145/3571217
	Chappe, Nicolas	Proc. ACM Program. Lang., vol. 7, issue POPL: "Choice Trees: Representing ..." Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, and Steve Zdancewic (University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, France; University of Pennsylvania, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p528-p doi:10.1145/3571254
	Charguéraud, Arthur	Proc. ACM Program. Lang., vol. 7, issue POPL: "A High-Level Separation Logic ..." A High-Level Separation Logic for Heap Space under Garbage Collection Alexandre Moine, Arthur Charguéraud, and François Pottier (Inria, France; Université de Strasbourg, France; CNRS, France; ICube, France) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p141-p doi:10.1145/3571218
	Chen, Yixuan	Proc. ACM Program. Lang., vol. 7, issue POPL: "A Compositional Theory of ..." A Compositional Theory of Linearizability Arthur Oliveira Vale, Zhong Shao, and Yixuan Chen (Yale University, USA) Publisher's Version Article: popl23main-p263-p doi:10.1145/3571231
	Chen, Zilin	Proc. ACM Program. Lang., vol. 7, issue POPL: "Dargent: A Silver Bullet for ..." Dargent: A Silver Bullet for Verified Data Layout Refinement Zilin Chen, Ambroise Lafont, Liam O'Connor, Gabriele Keller, Craig McLaughlin, Vincent Jackson, and Christine Rizkallah (UNSW, Australia; University of Cambridge, UK; University of Edinburgh, UK; Utrecht University, Netherlands; University of Melbourne, Australia) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p325-p doi:10.1145/3571240
	Cho, Hangyeol	Proc. ACM Program. Lang., vol. 7, issue POPL: "Inductive Synthesis of Structurally ..." Inductive Synthesis of Structurally Recursive Functional Programs from Non-recursive Expressions Woosuk Lee and Hangyeol Cho (Hanyang University, South Korea) Publisher's Version Published Artifact Archive submitted (710 kB) Artifacts Available Artifacts Reusable Article: popl23main-p658-p doi:10.1145/3571263
	Cho, Minki	Proc. ACM Program. Lang., vol. 7, issue POPL: "Conditional Contextual Refinement ..." Conditional Contextual Refinement Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Sammler, and Derek Dreyer (Seoul National University, South Korea; MPI-SWS, Germany) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p264-p doi:10.1145/3571232
	Chong, Stephen	Proc. ACM Program. Lang., vol. 7, issue POPL: "From SMT to ASP: Solver-Based ..." From SMT to ASP: Solver-Based Approaches to Solving Datalog Synthesis-as-Rule-Selection Problems Aaron Bembenek, Michael Greenberg, and Stephen Chong (Harvard University, USA; Stevens Institute of Technology, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p63-p doi:10.1145/3571200
	Clairambault, Pierre	Proc. ACM Program. Lang., vol. 7, issue POPL: "The Geometry of Causality: ..." The Geometry of Causality: Multi-token Geometry of Interaction and Its Causal Unfolding Simon Castellan and Pierre Clairambault (University of Rennes, France; Inria, France; CNRS, France; IRISA, France; Université Aix-Marseille, France; Université de Toulon, France; LIS, France) Publisher's Version Artifacts Functional Article: popl23main-p121-p doi:10.1145/3571217
	Clark, Jack	Proc. ACM Program. Lang., vol. 7, issue POPL: "Taking Back Control in an ..." Taking Back Control in an Intermediate Representation for GPU Computing Vasileios Klimis, Jack Clark, Alan Baker, David Neto, John Wickerson, and Alastair F. Donaldson (Imperial College London, UK; Google, Canada; Google, UK) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p511-p doi:10.1145/3571253
	D'Antoni, Loris	Proc. ACM Program. Lang., vol. 7, issue POPL: "Unrealizability Logic ..." Unrealizability Logic Jinwoo Kim, Loris D'Antoni, and Thomas Reps (University of Wisconsin-Madison, USA; Seoul National University, South Korea) Publisher's Version Article: popl23main-p120-p doi:10.1145/3571216
	Das, Ankush	Proc. ACM Program. Lang., vol. 7, issue POPL: "Probabilistic Resource-Aware ..." Probabilistic Resource-Aware Session Types Ankush Das, Di Wang, and Jan Hoffmann (Amazon, USA; Carnegie Mellon University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p590-p doi:10.1145/3571259
	Das, Ria	Proc. ACM Program. Lang., vol. 7, issue POPL: "Combining Functional and Automata ..." Combining Functional and Automata Synthesis to Discover Causal Reactive Programs Ria Das, Joshua B. Tenenbaum, Armando Solar-Lezama, and Zenna Tavares (Stanford University, USA; Massachusetts Institute of Technology, USA; Basis, USA; Columbia University, USA) Publisher's Version Archive submitted (780 kB) Article: popl23main-p449-p doi:10.1145/3571249
	Dash, Swaraj	Proc. ACM Program. Lang., vol. 7, issue POPL: "Affine Monads and Lazy Structures ..." Affine Monads and Lazy Structures for Bayesian Programming Swaraj Dash, Younesse Kaddar, Hugo Paquet, and Sam Staton (University of Oxford, UK) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p324-p doi:10.1145/3571239
	Day, Joel D.	Proc. ACM Program. Lang., vol. 7, issue POPL: "On the Expressive Power of ..." On the Expressive Power of String Constraints Joel D. Day, Vijay Ganesh, Nathan Grewal, and Florin Manea (Loughborough University, UK; University of Waterloo, Canada; University of Göttingen, Germany) Publisher's Version Article: popl23main-p75-p doi:10.1145/3571203
	Deep, Shaleen	Proc. ACM Program. Lang., vol. 7, issue POPL: "The Fine-Grained Complexity ..." The Fine-Grained Complexity of CFL Reachability Paraschos Koutris and Shaleen Deep (University of Wisconsin-Madison, USA; Microsoft, USA) Publisher's Version Article: popl23main-p490-p doi:10.1145/3571252
	Delaware, Benjamin	Proc. ACM Program. Lang., vol. 7, issue POPL: "A Type-Based Approach to Divide-and-Conquer ..." A Type-Based Approach to Divide-and-Conquer Recursion in Coq Pedro Abreu, Benjamin Delaware, Alex Hubers, Christa Jenkins, J. Garrett Morris, and Aaron Stump (Purdue University, USA; University of Iowa, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p17-p doi:10.1145/3571196
	Denlinger, Aidan	Proc. ACM Program. Lang., vol. 7, issue POPL: "MSWasm: Soundly Enforcing ..." MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code Alexandra E. Michael, Anitha Gollamudi, Jay Bosamiya, Evan Johnson, Aidan Denlinger, Craig Disselkoen, Conrad Watt, Bryan Parno, Marco Patrignani, Marco Vassena, and Deian Stefan (University of California at San Diego, USA; University of Washington, USA; University of Massachusetts Lowell, USA; Carnegie Mellon University, USA; Arm, USA; University of Cambridge, UK; University of Trento, Italy; Utrecht University, Netherlands) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl23main-p96-p doi:10.1145/3571208
	Di Florio, Cecilia	Proc. ACM Program. Lang., vol. 7, issue POPL: "Elements of Quantitative Rewriting ..." Elements of Quantitative Rewriting Francesco Gavazzo and Cecilia Di Florio (University of Pisa, Italy; University of Bologna, Italy) Publisher's Version Article: popl23main-p531-p doi:10.1145/3571256
	Di Giorgio, Alessandro	Proc. ACM Program. Lang., vol. 7, issue POPL: "Deconstructing the Calculus ..." Deconstructing the Calculus of Relations with Tape Diagrams Filippo Bonchi, Alessandro Di Giorgio, and Alessio Santamaria (University of Pisa, Italy; University of Sussex, UK) Publisher's Version Article: popl23main-p559-p doi:10.1145/3571257
	Di Giusto, Cinzia	Proc. ACM Program. Lang., vol. 7, issue POPL: "A Partial Order View of Message-Passing ..." A Partial Order View of Message-Passing Communication Models Cinzia Di Giusto, Davide Ferré, Laetitia Laversa, and Etienne Lozes (Université Côte d'Azur, France; CNRS, France) Publisher's Version Article: popl23main-p427-p doi:10.1145/3571248
	Ding, Shuo	Proc. ACM Program. Lang., vol. 7, issue POPL: "Witnessability of Undecidable ..." Witnessability of Undecidable Problems Shuo Ding and Qirun Zhang (Georgia Institute of Technology, USA) Publisher's Version Article: popl23main-p218-p doi:10.1145/3571227
	Disselkoen, Craig	Proc. ACM Program. Lang., vol. 7, issue POPL: "MSWasm: Soundly Enforcing ..." MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code Alexandra E. Michael, Anitha Gollamudi, Jay Bosamiya, Evan Johnson, Aidan Denlinger, Craig Disselkoen, Conrad Watt, Bryan Parno, Marco Patrignani, Marco Vassena, and Deian Stefan (University of California at San Diego, USA; University of Washington, USA; University of Massachusetts Lowell, USA; Carnegie Mellon University, USA; Arm, USA; University of Cambridge, UK; University of Trento, Italy; Utrecht University, Netherlands) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl23main-p96-p doi:10.1145/3571208
	Donaldson, Alastair F.	Proc. ACM Program. Lang., vol. 7, issue POPL: "Taking Back Control in an ..." Taking Back Control in an Intermediate Representation for GPU Computing Vasileios Klimis, Jack Clark, Alan Baker, David Neto, John Wickerson, and Alastair F. Donaldson (Imperial College London, UK; Google, Canada; Google, UK) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p511-p doi:10.1145/3571253
	D'Osualdo, Emanuele	Proc. ACM Program. Lang., vol. 7, issue POPL: "The Path to Durable Linearizability ..." The Path to Durable Linearizability Emanuele D'Osualdo, Azalea Raad, and Viktor Vafeiadis (MPI-SWS, Germany; Imperial College London, UK) Publisher's Version Article: popl23main-p144-p doi:10.1145/3571219 Proc. ACM Program. Lang., vol. 7, issue POPL: "DimSum: A Decentralized Approach ..." DimSum: A Decentralized Approach to Multi-language Semantics and Verification Michael Sammler, Simon Spies, Youngju Song, Emanuele D'Osualdo, Robbert Krebbers, Deepak Garg, and Derek Dreyer (MPI-SWS, Germany; Radboud University Nijmegen, Netherlands) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p145-p doi:10.1145/3571220
	Dreyer, Derek	Proc. ACM Program. Lang., vol. 7, issue POPL: "DimSum: A Decentralized Approach ..." DimSum: A Decentralized Approach to Multi-language Semantics and Verification Michael Sammler, Simon Spies, Youngju Song, Emanuele D'Osualdo, Robbert Krebbers, Deepak Garg, and Derek Dreyer (MPI-SWS, Germany; Radboud University Nijmegen, Netherlands) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p145-p doi:10.1145/3571220 Proc. ACM Program. Lang., vol. 7, issue POPL: "Conditional Contextual Refinement ..." Conditional Contextual Refinement Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Sammler, and Derek Dreyer (Seoul National University, South Korea; MPI-SWS, Germany) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p264-p doi:10.1145/3571232
	Ellis, Kevin	Proc. ACM Program. Lang., vol. 7, issue POPL: "Top-Down Synthesis for Library ..." Top-Down Synthesis for Library Learning Matthew Bowers, Theo X. Olausson, Lionel Wong, Gabriel Grand, Joshua B. Tenenbaum, Kevin Ellis, and Armando Solar-Lezama (Massachusetts Institute of Technology, USA; Cornell University, USA) Publisher's Version Published Artifact Archive submitted (1.6 MB) Artifacts Available Artifacts Reusable Article: popl23main-p278-p doi:10.1145/3571234
	Fan, Xiong	Proc. ACM Program. Lang., vol. 7, issue POPL: "A Core Calculus for Equational ..." A Core Calculus for Equational Proofs of Cryptographic Protocols Joshua Gancher, Kristina Sojakova, Xiong Fan, Elaine Shi, and Greg Morrisett (Carnegie Mellon University, USA; Inria, France; Rutgers University, USA; Cornell University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p185-p doi:10.1145/3571223
	Farzan, Azadeh	Proc. ACM Program. Lang., vol. 7, issue POPL: "Stratified Commutativity in ..." Stratified Commutativity in Verification Algorithms for Concurrent Programs Azadeh Farzan, Dominik Klumpp, and Andreas Podelski (University of Toronto, Canada; University of Freiburg, Germany) Publisher's Version Archive submitted (780 kB) Article: popl23main-p348-p doi:10.1145/3571242
	Ferré, Davide	Proc. ACM Program. Lang., vol. 7, issue POPL: "A Partial Order View of Message-Passing ..." A Partial Order View of Message-Passing Communication Models Cinzia Di Giusto, Davide Ferré, Laetitia Laversa, and Etienne Lozes (Université Côte d'Azur, France; CNRS, France) Publisher's Version Article: popl23main-p427-p doi:10.1145/3571248
	Frostig, Roy	Proc. ACM Program. Lang., vol. 7, issue POPL: "You Only Linearize Once: Tangents ..." You Only Linearize Once: Tangents Transpose to Gradients Alexey Radul, Adam Paszke, Roy Frostig, Matthew J. Johnson, and Dougal Maclaurin (Google Research, USA; Google Research, Poland) Publisher's Version Article: popl23main-p303-p doi:10.1145/3571236
	Fu, Peng	Proc. ACM Program. Lang., vol. 7, issue POPL: "Proto-Quipper with Dynamic ..." Proto-Quipper with Dynamic Lifting Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger (Dalhousie University, Canada; University of Illinois at Urbana-Champaign, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p79-p doi:10.1145/3571204
	Ganardi, Moses	Proc. ACM Program. Lang., vol. 7, issue POPL: "Context-Bounded Verification ..." Context-Bounded Verification of Context-Free Specifications Pascal Baumann, Moses Ganardi, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche (MPI-SWS, Germany) Publisher's Version Article: popl23main-p699-p doi:10.1145/3571266
	Gancher, Joshua	Proc. ACM Program. Lang., vol. 7, issue POPL: "A Core Calculus for Equational ..." A Core Calculus for Equational Proofs of Cryptographic Protocols Joshua Gancher, Kristina Sojakova, Xiong Fan, Elaine Shi, and Greg Morrisett (Carnegie Mellon University, USA; Inria, France; Rutgers University, USA; Cornell University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p185-p doi:10.1145/3571223
	Ganesh, Vijay	Proc. ACM Program. Lang., vol. 7, issue POPL: "On the Expressive Power of ..." On the Expressive Power of String Constraints Joel D. Day, Vijay Ganesh, Nathan Grewal, and Florin Manea (Loughborough University, UK; University of Waterloo, Canada; University of Göttingen, Germany) Publisher's Version Article: popl23main-p75-p doi:10.1145/3571203
	Garg, Deepak	Proc. ACM Program. Lang., vol. 7, issue POPL: "DimSum: A Decentralized Approach ..." DimSum: A Decentralized Approach to Multi-language Semantics and Verification Michael Sammler, Simon Spies, Youngju Song, Emanuele D'Osualdo, Robbert Krebbers, Deepak Garg, and Derek Dreyer (MPI-SWS, Germany; Radboud University Nijmegen, Netherlands) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p145-p doi:10.1145/3571220
	Gavazzo, Francesco	Proc. ACM Program. Lang., vol. 7, issue POPL: "Elements of Quantitative Rewriting ..." Elements of Quantitative Rewriting Francesco Gavazzo and Cecilia Di Florio (University of Pisa, Italy; University of Bologna, Italy) Publisher's Version Article: popl23main-p531-p doi:10.1145/3571256
	Gollamudi, Anitha	Proc. ACM Program. Lang., vol. 7, issue POPL: "MSWasm: Soundly Enforcing ..." MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code Alexandra E. Michael, Anitha Gollamudi, Jay Bosamiya, Evan Johnson, Aidan Denlinger, Craig Disselkoen, Conrad Watt, Bryan Parno, Marco Patrignani, Marco Vassena, and Deian Stefan (University of California at San Diego, USA; University of Washington, USA; University of Massachusetts Lowell, USA; Carnegie Mellon University, USA; Arm, USA; University of Cambridge, UK; University of Trento, Italy; Utrecht University, Netherlands) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl23main-p96-p doi:10.1145/3571208
	Goncharov, Sergey	Proc. ACM Program. Lang., vol. 7, issue POPL: "Towards a Higher-Order Mathematical ..." Towards a Higher-Order Mathematical Operational Semantics Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat (University of Erlangen-Nuremberg, Germany) Publisher's Version Article: popl23main-p119-p doi:10.1145/3571215
	Grand, Gabriel	Proc. ACM Program. Lang., vol. 7, issue POPL: "Top-Down Synthesis for Library ..." Top-Down Synthesis for Library Learning Matthew Bowers, Theo X. Olausson, Lionel Wong, Gabriel Grand, Joshua B. Tenenbaum, Kevin Ellis, and Armando Solar-Lezama (Massachusetts Institute of Technology, USA; Cornell University, USA) Publisher's Version Published Artifact Archive submitted (1.6 MB) Artifacts Available Artifacts Reusable Article: popl23main-p278-p doi:10.1145/3571234
	Greenberg, Michael	Proc. ACM Program. Lang., vol. 7, issue POPL: "From SMT to ASP: Solver-Based ..." From SMT to ASP: Solver-Based Approaches to Solving Datalog Synthesis-as-Rule-Selection Problems Aaron Bembenek, Michael Greenberg, and Stephen Chong (Harvard University, USA; Stevens Institute of Technology, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p63-p doi:10.1145/3571200
	Grewal, Nathan	Proc. ACM Program. Lang., vol. 7, issue POPL: "On the Expressive Power of ..." On the Expressive Power of String Constraints Joel D. Day, Vijay Ganesh, Nathan Grewal, and Florin Manea (Loughborough University, UK; University of Waterloo, Canada; University of Göttingen, Germany) Publisher's Version Article: popl23main-p75-p doi:10.1145/3571203
	Gu, Yu	Proc. ACM Program. Lang., vol. 7, issue POPL: "Optimal CHC Solving via Termination ..." Optimal CHC Solving via Termination Proofs Yu Gu, Takeshi Tsukada, and Hiroshi Unno (University of Tsukuba, Japan; Chiba University, Japan; RIKEN AIP, Japan) Publisher's Version Article: popl23main-p115-p doi:10.1145/3571214 Proc. ACM Program. Lang., vol. 7, issue POPL: "Modular Primal-Dual Fixpoint ..." Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinen (University of Tsukuba, Japan; RIKEN AIP, Japan; Waseda University, Japan; Stevens Institute of Technology, USA) Publisher's Version Article: popl23main-p691-p doi:10.1145/3571265
	Guerrieri, Giulio	Proc. ACM Program. Lang., vol. 7, issue POPL: "Quantitative Inhabitation ..." Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework Victor Arrial, Giulio Guerrieri, and Delia Kesner (Université Paris Cité - CNRS - IRIF, France; Aix Marseille Université - CNRS - LIS, France; Edinburgh Research Centre - Central Software Institute - Huawei, UK; Institut Universitaire de France, France) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p365-p doi:10.1145/3571244
	Gulwani, Sumit	Proc. ACM Program. Lang., vol. 7, issue POPL: "FlashFill++: Scaling Programming ..." FlashFill++: Scaling Programming by Example by Cutting to the Chase José Cambronero, Sumit Gulwani, Vu Le, Daniel Perelman, Arjun Radhakrishna, Clint Simon, and Ashish Tiwari (Microsoft, USA) Publisher's Version Article: popl23main-p198-p doi:10.1145/3571226
	Hainry, Emmanuel	Proc. ACM Program. Lang., vol. 7, issue POPL: "A General Noninterference ..." A General Noninterference Policy for Polynomial Time Emmanuel Hainry and Romain Péchoux (Université de Lorraine, France; CNRS, France; Inria, France; LORIA, France) Publisher's Version Article: popl23main-p149-p doi:10.1145/3571221
	Haller, Philipp	Proc. ACM Program. Lang., vol. 7, issue POPL: "Statically Resolvable Ambiguity ..." Statically Resolvable Ambiguity Viktor Palmkvist, Elias Castegren, Philipp Haller, and David Broman (KTH Royal Institute of Technology, Sweden; Uppsala University, Sweden) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p477-p doi:10.1145/3571251
	He, Paul	Proc. ACM Program. Lang., vol. 7, issue POPL: "Choice Trees: Representing ..." Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, and Steve Zdancewic (University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, France; University of Pennsylvania, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p528-p doi:10.1145/3571254
	Henrio, Ludovic	Proc. ACM Program. Lang., vol. 7, issue POPL: "Choice Trees: Representing ..." Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, and Steve Zdancewic (University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, France; University of Pennsylvania, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p528-p doi:10.1145/3571254
	Hicks, Michael	Proc. ACM Program. Lang., vol. 7, issue POPL: "Qunity: A Unified Language ..." Qunity: A Unified Language for Quantum and Classical Computing Finn Voichick, Liyi Li, Robert Rand, and Michael Hicks (University of Maryland, USA; University of Chicago, USA; Amazon, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p197-p doi:10.1145/3571225
	Hoffmann, Jan	Proc. ACM Program. Lang., vol. 7, issue POPL: "Probabilistic Resource-Aware ..." Probabilistic Resource-Aware Session Types Ankush Das, Di Wang, and Jan Hoffmann (Amazon, USA; Carnegie Mellon University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p590-p doi:10.1145/3571259
	Hou (Favonia), Kuen-Bang	Proc. ACM Program. Lang., vol. 7, issue POPL: "An Order-Theoretic Analysis ..." An Order-Theoretic Analysis of Universe Polymorphism Kuen-Bang Hou (Favonia), Carlo Angiuli, and Reed Mullanix (University of Minnesota, USA; Carnegie Mellon University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p471-p doi:10.1145/3571250
	Huang, Xuejing	Proc. ACM Program. Lang., vol. 7, issue POPL: "A Bowtie for a Beast: Overloading, ..." A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F⋈ Nick Rioux, Xuejing Huang, Bruno C. d. S. Oliveira, and Steve Zdancewic (University of Pennsylvania, USA; University of Hong Kong, China) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p111-p doi:10.1145/3571211 Proc. ACM Program. Lang., vol. 7, issue POPL: "Making a Type Difference: ..." Making a Type Difference: Subtraction on Intersection Types as Generalized Record Operations Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira (Peking University, China; University of Hong Kong, China) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p191-p doi:10.1145/3571224
	Hubers, Alex	Proc. ACM Program. Lang., vol. 7, issue POPL: "A Type-Based Approach to Divide-and-Conquer ..." A Type-Based Approach to Divide-and-Conquer Recursion in Coq Pedro Abreu, Benjamin Delaware, Alex Hubers, Christa Jenkins, J. Garrett Morris, and Aaron Stump (Purdue University, USA; University of Iowa, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p17-p doi:10.1145/3571196
	Hunt, Sebastian	Proc. ACM Program. Lang., vol. 7, issue POPL: "Reconciling Shannon and Scott ..." Reconciling Shannon and Scott with a Lattice of Computable Information Sebastian Hunt, David Sands, and Sandro Stucki (City University of London, UK; Chalmers University of Technology, Sweden; Amazon Prime Video, Sweden) Publisher's Version Article: popl23main-p600-p doi:10.1145/3571740
	Huot, Mathieu	Proc. ACM Program. Lang., vol. 7, issue POPL: "ADEV: Sound Automatic Differentiation ..." ADEV: Sound Automatic Differentiation of Expected Values of Probabilistic Programs Alexander K. Lew, Mathieu Huot, Sam Staton, and Vikash K. Mansinghka (Massachusetts Institute of Technology, USA; University of Oxford, UK) Publisher's Version Archive submitted (1 MB) Article: popl23main-p48-p doi:10.1145/3571198
	Hur, Chung-Kil	Proc. ACM Program. Lang., vol. 7, issue POPL: "Conditional Contextual Refinement ..." Conditional Contextual Refinement Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Sammler, and Derek Dreyer (Seoul National University, South Korea; MPI-SWS, Germany) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p264-p doi:10.1145/3571232
	Jackson, Vincent	Proc. ACM Program. Lang., vol. 7, issue POPL: "Dargent: A Silver Bullet for ..." Dargent: A Silver Bullet for Verified Data Layout Refinement Zilin Chen, Ambroise Lafont, Liam O'Connor, Gabriele Keller, Craig McLaughlin, Vincent Jackson, and Christine Rizkallah (UNSW, Australia; University of Cambridge, UK; University of Edinburgh, UK; Utrecht University, Netherlands; University of Melbourne, Australia) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p325-p doi:10.1145/3571240
	Jacobs, Jules	Proc. ACM Program. Lang., vol. 7, issue POPL: "Higher-Order Leak and Deadlock ..." Higher-Order Leak and Deadlock Free Locks Jules Jacobs and Stephanie Balzer (Radboud University Nijmegen, Netherlands; Carnegie Mellon University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p231-p doi:10.1145/3571229 Proc. ACM Program. Lang., vol. 7, issue POPL: "Fast Coalgebraic Bisimilarity ..." Fast Coalgebraic Bisimilarity Minimization Jules Jacobs and Thorsten Wißmann (Radboud University Nijmegen, Netherlands) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl23main-p373-p doi:10.1145/3571245
	Jenkins, Christa	Proc. ACM Program. Lang., vol. 7, issue POPL: "A Type-Based Approach to Divide-and-Conquer ..." A Type-Based Approach to Divide-and-Conquer Recursion in Coq Pedro Abreu, Benjamin Delaware, Alex Hubers, Christa Jenkins, J. Garrett Morris, and Aaron Stump (Purdue University, USA; University of Iowa, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p17-p doi:10.1145/3571196
	Jiang, Chuan	Proc. ACM Program. Lang., vol. 7, issue POPL: "Comparative Synthesis: Learning ..." Comparative Synthesis: Learning Near-Optimal Network Designs by Query Yanjun Wang, Zixuan Li, Chuan Jiang, Xiaokang Qiu, and Sanjay Rao (Purdue University, USA) Publisher's Version Archive submitted (1.3 MB) Artifacts Functional Article: popl23main-p33-p doi:10.1145/3571197
	Jochems, Jerome	Proc. ACM Program. Lang., vol. 7, issue POPL: "Higher-Order MSL Horn Constraints ..." Higher-Order MSL Horn Constraints Jerome Jochems, Eddie Jones, and Steven Ramsay (University of Bristol, UK) Publisher's Version Article: popl23main-p650-p doi:10.1145/3571262
	Johnson, Evan	Proc. ACM Program. Lang., vol. 7, issue POPL: "MSWasm: Soundly Enforcing ..." MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code Alexandra E. Michael, Anitha Gollamudi, Jay Bosamiya, Evan Johnson, Aidan Denlinger, Craig Disselkoen, Conrad Watt, Bryan Parno, Marco Patrignani, Marco Vassena, and Deian Stefan (University of California at San Diego, USA; University of Washington, USA; University of Massachusetts Lowell, USA; Carnegie Mellon University, USA; Arm, USA; University of Cambridge, UK; University of Trento, Italy; Utrecht University, Netherlands) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl23main-p96-p doi:10.1145/3571208
	Johnson, Matthew J.	Proc. ACM Program. Lang., vol. 7, issue POPL: "You Only Linearize Once: Tangents ..." You Only Linearize Once: Tangents Transpose to Gradients Alexey Radul, Adam Paszke, Roy Frostig, Matthew J. Johnson, and Dougal Maclaurin (Google Research, USA; Google Research, Poland) Publisher's Version Article: popl23main-p303-p doi:10.1145/3571236
	Jones, Eddie	Proc. ACM Program. Lang., vol. 7, issue POPL: "Higher-Order MSL Horn Constraints ..." Higher-Order MSL Horn Constraints Jerome Jochems, Eddie Jones, and Steven Ramsay (University of Bristol, UK) Publisher's Version Article: popl23main-p650-p doi:10.1145/3571262
	Kaddar, Younesse	Proc. ACM Program. Lang., vol. 7, issue POPL: "Affine Monads and Lazy Structures ..." Affine Monads and Lazy Structures for Bayesian Programming Swaraj Dash, Younesse Kaddar, Hugo Paquet, and Sam Staton (University of Oxford, UK) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p324-p doi:10.1145/3571239
	Kallas, Konstantinos	Proc. ACM Program. Lang., vol. 7, issue POPL: "Executing Microservice Applications ..." Executing Microservice Applications on Serverless, Correctly Konstantinos Kallas, Haoran Zhang, Rajeev Alur, Sebastian Angel, and Vincent Liu (University of Pennsylvania, USA; Microsoft Research, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl23main-p93-p doi:10.1145/3571206
	Kaminski, Benjamin Lucien	Proc. ACM Program. Lang., vol. 7, issue POPL: "A Calculus for Amortized Expected ..." A Calculus for Amortized Expected Runtimes Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Lena Verscht (RWTH Aachen University, Germany; Saarland University, Germany; University College London, UK; DTU, Denmark) Publisher's Version Article: popl23main-p592-p doi:10.1145/3571260
	Katoen, Joost-Pieter	Proc. ACM Program. Lang., vol. 7, issue POPL: "A Calculus for Amortized Expected ..." A Calculus for Amortized Expected Runtimes Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Lena Verscht (RWTH Aachen University, Germany; Saarland University, Germany; University College London, UK; DTU, Denmark) Publisher's Version Article: popl23main-p592-p doi:10.1145/3571260
	Keller, Gabriele	Proc. ACM Program. Lang., vol. 7, issue POPL: "Dargent: A Silver Bullet for ..." Dargent: A Silver Bullet for Verified Data Layout Refinement Zilin Chen, Ambroise Lafont, Liam O'Connor, Gabriele Keller, Craig McLaughlin, Vincent Jackson, and Christine Rizkallah (UNSW, Australia; University of Cambridge, UK; University of Edinburgh, UK; Utrecht University, Netherlands; University of Melbourne, Australia) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p325-p doi:10.1145/3571240
	Kerinec, Axel	Proc. ACM Program. Lang., vol. 7, issue POPL: "Why Are Proofs Relevant in ..." Why Are Proofs Relevant in Proof-Relevant Models? Axel Kerinec, Giulio Manzonetto, and Federico Olimpieri (Université Sorbonne Paris Nord, France; LIPN, France; CNRS, France; University of Leeds, UK) Publisher's Version Article: popl23main-p66-p doi:10.1145/3571201
	Kesner, Delia	Proc. ACM Program. Lang., vol. 7, issue POPL: "Quantitative Inhabitation ..." Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework Victor Arrial, Giulio Guerrieri, and Delia Kesner (Université Paris Cité - CNRS - IRIF, France; Aix Marseille Université - CNRS - LIS, France; Edinburgh Research Centre - Central Software Institute - Huawei, UK; Institut Universitaire de France, France) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p365-p doi:10.1145/3571244
	Kim, Jinwoo	Proc. ACM Program. Lang., vol. 7, issue POPL: "Unrealizability Logic ..." Unrealizability Logic Jinwoo Kim, Loris D'Antoni, and Thomas Reps (University of Wisconsin-Madison, USA; Seoul National University, South Korea) Publisher's Version Article: popl23main-p120-p doi:10.1145/3571216
	Kincaid, Zachary	Proc. ACM Program. Lang., vol. 7, issue POPL: "When Less Is More: Consequence-Finding ..." When Less Is More: Consequence-Finding in a Weak Theory of Arithmetic Zachary Kincaid, Nicolas Koh, and Shaowei Zhu (Princeton University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p305-p doi:10.1145/3571237
	Kishida, Kohei	Proc. ACM Program. Lang., vol. 7, issue POPL: "Proto-Quipper with Dynamic ..." Proto-Quipper with Dynamic Lifting Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger (Dalhousie University, Canada; University of Illinois at Urbana-Champaign, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p79-p doi:10.1145/3571204
	Klimis, Vasileios	Proc. ACM Program. Lang., vol. 7, issue POPL: "Taking Back Control in an ..." Taking Back Control in an Intermediate Representation for GPU Computing Vasileios Klimis, Jack Clark, Alan Baker, David Neto, John Wickerson, and Alastair F. Donaldson (Imperial College London, UK; Google, Canada; Google, UK) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p511-p doi:10.1145/3571253
	Klumpp, Dominik	Proc. ACM Program. Lang., vol. 7, issue POPL: "Stratified Commutativity in ..." Stratified Commutativity in Verification Algorithms for Concurrent Programs Azadeh Farzan, Dominik Klumpp, and Andreas Podelski (University of Toronto, Canada; University of Freiburg, Germany) Publisher's Version Archive submitted (780 kB) Article: popl23main-p348-p doi:10.1145/3571242
	Kobayashi, Naoki	Proc. ACM Program. Lang., vol. 7, issue POPL: "HFL(Z) Validity Checking for ..." HFL(Z) Validity Checking for Automated Program Verification Naoki Kobayashi, Kento Tanahashi, Ryosuke Sato, and Takeshi Tsukada (University of Tokyo, Japan; Chiba University, Japan) Publisher's Version Article: popl23main-p55-p doi:10.1145/3571199
	Koh, Nicolas	Proc. ACM Program. Lang., vol. 7, issue POPL: "When Less Is More: Consequence-Finding ..." When Less Is More: Consequence-Finding in a Weak Theory of Arithmetic Zachary Kincaid, Nicolas Koh, and Shaowei Zhu (Princeton University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p305-p doi:10.1145/3571237
	Kokologiannakis, Michalis	Proc. ACM Program. Lang., vol. 7, issue POPL: "Kater: Automating Weak Memory ..." Kater: Automating Weak Memory Model Metatheory and Consistency Checking Michalis Kokologiannakis, Ori Lahav, and Viktor Vafeiadis (MPI-SWS, Germany; Tel Aviv University, Israel) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p112-p doi:10.1145/3571212
	Koskinen, Eric	Proc. ACM Program. Lang., vol. 7, issue POPL: "An Algebra of Alignment for ..." An Algebra of Alignment for Relational Verification Timos Antonopoulos, Eric Koskinen, Ton Chanh Le, Ramana Nagasamudram, David A. Naumann, and Minh Ngo (Yale University, USA; Stevens Institute of Technology, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p114-p doi:10.1145/3571213 Proc. ACM Program. Lang., vol. 7, issue POPL: "Modular Primal-Dual Fixpoint ..." Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinen (University of Tsukuba, Japan; RIKEN AIP, Japan; Waseda University, Japan; Stevens Institute of Technology, USA) Publisher's Version Article: popl23main-p691-p doi:10.1145/3571265
	Koutris, Paraschos	Proc. ACM Program. Lang., vol. 7, issue POPL: "The Fine-Grained Complexity ..." The Fine-Grained Complexity of CFL Reachability Paraschos Koutris and Shaleen Deep (University of Wisconsin-Madison, USA; Microsoft, USA) Publisher's Version Article: popl23main-p490-p doi:10.1145/3571252
	Krebbers, Robbert	Proc. ACM Program. Lang., vol. 7, issue POPL: "DimSum: A Decentralized Approach ..." DimSum: A Decentralized Approach to Multi-language Semantics and Verification Michael Sammler, Simon Spies, Youngju Song, Emanuele D'Osualdo, Robbert Krebbers, Deepak Garg, and Derek Dreyer (MPI-SWS, Germany; Radboud University Nijmegen, Netherlands) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p145-p doi:10.1145/3571220
	Krishnaswami, Neel	Proc. ACM Program. Lang., vol. 7, issue POPL: "CN: Verifying Systems C Code ..." CN: Verifying Systems C Code with Separation-Logic Refinement Types Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, and Neel Krishnaswami (University of Cambridge, UK) Publisher's Version Article: popl23main-p2-p doi:10.1145/3571194
	Kunkel, Rose	Proc. ACM Program. Lang., vol. 7, issue POPL: "babble: Learning Better Abstractions ..." babble: Learning Better Abstractions with E-Graphs and Anti-unification David Cao, Rose Kunkel, Chandrakana Nandi, Max Willsey, Zachary Tatlock, and Nadia Polikarpova (University of California at San Diego, USA; Certora, USA; University of Washington, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p94-p doi:10.1145/3571207
	Lafont, Ambroise	Proc. ACM Program. Lang., vol. 7, issue POPL: "Dargent: A Silver Bullet for ..." Dargent: A Silver Bullet for Verified Data Layout Refinement Zilin Chen, Ambroise Lafont, Liam O'Connor, Gabriele Keller, Craig McLaughlin, Vincent Jackson, and Christine Rizkallah (UNSW, Australia; University of Cambridge, UK; University of Edinburgh, UK; Utrecht University, Netherlands; University of Melbourne, Australia) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p325-p doi:10.1145/3571240
	Lahav, Ori	Proc. ACM Program. Lang., vol. 7, issue POPL: "Kater: Automating Weak Memory ..." Kater: Automating Weak Memory Model Metatheory and Consistency Checking Michalis Kokologiannakis, Ori Lahav, and Viktor Vafeiadis (MPI-SWS, Germany; Tel Aviv University, Israel) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p112-p doi:10.1145/3571212 Proc. ACM Program. Lang., vol. 7, issue POPL: "An Operational Approach to ..." An Operational Approach to Library Abstraction under Relaxed Memory Concurrency Abhishek Kr Singh and Ori Lahav (Tel Aviv University, Israel) Publisher's Version Article: popl23main-p380-p doi:10.1145/3571246
	Laversa, Laetitia	Proc. ACM Program. Lang., vol. 7, issue POPL: "A Partial Order View of Message-Passing ..." A Partial Order View of Message-Passing Communication Models Cinzia Di Giusto, Davide Ferré, Laetitia Laversa, and Etienne Lozes (Université Côte d'Azur, France; CNRS, France) Publisher's Version Article: popl23main-p427-p doi:10.1145/3571248
	Le, Ton Chanh	Proc. ACM Program. Lang., vol. 7, issue POPL: "An Algebra of Alignment for ..." An Algebra of Alignment for Relational Verification Timos Antonopoulos, Eric Koskinen, Ton Chanh Le, Ramana Nagasamudram, David A. Naumann, and Minh Ngo (Yale University, USA; Stevens Institute of Technology, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p114-p doi:10.1145/3571213
	Le, Vu	Proc. ACM Program. Lang., vol. 7, issue POPL: "FlashFill++: Scaling Programming ..." FlashFill++: Scaling Programming by Example by Cutting to the Chase José Cambronero, Sumit Gulwani, Vu Le, Daniel Perelman, Arjun Radhakrishna, Clint Simon, and Ashish Tiwari (Microsoft, USA) Publisher's Version Article: popl23main-p198-p doi:10.1145/3571226
	Lee, Dongjae	Proc. ACM Program. Lang., vol. 7, issue POPL: "Conditional Contextual Refinement ..." Conditional Contextual Refinement Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Sammler, and Derek Dreyer (Seoul National University, South Korea; MPI-SWS, Germany) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p264-p doi:10.1145/3571232
	Lee, Wonyeol	Proc. ACM Program. Lang., vol. 7, issue POPL: "Smoothness Analysis for Probabilistic ..." Smoothness Analysis for Probabilistic Programs with Application to Optimised Variational Inference Wonyeol Lee, Xavier Rival, and Hongseok Yang (Stanford University, USA; Inria, France; ENS, France; CNRS, France; PSL University, France; KAIST, South Korea; IBS, South Korea) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p85-p doi:10.1145/3571205
	Lee, Woosuk	Proc. ACM Program. Lang., vol. 7, issue POPL: "Inductive Synthesis of Structurally ..." Inductive Synthesis of Structurally Recursive Functional Programs from Non-recursive Expressions Woosuk Lee and Hangyeol Cho (Hanyang University, South Korea) Publisher's Version Published Artifact Archive submitted (710 kB) Artifacts Available Artifacts Reusable Article: popl23main-p658-p doi:10.1145/3571263
	Leijen, Daan	Proc. ACM Program. Lang., vol. 7, issue POPL: "Tail Recursion Modulo Context: ..." Tail Recursion Modulo Context: An Equational Approach Daan Leijen and Anton Lorenzen (Microsoft Research, USA; University of Edinburgh, UK) Publisher's Version Article: popl23main-p271-p doi:10.1145/3571233
	Lemerre, Matthieu	Proc. ACM Program. Lang., vol. 7, issue POPL: "SSA Translation Is an Abstract ..." SSA Translation Is an Abstract Interpretation Matthieu Lemerre (Université Paris-Saclay - CEA LIST, France) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p570-p doi:10.1145/3571258
	Lew, Alexander K.	Proc. ACM Program. Lang., vol. 7, issue POPL: "ADEV: Sound Automatic Differentiation ..." ADEV: Sound Automatic Differentiation of Expected Values of Probabilistic Programs Alexander K. Lew, Mathieu Huot, Sam Staton, and Vikash K. Mansinghka (Massachusetts Institute of Technology, USA; University of Oxford, UK) Publisher's Version Archive submitted (1 MB) Article: popl23main-p48-p doi:10.1145/3571198
	Li, Jianlin	Proc. ACM Program. Lang., vol. 7, issue POPL: "Type-Preserving, Dependence-Aware ..." Type-Preserving, Dependence-Aware Guide Generation for Sound, Effective Amortized Probabilistic Inference Jianlin Li, Leni Ven, Pengyuan Shi, and Yizhou Zhang (University of Waterloo, Canada) Publisher's Version Article: popl23main-p354-p doi:10.1145/3571243
	Li, Liyi	Proc. ACM Program. Lang., vol. 7, issue POPL: "Qunity: A Unified Language ..." Qunity: A Unified Language for Quantum and Classical Computing Finn Voichick, Liyi Li, Robert Rand, and Michael Hicks (University of Maryland, USA; University of Chicago, USA; Amazon, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p197-p doi:10.1145/3571225
	Li, Yuanbo	Proc. ACM Program. Lang., vol. 7, issue POPL: "Single-Source-Single-Target ..." Single-Source-Single-Target Interleaved-Dyck Reachability via Integer Linear Programming Yuanbo Li, Qirun Zhang, and Thomas Reps (Georgia Institute of Technology, USA; University of Wisconsin-Madison, USA) Publisher's Version Article: popl23main-p222-p doi:10.1145/3571228
	Li, Zixuan	Proc. ACM Program. Lang., vol. 7, issue POPL: "Comparative Synthesis: Learning ..." Comparative Synthesis: Learning Near-Optimal Network Designs by Query Yanjun Wang, Zixuan Li, Chuan Jiang, Xiaokang Qiu, and Sanjay Rao (Purdue University, USA) Publisher's Version Archive submitted (1.3 MB) Artifacts Functional Article: popl23main-p33-p doi:10.1145/3571197
	Liu, Junyi	Proc. ACM Program. Lang., vol. 7, issue POPL: "CoqQ: Foundational Verification ..." CoqQ: Foundational Verification of Quantum Programs Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, and Mingsheng Ying (MPI-SP, Germany; Institute of Software at Chinese Academy of Sciences, China; IMDEA Software Institute, Spain; Meta, France; University of Chinese Academy of Sciences, China; Tsinghua University, China) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p163-p doi:10.1145/3571222
	Liu, Vincent	Proc. ACM Program. Lang., vol. 7, issue POPL: "Executing Microservice Applications ..." Executing Microservice Applications on Serverless, Correctly Konstantinos Kallas, Haoran Zhang, Rajeev Alur, Sebastian Angel, and Vincent Liu (University of Pennsylvania, USA; Microsoft Research, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl23main-p93-p doi:10.1145/3571206
	Lorenzen, Anton	Proc. ACM Program. Lang., vol. 7, issue POPL: "Tail Recursion Modulo Context: ..." Tail Recursion Modulo Context: An Equational Approach Daan Leijen and Anton Lorenzen (Microsoft Research, USA; University of Edinburgh, UK) Publisher's Version Article: popl23main-p271-p doi:10.1145/3571233
	Lozes, Etienne	Proc. ACM Program. Lang., vol. 7, issue POPL: "A Partial Order View of Message-Passing ..." A Partial Order View of Message-Passing Communication Models Cinzia Di Giusto, Davide Ferré, Laetitia Laversa, and Etienne Lozes (Université Côte d'Azur, France; CNRS, France) Publisher's Version Article: popl23main-p427-p doi:10.1145/3571248
	Lu, Sirui	Proc. ACM Program. Lang., vol. 7, issue POPL: "Grisette: Symbolic Compilation ..." Grisette: Symbolic Compilation as a Functional Programming Library Sirui Lu and Rastislav Bodík (University of Washington, USA; Google Research, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p97-p doi:10.1145/3571209
	Maclaurin, Dougal	Proc. ACM Program. Lang., vol. 7, issue POPL: "You Only Linearize Once: Tangents ..." You Only Linearize Once: Tangents Transpose to Gradients Alexey Radul, Adam Paszke, Roy Frostig, Matthew J. Johnson, and Dougal Maclaurin (Google Research, USA; Google Research, Poland) Publisher's Version Article: popl23main-p303-p doi:10.1145/3571236
	Majumdar, Rupak	Proc. ACM Program. Lang., vol. 7, issue POPL: "Context-Bounded Verification ..." Context-Bounded Verification of Context-Free Specifications Pascal Baumann, Moses Ganardi, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche (MPI-SWS, Germany) Publisher's Version Article: popl23main-p699-p doi:10.1145/3571266
	Makwana, Dhruv C.	Proc. ACM Program. Lang., vol. 7, issue POPL: "CN: Verifying Systems C Code ..." CN: Verifying Systems C Code with Separation-Logic Refinement Types Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, and Neel Krishnaswami (University of Cambridge, UK) Publisher's Version Article: popl23main-p2-p doi:10.1145/3571194
	Manea, Florin	Proc. ACM Program. Lang., vol. 7, issue POPL: "On the Expressive Power of ..." On the Expressive Power of String Constraints Joel D. Day, Vijay Ganesh, Nathan Grewal, and Florin Manea (Loughborough University, UK; University of Waterloo, Canada; University of Göttingen, Germany) Publisher's Version Article: popl23main-p75-p doi:10.1145/3571203
	Mansinghka, Vikash K.	Proc. ACM Program. Lang., vol. 7, issue POPL: "ADEV: Sound Automatic Differentiation ..." ADEV: Sound Automatic Differentiation of Expected Values of Probabilistic Programs Alexander K. Lew, Mathieu Huot, Sam Staton, and Vikash K. Mansinghka (Massachusetts Institute of Technology, USA; University of Oxford, UK) Publisher's Version Archive submitted (1 MB) Article: popl23main-p48-p doi:10.1145/3571198
	Manzonetto, Giulio	Proc. ACM Program. Lang., vol. 7, issue POPL: "Why Are Proofs Relevant in ..." Why Are Proofs Relevant in Proof-Relevant Models? Axel Kerinec, Giulio Manzonetto, and Federico Olimpieri (Université Sorbonne Paris Nord, France; LIPN, France; CNRS, France; University of Leeds, UK) Publisher's Version Article: popl23main-p66-p doi:10.1145/3571201
	Matheja, Christoph	Proc. ACM Program. Lang., vol. 7, issue POPL: "A Calculus for Amortized Expected ..." A Calculus for Amortized Expected Runtimes Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Lena Verscht (RWTH Aachen University, Germany; Saarland University, Germany; University College London, UK; DTU, Denmark) Publisher's Version Article: popl23main-p592-p doi:10.1145/3571260
	Mathur, Umang	Proc. ACM Program. Lang., vol. 7, issue POPL: "Dynamic Race Detection with ..." Dynamic Race Detection with O(1) Samples Mosaad Al Thokair, Minjian Zhang, Umang Mathur, and Mahesh Viswanathan (University of Illinois at Urbana-Champaign, USA; National University of Singapore, Singapore) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p314-p doi:10.1145/3571238
	McLaughlin, Craig	Proc. ACM Program. Lang., vol. 7, issue POPL: "Dargent: A Silver Bullet for ..." Dargent: A Silver Bullet for Verified Data Layout Refinement Zilin Chen, Ambroise Lafont, Liam O'Connor, Gabriele Keller, Craig McLaughlin, Vincent Jackson, and Christine Rizkallah (UNSW, Australia; University of Cambridge, UK; University of Edinburgh, UK; Utrecht University, Netherlands; University of Melbourne, Australia) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p325-p doi:10.1145/3571240
	Memarian, Kayvan	Proc. ACM Program. Lang., vol. 7, issue POPL: "CN: Verifying Systems C Code ..." CN: Verifying Systems C Code with Separation-Logic Refinement Types Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, and Neel Krishnaswami (University of Cambridge, UK) Publisher's Version Article: popl23main-p2-p doi:10.1145/3571194
	Michael, Alexandra E.	Proc. ACM Program. Lang., vol. 7, issue POPL: "MSWasm: Soundly Enforcing ..." MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code Alexandra E. Michael, Anitha Gollamudi, Jay Bosamiya, Evan Johnson, Aidan Denlinger, Craig Disselkoen, Conrad Watt, Bryan Parno, Marco Patrignani, Marco Vassena, and Deian Stefan (University of California at San Diego, USA; University of Washington, USA; University of Massachusetts Lowell, USA; Carnegie Mellon University, USA; Arm, USA; University of Cambridge, UK; University of Trento, Italy; Utrecht University, Netherlands) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl23main-p96-p doi:10.1145/3571208
	Milius, Stefan	Proc. ACM Program. Lang., vol. 7, issue POPL: "Towards a Higher-Order Mathematical ..." Towards a Higher-Order Mathematical Operational Semantics Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat (University of Erlangen-Nuremberg, Germany) Publisher's Version Article: popl23main-p119-p doi:10.1145/3571215
	Moine, Alexandre	Proc. ACM Program. Lang., vol. 7, issue POPL: "A High-Level Separation Logic ..." A High-Level Separation Logic for Heap Space under Garbage Collection Alexandre Moine, Arthur Charguéraud, and François Pottier (Inria, France; Université de Strasbourg, France; CNRS, France; ICube, France) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p141-p doi:10.1145/3571218
	Morris, J. Garrett	Proc. ACM Program. Lang., vol. 7, issue POPL: "A Type-Based Approach to Divide-and-Conquer ..." A Type-Based Approach to Divide-and-Conquer Recursion in Coq Pedro Abreu, Benjamin Delaware, Alex Hubers, Christa Jenkins, J. Garrett Morris, and Aaron Stump (Purdue University, USA; University of Iowa, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p17-p doi:10.1145/3571196
	Morrisett, Greg	Proc. ACM Program. Lang., vol. 7, issue POPL: "A Core Calculus for Equational ..." A Core Calculus for Equational Proofs of Cryptographic Protocols Joshua Gancher, Kristina Sojakova, Xiong Fan, Elaine Shi, and Greg Morrisett (Carnegie Mellon University, USA; Inria, France; Rutgers University, USA; Cornell University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p185-p doi:10.1145/3571223
	Mullanix, Reed	Proc. ACM Program. Lang., vol. 7, issue POPL: "An Order-Theoretic Analysis ..." An Order-Theoretic Analysis of Universe Polymorphism Kuen-Bang Hou (Favonia), Carlo Angiuli, and Reed Mullanix (University of Minnesota, USA; Carnegie Mellon University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p471-p doi:10.1145/3571250
	Nagasamudram, Ramana	Proc. ACM Program. Lang., vol. 7, issue POPL: "An Algebra of Alignment for ..." An Algebra of Alignment for Relational Verification Timos Antonopoulos, Eric Koskinen, Ton Chanh Le, Ramana Nagasamudram, David A. Naumann, and Minh Ngo (Yale University, USA; Stevens Institute of Technology, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p114-p doi:10.1145/3571213
	Nandi, Chandrakana	Proc. ACM Program. Lang., vol. 7, issue POPL: "babble: Learning Better Abstractions ..." babble: Learning Better Abstractions with E-Graphs and Anti-unification David Cao, Rose Kunkel, Chandrakana Nandi, Max Willsey, Zachary Tatlock, and Nadia Polikarpova (University of California at San Diego, USA; Certora, USA; University of Washington, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p94-p doi:10.1145/3571207
	Naumann, David A.	Proc. ACM Program. Lang., vol. 7, issue POPL: "An Algebra of Alignment for ..." An Algebra of Alignment for Relational Verification Timos Antonopoulos, Eric Koskinen, Ton Chanh Le, Ramana Nagasamudram, David A. Naumann, and Minh Ngo (Yale University, USA; Stevens Institute of Technology, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p114-p doi:10.1145/3571213
	Neto, David	Proc. ACM Program. Lang., vol. 7, issue POPL: "Taking Back Control in an ..." Taking Back Control in an Intermediate Representation for GPU Computing Vasileios Klimis, Jack Clark, Alan Baker, David Neto, John Wickerson, and Alastair F. Donaldson (Imperial College London, UK; Google, Canada; Google, UK) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p511-p doi:10.1145/3571253
	Ngo, Minh	Proc. ACM Program. Lang., vol. 7, issue POPL: "An Algebra of Alignment for ..." An Algebra of Alignment for Relational Verification Timos Antonopoulos, Eric Koskinen, Ton Chanh Le, Ramana Nagasamudram, David A. Naumann, and Minh Ngo (Yale University, USA; Stevens Institute of Technology, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p114-p doi:10.1145/3571213
	O'Connor, Liam	Proc. ACM Program. Lang., vol. 7, issue POPL: "Dargent: A Silver Bullet for ..." Dargent: A Silver Bullet for Verified Data Layout Refinement Zilin Chen, Ambroise Lafont, Liam O'Connor, Gabriele Keller, Craig McLaughlin, Vincent Jackson, and Christine Rizkallah (UNSW, Australia; University of Cambridge, UK; University of Edinburgh, UK; Utrecht University, Netherlands; University of Melbourne, Australia) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p325-p doi:10.1145/3571240
	Olausson, Theo X.	Proc. ACM Program. Lang., vol. 7, issue POPL: "Top-Down Synthesis for Library ..." Top-Down Synthesis for Library Learning Matthew Bowers, Theo X. Olausson, Lionel Wong, Gabriel Grand, Joshua B. Tenenbaum, Kevin Ellis, and Armando Solar-Lezama (Massachusetts Institute of Technology, USA; Cornell University, USA) Publisher's Version Published Artifact Archive submitted (1.6 MB) Artifacts Available Artifacts Reusable Article: popl23main-p278-p doi:10.1145/3571234
	Olimpieri, Federico	Proc. ACM Program. Lang., vol. 7, issue POPL: "Why Are Proofs Relevant in ..." Why Are Proofs Relevant in Proof-Relevant Models? Axel Kerinec, Giulio Manzonetto, and Federico Olimpieri (Université Sorbonne Paris Nord, France; LIPN, France; CNRS, France; University of Leeds, UK) Publisher's Version Article: popl23main-p66-p doi:10.1145/3571201
	Oliveira, Bruno C. d. S.	Proc. ACM Program. Lang., vol. 7, issue POPL: "A Bowtie for a Beast: Overloading, ..." A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F⋈ Nick Rioux, Xuejing Huang, Bruno C. d. S. Oliveira, and Steve Zdancewic (University of Pennsylvania, USA; University of Hong Kong, China) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p111-p doi:10.1145/3571211 Proc. ACM Program. Lang., vol. 7, issue POPL: "Making a Type Difference: ..." Making a Type Difference: Subtraction on Intersection Types as Generalized Record Operations Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira (Peking University, China; University of Hong Kong, China) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p191-p doi:10.1145/3571224 Proc. ACM Program. Lang., vol. 7, issue POPL: "Recursive Subtyping for All ..." Recursive Subtyping for All Litao Zhou, Yaoda Zhou, and Bruno C. d. S. Oliveira (University of Hong Kong, China) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p335-p doi:10.1145/3571241
	Oliveira Vale, Arthur	Proc. ACM Program. Lang., vol. 7, issue POPL: "A Compositional Theory of ..." A Compositional Theory of Linearizability Arthur Oliveira Vale, Zhong Shao, and Yixuan Chen (Yale University, USA) Publisher's Version Article: popl23main-p263-p doi:10.1145/3571231
	Palmkvist, Viktor	Proc. ACM Program. Lang., vol. 7, issue POPL: "Statically Resolvable Ambiguity ..." Statically Resolvable Ambiguity Viktor Palmkvist, Elias Castegren, Philipp Haller, and David Broman (KTH Royal Institute of Technology, Sweden; Uppsala University, Sweden) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p477-p doi:10.1145/3571251
	Paquet, Hugo	Proc. ACM Program. Lang., vol. 7, issue POPL: "Affine Monads and Lazy Structures ..." Affine Monads and Lazy Structures for Bayesian Programming Swaraj Dash, Younesse Kaddar, Hugo Paquet, and Sam Staton (University of Oxford, UK) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p324-p doi:10.1145/3571239
	Parno, Bryan	Proc. ACM Program. Lang., vol. 7, issue POPL: "MSWasm: Soundly Enforcing ..." MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code Alexandra E. Michael, Anitha Gollamudi, Jay Bosamiya, Evan Johnson, Aidan Denlinger, Craig Disselkoen, Conrad Watt, Bryan Parno, Marco Patrignani, Marco Vassena, and Deian Stefan (University of California at San Diego, USA; University of Washington, USA; University of Massachusetts Lowell, USA; Carnegie Mellon University, USA; Arm, USA; University of Cambridge, UK; University of Trento, Italy; Utrecht University, Netherlands) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl23main-p96-p doi:10.1145/3571208
	Paszke, Adam	Proc. ACM Program. Lang., vol. 7, issue POPL: "You Only Linearize Once: Tangents ..." You Only Linearize Once: Tangents Transpose to Gradients Alexey Radul, Adam Paszke, Roy Frostig, Matthew J. Johnson, and Dougal Maclaurin (Google Research, USA; Google Research, Poland) Publisher's Version Article: popl23main-p303-p doi:10.1145/3571236
	Patrignani, Marco	Proc. ACM Program. Lang., vol. 7, issue POPL: "MSWasm: Soundly Enforcing ..." MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code Alexandra E. Michael, Anitha Gollamudi, Jay Bosamiya, Evan Johnson, Aidan Denlinger, Craig Disselkoen, Conrad Watt, Bryan Parno, Marco Patrignani, Marco Vassena, and Deian Stefan (University of California at San Diego, USA; University of Washington, USA; University of Massachusetts Lowell, USA; Carnegie Mellon University, USA; Arm, USA; University of Cambridge, UK; University of Trento, Italy; Utrecht University, Netherlands) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl23main-p96-p doi:10.1145/3571208
	Péchoux, Romain	Proc. ACM Program. Lang., vol. 7, issue POPL: "A General Noninterference ..." A General Noninterference Policy for Polynomial Time Emmanuel Hainry and Romain Péchoux (Université de Lorraine, France; CNRS, France; Inria, France; LORIA, France) Publisher's Version Article: popl23main-p149-p doi:10.1145/3571221
	Perelman, Daniel	Proc. ACM Program. Lang., vol. 7, issue POPL: "FlashFill++: Scaling Programming ..." FlashFill++: Scaling Programming by Example by Cutting to the Chase José Cambronero, Sumit Gulwani, Vu Le, Daniel Perelman, Arjun Radhakrishna, Clint Simon, and Ashish Tiwari (Microsoft, USA) Publisher's Version Article: popl23main-p198-p doi:10.1145/3571226
	Pichardie, David	Proc. ACM Program. Lang., vol. 7, issue POPL: "Formally Verified Native Code ..." Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler Aurèle Barrière, Sandrine Blazy, and David Pichardie (University of Rennes, France; Inria, France; CNRS, France; IRISA, France; Meta, France) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p72-p doi:10.1145/3571202
	Pitts, Andrew M.	Proc. ACM Program. Lang., vol. 7, issue POPL: "Locally Nameless Sets ..." Locally Nameless Sets Andrew M. Pitts (University of Cambridge, UK) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p106-p doi:10.1145/3571210
	Podelski, Andreas	Proc. ACM Program. Lang., vol. 7, issue POPL: "Stratified Commutativity in ..." Stratified Commutativity in Verification Algorithms for Concurrent Programs Azadeh Farzan, Dominik Klumpp, and Andreas Podelski (University of Toronto, Canada; University of Freiburg, Germany) Publisher's Version Archive submitted (780 kB) Article: popl23main-p348-p doi:10.1145/3571242
	Polikarpova, Nadia	Proc. ACM Program. Lang., vol. 7, issue POPL: "babble: Learning Better Abstractions ..." babble: Learning Better Abstractions with E-Graphs and Anti-unification David Cao, Rose Kunkel, Chandrakana Nandi, Max Willsey, Zachary Tatlock, and Nadia Polikarpova (University of California at San Diego, USA; Certora, USA; University of Washington, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p94-p doi:10.1145/3571207
	Popescu, Andrei	Proc. ACM Program. Lang., vol. 7, issue POPL: "Admissible Types-to-PERs Relativization ..." Admissible Types-to-PERs Relativization in Higher-Order Logic Andrei Popescu and Dmitriy Traytel (University of Sheffield, UK; University of Copenhagen, Denmark) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p299-p doi:10.1145/3571235
	Pottier, François	Proc. ACM Program. Lang., vol. 7, issue POPL: "A High-Level Separation Logic ..." A High-Level Separation Logic for Heap Space under Garbage Collection Alexandre Moine, Arthur Charguéraud, and François Pottier (Inria, France; Université de Strasbourg, France; CNRS, France; ICube, France) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p141-p doi:10.1145/3571218
	Pujet, Loïc	Proc. ACM Program. Lang., vol. 7, issue POPL: "Impredicative Observational ..." Impredicative Observational Equality Loïc Pujet and Nicolas Tabareau (Inria, France) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p756-p doi:10.1145/3571739
	Pulte, Christopher	Proc. ACM Program. Lang., vol. 7, issue POPL: "CN: Verifying Systems C Code ..." CN: Verifying Systems C Code with Separation-Logic Refinement Types Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, and Neel Krishnaswami (University of Cambridge, UK) Publisher's Version Article: popl23main-p2-p doi:10.1145/3571194
	Qiu, Xiaokang	Proc. ACM Program. Lang., vol. 7, issue POPL: "Comparative Synthesis: Learning ..." Comparative Synthesis: Learning Near-Optimal Network Designs by Query Yanjun Wang, Zixuan Li, Chuan Jiang, Xiaokang Qiu, and Sanjay Rao (Purdue University, USA) Publisher's Version Archive submitted (1.3 MB) Artifacts Functional Article: popl23main-p33-p doi:10.1145/3571197
	Raad, Azalea	Proc. ACM Program. Lang., vol. 7, issue POPL: "The Path to Durable Linearizability ..." The Path to Durable Linearizability Emanuele D'Osualdo, Azalea Raad, and Viktor Vafeiadis (MPI-SWS, Germany; Imperial College London, UK) Publisher's Version Article: popl23main-p144-p doi:10.1145/3571219
	Radhakrishna, Arjun	Proc. ACM Program. Lang., vol. 7, issue POPL: "FlashFill++: Scaling Programming ..." FlashFill++: Scaling Programming by Example by Cutting to the Chase José Cambronero, Sumit Gulwani, Vu Le, Daniel Perelman, Arjun Radhakrishna, Clint Simon, and Ashish Tiwari (Microsoft, USA) Publisher's Version Article: popl23main-p198-p doi:10.1145/3571226
	Radul, Alexey	Proc. ACM Program. Lang., vol. 7, issue POPL: "You Only Linearize Once: Tangents ..." You Only Linearize Once: Tangents Transpose to Gradients Alexey Radul, Adam Paszke, Roy Frostig, Matthew J. Johnson, and Dougal Maclaurin (Google Research, USA; Google Research, Poland) Publisher's Version Article: popl23main-p303-p doi:10.1145/3571236
	Ramsay, Steven	Proc. ACM Program. Lang., vol. 7, issue POPL: "Higher-Order MSL Horn Constraints ..." Higher-Order MSL Horn Constraints Jerome Jochems, Eddie Jones, and Steven Ramsay (University of Bristol, UK) Publisher's Version Article: popl23main-p650-p doi:10.1145/3571262
	Rand, Robert	Proc. ACM Program. Lang., vol. 7, issue POPL: "Qunity: A Unified Language ..." Qunity: A Unified Language for Quantum and Classical Computing Finn Voichick, Liyi Li, Robert Rand, and Michael Hicks (University of Maryland, USA; University of Chicago, USA; Amazon, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p197-p doi:10.1145/3571225
	Rao, Sanjay	Proc. ACM Program. Lang., vol. 7, issue POPL: "Comparative Synthesis: Learning ..." Comparative Synthesis: Learning Near-Optimal Network Designs by Query Yanjun Wang, Zixuan Li, Chuan Jiang, Xiaokang Qiu, and Sanjay Rao (Purdue University, USA) Publisher's Version Archive submitted (1.3 MB) Artifacts Functional Article: popl23main-p33-p doi:10.1145/3571197
	Reps, Thomas	Proc. ACM Program. Lang., vol. 7, issue POPL: "Unrealizability Logic ..." Unrealizability Logic Jinwoo Kim, Loris D'Antoni, and Thomas Reps (University of Wisconsin-Madison, USA; Seoul National University, South Korea) Publisher's Version Article: popl23main-p120-p doi:10.1145/3571216 Proc. ACM Program. Lang., vol. 7, issue POPL: "Single-Source-Single-Target ..." Single-Source-Single-Target Interleaved-Dyck Reachability via Integer Linear Programming Yuanbo Li, Qirun Zhang, and Thomas Reps (Georgia Institute of Technology, USA; University of Wisconsin-Madison, USA) Publisher's Version Article: popl23main-p222-p doi:10.1145/3571228
	Rioux, Nick	Proc. ACM Program. Lang., vol. 7, issue POPL: "A Bowtie for a Beast: Overloading, ..." A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F⋈ Nick Rioux, Xuejing Huang, Bruno C. d. S. Oliveira, and Steve Zdancewic (University of Pennsylvania, USA; University of Hong Kong, China) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p111-p doi:10.1145/3571211
	Rival, Xavier	Proc. ACM Program. Lang., vol. 7, issue POPL: "Smoothness Analysis for Probabilistic ..." Smoothness Analysis for Probabilistic Programs with Application to Optimised Variational Inference Wonyeol Lee, Xavier Rival, and Hongseok Yang (Stanford University, USA; Inria, France; ENS, France; CNRS, France; PSL University, France; KAIST, South Korea; IBS, South Korea) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p85-p doi:10.1145/3571205
	Rizkallah, Christine	Proc. ACM Program. Lang., vol. 7, issue POPL: "Dargent: A Silver Bullet for ..." Dargent: A Silver Bullet for Verified Data Layout Refinement Zilin Chen, Ambroise Lafont, Liam O'Connor, Gabriele Keller, Craig McLaughlin, Vincent Jackson, and Christine Rizkallah (UNSW, Australia; University of Cambridge, UK; University of Edinburgh, UK; Utrecht University, Netherlands; University of Melbourne, Australia) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p325-p doi:10.1145/3571240
	Ross, Neil J.	Proc. ACM Program. Lang., vol. 7, issue POPL: "Proto-Quipper with Dynamic ..." Proto-Quipper with Dynamic Lifting Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger (Dalhousie University, Canada; University of Illinois at Urbana-Champaign, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p79-p doi:10.1145/3571204
	Sammler, Michael	Proc. ACM Program. Lang., vol. 7, issue POPL: "DimSum: A Decentralized Approach ..." DimSum: A Decentralized Approach to Multi-language Semantics and Verification Michael Sammler, Simon Spies, Youngju Song, Emanuele D'Osualdo, Robbert Krebbers, Deepak Garg, and Derek Dreyer (MPI-SWS, Germany; Radboud University Nijmegen, Netherlands) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p145-p doi:10.1145/3571220 Proc. ACM Program. Lang., vol. 7, issue POPL: "Conditional Contextual Refinement ..." Conditional Contextual Refinement Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Sammler, and Derek Dreyer (Seoul National University, South Korea; MPI-SWS, Germany) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p264-p doi:10.1145/3571232
	Sands, David	Proc. ACM Program. Lang., vol. 7, issue POPL: "Reconciling Shannon and Scott ..." Reconciling Shannon and Scott with a Lattice of Computable Information Sebastian Hunt, David Sands, and Sandro Stucki (City University of London, UK; Chalmers University of Technology, Sweden; Amazon Prime Video, Sweden) Publisher's Version Article: popl23main-p600-p doi:10.1145/3571740
	Santamaria, Alessio	Proc. ACM Program. Lang., vol. 7, issue POPL: "Deconstructing the Calculus ..." Deconstructing the Calculus of Relations with Tape Diagrams Filippo Bonchi, Alessandro Di Giorgio, and Alessio Santamaria (University of Pisa, Italy; University of Sussex, UK) Publisher's Version Article: popl23main-p559-p doi:10.1145/3571257
	Sato, Ryosuke	Proc. ACM Program. Lang., vol. 7, issue POPL: "HFL(Z) Validity Checking for ..." HFL(Z) Validity Checking for Automated Program Verification Naoki Kobayashi, Kento Tanahashi, Ryosuke Sato, and Takeshi Tsukada (University of Tokyo, Japan; Chiba University, Japan) Publisher's Version Article: popl23main-p55-p doi:10.1145/3571199
	Schröder, Lutz	Proc. ACM Program. Lang., vol. 7, issue POPL: "Towards a Higher-Order Mathematical ..." Towards a Higher-Order Mathematical Operational Semantics Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat (University of Erlangen-Nuremberg, Germany) Publisher's Version Article: popl23main-p119-p doi:10.1145/3571215
	Sekiyama, Taro	Proc. ACM Program. Lang., vol. 7, issue POPL: "Temporal Verification with ..." Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations Taro Sekiyama and Hiroshi Unno (National Institute of Informatics, Japan; University of Tsukuba, Japan; RIKEN AIP, Japan) Publisher's Version Archive submitted (940 kB) Article: popl23main-p688-p doi:10.1145/3571264
	Selinger, Peter	Proc. ACM Program. Lang., vol. 7, issue POPL: "Proto-Quipper with Dynamic ..." Proto-Quipper with Dynamic Lifting Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger (Dalhousie University, Canada; University of Illinois at Urbana-Champaign, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p79-p doi:10.1145/3571204
	Sewell, Peter	Proc. ACM Program. Lang., vol. 7, issue POPL: "CN: Verifying Systems C Code ..." CN: Verifying Systems C Code with Separation-Logic Refinement Types Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, and Neel Krishnaswami (University of Cambridge, UK) Publisher's Version Article: popl23main-p2-p doi:10.1145/3571194
	Sewell, Thomas	Proc. ACM Program. Lang., vol. 7, issue POPL: "CN: Verifying Systems C Code ..." CN: Verifying Systems C Code with Separation-Logic Refinement Types Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, and Neel Krishnaswami (University of Cambridge, UK) Publisher's Version Article: popl23main-p2-p doi:10.1145/3571194
	Shao, Zhong	Proc. ACM Program. Lang., vol. 7, issue POPL: "A Compositional Theory of ..." A Compositional Theory of Linearizability Arthur Oliveira Vale, Zhong Shao, and Yixuan Chen (Yale University, USA) Publisher's Version Article: popl23main-p263-p doi:10.1145/3571231
	Shi, Elaine	Proc. ACM Program. Lang., vol. 7, issue POPL: "A Core Calculus for Equational ..." A Core Calculus for Equational Proofs of Cryptographic Protocols Joshua Gancher, Kristina Sojakova, Xiong Fan, Elaine Shi, and Greg Morrisett (Carnegie Mellon University, USA; Inria, France; Rutgers University, USA; Cornell University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p185-p doi:10.1145/3571223
	Shi, Pengyuan	Proc. ACM Program. Lang., vol. 7, issue POPL: "Type-Preserving, Dependence-Aware ..." Type-Preserving, Dependence-Aware Guide Generation for Sound, Effective Amortized Probabilistic Inference Jianlin Li, Leni Ven, Pengyuan Shi, and Yizhou Zhang (University of Waterloo, Canada) Publisher's Version Article: popl23main-p354-p doi:10.1145/3571243
	Simon, Clint	Proc. ACM Program. Lang., vol. 7, issue POPL: "FlashFill++: Scaling Programming ..." FlashFill++: Scaling Programming by Example by Cutting to the Chase José Cambronero, Sumit Gulwani, Vu Le, Daniel Perelman, Arjun Radhakrishna, Clint Simon, and Ashish Tiwari (Microsoft, USA) Publisher's Version Article: popl23main-p198-p doi:10.1145/3571226
	Singh, Abhishek Kr	Proc. ACM Program. Lang., vol. 7, issue POPL: "An Operational Approach to ..." An Operational Approach to Library Abstraction under Relaxed Memory Concurrency Abhishek Kr Singh and Ori Lahav (Tel Aviv University, Israel) Publisher's Version Article: popl23main-p380-p doi:10.1145/3571246
	Smeding, Tom J.	Proc. ACM Program. Lang., vol. 7, issue POPL: "Efficient Dual-Numbers Reverse ..." Efficient Dual-Numbers Reverse AD via Well-Known Program Transformations Tom J. Smeding and Matthijs I. L. Vákár (Utrecht University, Netherlands) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p409-p doi:10.1145/3571247
	Sojakova, Kristina	Proc. ACM Program. Lang., vol. 7, issue POPL: "A Core Calculus for Equational ..." A Core Calculus for Equational Proofs of Cryptographic Protocols Joshua Gancher, Kristina Sojakova, Xiong Fan, Elaine Shi, and Greg Morrisett (Carnegie Mellon University, USA; Inria, France; Rutgers University, USA; Cornell University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p185-p doi:10.1145/3571223
	Solar-Lezama, Armando	Proc. ACM Program. Lang., vol. 7, issue POPL: "Top-Down Synthesis for Library ..." Top-Down Synthesis for Library Learning Matthew Bowers, Theo X. Olausson, Lionel Wong, Gabriel Grand, Joshua B. Tenenbaum, Kevin Ellis, and Armando Solar-Lezama (Massachusetts Institute of Technology, USA; Cornell University, USA) Publisher's Version Published Artifact Archive submitted (1.6 MB) Artifacts Available Artifacts Reusable Article: popl23main-p278-p doi:10.1145/3571234 Proc. ACM Program. Lang., vol. 7, issue POPL: "Combining Functional and Automata ..." Combining Functional and Automata Synthesis to Discover Causal Reactive Programs Ria Das, Joshua B. Tenenbaum, Armando Solar-Lezama, and Zenna Tavares (Stanford University, USA; Massachusetts Institute of Technology, USA; Basis, USA; Columbia University, USA) Publisher's Version Archive submitted (780 kB) Article: popl23main-p449-p doi:10.1145/3571249
	Song, Youngju	Proc. ACM Program. Lang., vol. 7, issue POPL: "DimSum: A Decentralized Approach ..." DimSum: A Decentralized Approach to Multi-language Semantics and Verification Michael Sammler, Simon Spies, Youngju Song, Emanuele D'Osualdo, Robbert Krebbers, Deepak Garg, and Derek Dreyer (MPI-SWS, Germany; Radboud University Nijmegen, Netherlands) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p145-p doi:10.1145/3571220 Proc. ACM Program. Lang., vol. 7, issue POPL: "Conditional Contextual Refinement ..." Conditional Contextual Refinement Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Sammler, and Derek Dreyer (Seoul National University, South Korea; MPI-SWS, Germany) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p264-p doi:10.1145/3571232
	Spies, Simon	Proc. ACM Program. Lang., vol. 7, issue POPL: "DimSum: A Decentralized Approach ..." DimSum: A Decentralized Approach to Multi-language Semantics and Verification Michael Sammler, Simon Spies, Youngju Song, Emanuele D'Osualdo, Robbert Krebbers, Deepak Garg, and Derek Dreyer (MPI-SWS, Germany; Radboud University Nijmegen, Netherlands) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p145-p doi:10.1145/3571220
	Stanford, Caleb	Proc. ACM Program. Lang., vol. 7, issue POPL: "A Robust Theory of Series ..." A Robust Theory of Series Parallel Graphs Rajeev Alur, Caleb Stanford, and Christopher Watson (University of Pennsylvania, USA; University of California at San Diego, USA; University of California at Davis, USA) Publisher's Version Article: popl23main-p256-p doi:10.1145/3571230
	Staton, Sam	Proc. ACM Program. Lang., vol. 7, issue POPL: "Affine Monads and Lazy Structures ..." Affine Monads and Lazy Structures for Bayesian Programming Swaraj Dash, Younesse Kaddar, Hugo Paquet, and Sam Staton (University of Oxford, UK) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p324-p doi:10.1145/3571239 Proc. ACM Program. Lang., vol. 7, issue POPL: "ADEV: Sound Automatic Differentiation ..." ADEV: Sound Automatic Differentiation of Expected Values of Probabilistic Programs Alexander K. Lew, Mathieu Huot, Sam Staton, and Vikash K. Mansinghka (Massachusetts Institute of Technology, USA; University of Oxford, UK) Publisher's Version Archive submitted (1 MB) Article: popl23main-p48-p doi:10.1145/3571198
	Stefan, Deian	Proc. ACM Program. Lang., vol. 7, issue POPL: "MSWasm: Soundly Enforcing ..." MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code Alexandra E. Michael, Anitha Gollamudi, Jay Bosamiya, Evan Johnson, Aidan Denlinger, Craig Disselkoen, Conrad Watt, Bryan Parno, Marco Patrignani, Marco Vassena, and Deian Stefan (University of California at San Diego, USA; University of Washington, USA; University of Massachusetts Lowell, USA; Carnegie Mellon University, USA; Arm, USA; University of Cambridge, UK; University of Trento, Italy; Utrecht University, Netherlands) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl23main-p96-p doi:10.1145/3571208
	Strub, Pierre-Yves	Proc. ACM Program. Lang., vol. 7, issue POPL: "CoqQ: Foundational Verification ..." CoqQ: Foundational Verification of Quantum Programs Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, and Mingsheng Ying (MPI-SP, Germany; Institute of Software at Chinese Academy of Sciences, China; IMDEA Software Institute, Spain; Meta, France; University of Chinese Academy of Sciences, China; Tsinghua University, China) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p163-p doi:10.1145/3571222
	Stucki, Sandro	Proc. ACM Program. Lang., vol. 7, issue POPL: "Reconciling Shannon and Scott ..." Reconciling Shannon and Scott with a Lattice of Computable Information Sebastian Hunt, David Sands, and Sandro Stucki (City University of London, UK; Chalmers University of Technology, Sweden; Amazon Prime Video, Sweden) Publisher's Version Article: popl23main-p600-p doi:10.1145/3571740
	Stump, Aaron	Proc. ACM Program. Lang., vol. 7, issue POPL: "A Type-Based Approach to Divide-and-Conquer ..." A Type-Based Approach to Divide-and-Conquer Recursion in Coq Pedro Abreu, Benjamin Delaware, Alex Hubers, Christa Jenkins, J. Garrett Morris, and Aaron Stump (Purdue University, USA; University of Iowa, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p17-p doi:10.1145/3571196
	Tabareau, Nicolas	Proc. ACM Program. Lang., vol. 7, issue POPL: "Impredicative Observational ..." Impredicative Observational Equality Loïc Pujet and Nicolas Tabareau (Inria, France) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p756-p doi:10.1145/3571739
	Tanahashi, Kento	Proc. ACM Program. Lang., vol. 7, issue POPL: "HFL(Z) Validity Checking for ..." HFL(Z) Validity Checking for Automated Program Verification Naoki Kobayashi, Kento Tanahashi, Ryosuke Sato, and Takeshi Tsukada (University of Tokyo, Japan; Chiba University, Japan) Publisher's Version Article: popl23main-p55-p doi:10.1145/3571199
	Tatlock, Zachary	Proc. ACM Program. Lang., vol. 7, issue POPL: "babble: Learning Better Abstractions ..." babble: Learning Better Abstractions with E-Graphs and Anti-unification David Cao, Rose Kunkel, Chandrakana Nandi, Max Willsey, Zachary Tatlock, and Nadia Polikarpova (University of California at San Diego, USA; Certora, USA; University of Washington, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p94-p doi:10.1145/3571207
	Tavares, Zenna	Proc. ACM Program. Lang., vol. 7, issue POPL: "Combining Functional and Automata ..." Combining Functional and Automata Synthesis to Discover Causal Reactive Programs Ria Das, Joshua B. Tenenbaum, Armando Solar-Lezama, and Zenna Tavares (Stanford University, USA; Massachusetts Institute of Technology, USA; Basis, USA; Columbia University, USA) Publisher's Version Archive submitted (780 kB) Article: popl23main-p449-p doi:10.1145/3571249
	Tenenbaum, Joshua B.	Proc. ACM Program. Lang., vol. 7, issue POPL: "Top-Down Synthesis for Library ..." Top-Down Synthesis for Library Learning Matthew Bowers, Theo X. Olausson, Lionel Wong, Gabriel Grand, Joshua B. Tenenbaum, Kevin Ellis, and Armando Solar-Lezama (Massachusetts Institute of Technology, USA; Cornell University, USA) Publisher's Version Published Artifact Archive submitted (1.6 MB) Artifacts Available Artifacts Reusable Article: popl23main-p278-p doi:10.1145/3571234 Proc. ACM Program. Lang., vol. 7, issue POPL: "Combining Functional and Automata ..." Combining Functional and Automata Synthesis to Discover Causal Reactive Programs Ria Das, Joshua B. Tenenbaum, Armando Solar-Lezama, and Zenna Tavares (Stanford University, USA; Massachusetts Institute of Technology, USA; Basis, USA; Columbia University, USA) Publisher's Version Archive submitted (780 kB) Article: popl23main-p449-p doi:10.1145/3571249
	Terauchi, Tachio	Proc. ACM Program. Lang., vol. 7, issue POPL: "Modular Primal-Dual Fixpoint ..." Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinen (University of Tsukuba, Japan; RIKEN AIP, Japan; Waseda University, Japan; Stevens Institute of Technology, USA) Publisher's Version Article: popl23main-p691-p doi:10.1145/3571265
	Thinniyam, Ramanathan S.	Proc. ACM Program. Lang., vol. 7, issue POPL: "Context-Bounded Verification ..." Context-Bounded Verification of Context-Free Specifications Pascal Baumann, Moses Ganardi, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche (MPI-SWS, Germany) Publisher's Version Article: popl23main-p699-p doi:10.1145/3571266
	Thokair, Mosaad Al	Proc. ACM Program. Lang., vol. 7, issue POPL: "Dynamic Race Detection with ..." Dynamic Race Detection with O(1) Samples Mosaad Al Thokair, Minjian Zhang, Umang Mathur, and Mahesh Viswanathan (University of Illinois at Urbana-Champaign, USA; National University of Singapore, Singapore) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p314-p doi:10.1145/3571238
	Tiwari, Ashish	Proc. ACM Program. Lang., vol. 7, issue POPL: "FlashFill++: Scaling Programming ..." FlashFill++: Scaling Programming by Example by Cutting to the Chase José Cambronero, Sumit Gulwani, Vu Le, Daniel Perelman, Arjun Radhakrishna, Clint Simon, and Ashish Tiwari (Microsoft, USA) Publisher's Version Article: popl23main-p198-p doi:10.1145/3571226
	Traytel, Dmitriy	Proc. ACM Program. Lang., vol. 7, issue POPL: "Admissible Types-to-PERs Relativization ..." Admissible Types-to-PERs Relativization in Higher-Order Logic Andrei Popescu and Dmitriy Traytel (University of Sheffield, UK; University of Copenhagen, Denmark) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p299-p doi:10.1145/3571235
	Tsampas, Stelios	Proc. ACM Program. Lang., vol. 7, issue POPL: "Towards a Higher-Order Mathematical ..." Towards a Higher-Order Mathematical Operational Semantics Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat (University of Erlangen-Nuremberg, Germany) Publisher's Version Article: popl23main-p119-p doi:10.1145/3571215
	Tsukada, Takeshi	Proc. ACM Program. Lang., vol. 7, issue POPL: "Optimal CHC Solving via Termination ..." Optimal CHC Solving via Termination Proofs Yu Gu, Takeshi Tsukada, and Hiroshi Unno (University of Tsukuba, Japan; Chiba University, Japan; RIKEN AIP, Japan) Publisher's Version Article: popl23main-p115-p doi:10.1145/3571214 Proc. ACM Program. Lang., vol. 7, issue POPL: "HFL(Z) Validity Checking for ..." HFL(Z) Validity Checking for Automated Program Verification Naoki Kobayashi, Kento Tanahashi, Ryosuke Sato, and Takeshi Tsukada (University of Tokyo, Japan; Chiba University, Japan) Publisher's Version Article: popl23main-p55-p doi:10.1145/3571199
	Unno, Hiroshi	Proc. ACM Program. Lang., vol. 7, issue POPL: "Optimal CHC Solving via Termination ..." Optimal CHC Solving via Termination Proofs Yu Gu, Takeshi Tsukada, and Hiroshi Unno (University of Tsukuba, Japan; Chiba University, Japan; RIKEN AIP, Japan) Publisher's Version Article: popl23main-p115-p doi:10.1145/3571214 Proc. ACM Program. Lang., vol. 7, issue POPL: "Temporal Verification with ..." Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations Taro Sekiyama and Hiroshi Unno (National Institute of Informatics, Japan; University of Tsukuba, Japan; RIKEN AIP, Japan) Publisher's Version Archive submitted (940 kB) Article: popl23main-p688-p doi:10.1145/3571264 Proc. ACM Program. Lang., vol. 7, issue POPL: "Modular Primal-Dual Fixpoint ..." Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinen (University of Tsukuba, Japan; RIKEN AIP, Japan; Waseda University, Japan; Stevens Institute of Technology, USA) Publisher's Version Article: popl23main-p691-p doi:10.1145/3571265
	Urbat, Henning	Proc. ACM Program. Lang., vol. 7, issue POPL: "Towards a Higher-Order Mathematical ..." Towards a Higher-Order Mathematical Operational Semantics Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat (University of Erlangen-Nuremberg, Germany) Publisher's Version Article: popl23main-p119-p doi:10.1145/3571215
	Vafeiadis, Viktor	Proc. ACM Program. Lang., vol. 7, issue POPL: "Kater: Automating Weak Memory ..." Kater: Automating Weak Memory Model Metatheory and Consistency Checking Michalis Kokologiannakis, Ori Lahav, and Viktor Vafeiadis (MPI-SWS, Germany; Tel Aviv University, Israel) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p112-p doi:10.1145/3571212 Proc. ACM Program. Lang., vol. 7, issue POPL: "The Path to Durable Linearizability ..." The Path to Durable Linearizability Emanuele D'Osualdo, Azalea Raad, and Viktor Vafeiadis (MPI-SWS, Germany; Imperial College London, UK) Publisher's Version Article: popl23main-p144-p doi:10.1145/3571219
	Vákár, Matthijs I. L.	Proc. ACM Program. Lang., vol. 7, issue POPL: "Efficient Dual-Numbers Reverse ..." Efficient Dual-Numbers Reverse AD via Well-Known Program Transformations Tom J. Smeding and Matthijs I. L. Vákár (Utrecht University, Netherlands) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p409-p doi:10.1145/3571247
	Van der Rest, Cas	Proc. ACM Program. Lang., vol. 7, issue POPL: "Hefty Algebras: Modular Elaboration ..." Hefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects Casper Bach Poulsen and Cas van der Rest (Delft University of Technology, Netherlands) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p530-p doi:10.1145/3571255
	Vassena, Marco	Proc. ACM Program. Lang., vol. 7, issue POPL: "MSWasm: Soundly Enforcing ..." MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code Alexandra E. Michael, Anitha Gollamudi, Jay Bosamiya, Evan Johnson, Aidan Denlinger, Craig Disselkoen, Conrad Watt, Bryan Parno, Marco Patrignani, Marco Vassena, and Deian Stefan (University of California at San Diego, USA; University of Washington, USA; University of Massachusetts Lowell, USA; Carnegie Mellon University, USA; Arm, USA; University of Cambridge, UK; University of Trento, Italy; Utrecht University, Netherlands) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl23main-p96-p doi:10.1145/3571208
	Ven, Leni	Proc. ACM Program. Lang., vol. 7, issue POPL: "Type-Preserving, Dependence-Aware ..." Type-Preserving, Dependence-Aware Guide Generation for Sound, Effective Amortized Probabilistic Inference Jianlin Li, Leni Ven, Pengyuan Shi, and Yizhou Zhang (University of Waterloo, Canada) Publisher's Version Article: popl23main-p354-p doi:10.1145/3571243
	Verscht, Lena	Proc. ACM Program. Lang., vol. 7, issue POPL: "A Calculus for Amortized Expected ..." A Calculus for Amortized Expected Runtimes Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Lena Verscht (RWTH Aachen University, Germany; Saarland University, Germany; University College London, UK; DTU, Denmark) Publisher's Version Article: popl23main-p592-p doi:10.1145/3571260
	Viswanathan, Mahesh	Proc. ACM Program. Lang., vol. 7, issue POPL: "Dynamic Race Detection with ..." Dynamic Race Detection with O(1) Samples Mosaad Al Thokair, Minjian Zhang, Umang Mathur, and Mahesh Viswanathan (University of Illinois at Urbana-Champaign, USA; National University of Singapore, Singapore) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p314-p doi:10.1145/3571238
	Voichick, Finn	Proc. ACM Program. Lang., vol. 7, issue POPL: "Qunity: A Unified Language ..." Qunity: A Unified Language for Quantum and Classical Computing Finn Voichick, Liyi Li, Robert Rand, and Michael Hicks (University of Maryland, USA; University of Chicago, USA; Amazon, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p197-p doi:10.1145/3571225
	Wang, Di	Proc. ACM Program. Lang., vol. 7, issue POPL: "Probabilistic Resource-Aware ..." Probabilistic Resource-Aware Session Types Ankush Das, Di Wang, and Jan Hoffmann (Amazon, USA; Carnegie Mellon University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p590-p doi:10.1145/3571259
	Wang, Yanjun	Proc. ACM Program. Lang., vol. 7, issue POPL: "Comparative Synthesis: Learning ..." Comparative Synthesis: Learning Near-Optimal Network Designs by Query Yanjun Wang, Zixuan Li, Chuan Jiang, Xiaokang Qiu, and Sanjay Rao (Purdue University, USA) Publisher's Version Archive submitted (1.3 MB) Artifacts Functional Article: popl23main-p33-p doi:10.1145/3571197
	Watson, Christopher	Proc. ACM Program. Lang., vol. 7, issue POPL: "A Robust Theory of Series ..." A Robust Theory of Series Parallel Graphs Rajeev Alur, Caleb Stanford, and Christopher Watson (University of Pennsylvania, USA; University of California at San Diego, USA; University of California at Davis, USA) Publisher's Version Article: popl23main-p256-p doi:10.1145/3571230
	Watt, Conrad	Proc. ACM Program. Lang., vol. 7, issue POPL: "MSWasm: Soundly Enforcing ..." MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code Alexandra E. Michael, Anitha Gollamudi, Jay Bosamiya, Evan Johnson, Aidan Denlinger, Craig Disselkoen, Conrad Watt, Bryan Parno, Marco Patrignani, Marco Vassena, and Deian Stefan (University of California at San Diego, USA; University of Washington, USA; University of Massachusetts Lowell, USA; Carnegie Mellon University, USA; Arm, USA; University of Cambridge, UK; University of Trento, Italy; Utrecht University, Netherlands) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl23main-p96-p doi:10.1145/3571208
	Wickerson, John	Proc. ACM Program. Lang., vol. 7, issue POPL: "Taking Back Control in an ..." Taking Back Control in an Intermediate Representation for GPU Computing Vasileios Klimis, Jack Clark, Alan Baker, David Neto, John Wickerson, and Alastair F. Donaldson (Imperial College London, UK; Google, Canada; Google, UK) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p511-p doi:10.1145/3571253
	Willsey, Max	Proc. ACM Program. Lang., vol. 7, issue POPL: "babble: Learning Better Abstractions ..." babble: Learning Better Abstractions with E-Graphs and Anti-unification David Cao, Rose Kunkel, Chandrakana Nandi, Max Willsey, Zachary Tatlock, and Nadia Polikarpova (University of California at San Diego, USA; Certora, USA; University of Washington, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p94-p doi:10.1145/3571207
	Wißmann, Thorsten	Proc. ACM Program. Lang., vol. 7, issue POPL: "Fast Coalgebraic Bisimilarity ..." Fast Coalgebraic Bisimilarity Minimization Jules Jacobs and Thorsten Wißmann (Radboud University Nijmegen, Netherlands) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl23main-p373-p doi:10.1145/3571245
	Wong, Lionel	Proc. ACM Program. Lang., vol. 7, issue POPL: "Top-Down Synthesis for Library ..." Top-Down Synthesis for Library Learning Matthew Bowers, Theo X. Olausson, Lionel Wong, Gabriel Grand, Joshua B. Tenenbaum, Kevin Ellis, and Armando Solar-Lezama (Massachusetts Institute of Technology, USA; Cornell University, USA) Publisher's Version Published Artifact Archive submitted (1.6 MB) Artifacts Available Artifacts Reusable Article: popl23main-p278-p doi:10.1145/3571234
	Xu, Han	Proc. ACM Program. Lang., vol. 7, issue POPL: "Making a Type Difference: ..." Making a Type Difference: Subtraction on Intersection Types as Generalized Record Operations Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira (Peking University, China; University of Hong Kong, China) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p191-p doi:10.1145/3571224
	Yang, Hongseok	Proc. ACM Program. Lang., vol. 7, issue POPL: "Smoothness Analysis for Probabilistic ..." Smoothness Analysis for Probabilistic Programs with Application to Optimised Variational Inference Wonyeol Lee, Xavier Rival, and Hongseok Yang (Stanford University, USA; Inria, France; ENS, France; CNRS, France; PSL University, France; KAIST, South Korea; IBS, South Korea) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p85-p doi:10.1145/3571205
	Ying, Mingsheng	Proc. ACM Program. Lang., vol. 7, issue POPL: "CoqQ: Foundational Verification ..." CoqQ: Foundational Verification of Quantum Programs Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, and Mingsheng Ying (MPI-SP, Germany; Institute of Software at Chinese Academy of Sciences, China; IMDEA Software Institute, Spain; Meta, France; University of Chinese Academy of Sciences, China; Tsinghua University, China) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p163-p doi:10.1145/3571222
	Zakowski, Yannick	Proc. ACM Program. Lang., vol. 7, issue POPL: "Choice Trees: Representing ..." Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, and Steve Zdancewic (University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, France; University of Pennsylvania, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p528-p doi:10.1145/3571254
	Zdancewic, Steve	Proc. ACM Program. Lang., vol. 7, issue POPL: "A Bowtie for a Beast: Overloading, ..." A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F⋈ Nick Rioux, Xuejing Huang, Bruno C. d. S. Oliveira, and Steve Zdancewic (University of Pennsylvania, USA; University of Hong Kong, China) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p111-p doi:10.1145/3571211 Proc. ACM Program. Lang., vol. 7, issue POPL: "Choice Trees: Representing ..." Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, and Steve Zdancewic (University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, France; University of Pennsylvania, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p528-p doi:10.1145/3571254
	Zetzsche, Georg	Proc. ACM Program. Lang., vol. 7, issue POPL: "Context-Bounded Verification ..." Context-Bounded Verification of Context-Free Specifications Pascal Baumann, Moses Ganardi, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche (MPI-SWS, Germany) Publisher's Version Article: popl23main-p699-p doi:10.1145/3571266
	Zhang, Haoran	Proc. ACM Program. Lang., vol. 7, issue POPL: "Executing Microservice Applications ..." Executing Microservice Applications on Serverless, Correctly Konstantinos Kallas, Haoran Zhang, Rajeev Alur, Sebastian Angel, and Vincent Liu (University of Pennsylvania, USA; Microsoft Research, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl23main-p93-p doi:10.1145/3571206
	Zhang, Minjian	Proc. ACM Program. Lang., vol. 7, issue POPL: "Dynamic Race Detection with ..." Dynamic Race Detection with O(1) Samples Mosaad Al Thokair, Minjian Zhang, Umang Mathur, and Mahesh Viswanathan (University of Illinois at Urbana-Champaign, USA; National University of Singapore, Singapore) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p314-p doi:10.1145/3571238
	Zhang, Qirun	Proc. ACM Program. Lang., vol. 7, issue POPL: "Witnessability of Undecidable ..." Witnessability of Undecidable Problems Shuo Ding and Qirun Zhang (Georgia Institute of Technology, USA) Publisher's Version Article: popl23main-p218-p doi:10.1145/3571227 Proc. ACM Program. Lang., vol. 7, issue POPL: "Single-Source-Single-Target ..." Single-Source-Single-Target Interleaved-Dyck Reachability via Integer Linear Programming Yuanbo Li, Qirun Zhang, and Thomas Reps (Georgia Institute of Technology, USA; University of Wisconsin-Madison, USA) Publisher's Version Article: popl23main-p222-p doi:10.1145/3571228
	Zhang, Yizhou	Proc. ACM Program. Lang., vol. 7, issue POPL: "Type-Preserving, Dependence-Aware ..." Type-Preserving, Dependence-Aware Guide Generation for Sound, Effective Amortized Probabilistic Inference Jianlin Li, Leni Ven, Pengyuan Shi, and Yizhou Zhang (University of Waterloo, Canada) Publisher's Version Article: popl23main-p354-p doi:10.1145/3571243
	Zhou, Li	Proc. ACM Program. Lang., vol. 7, issue POPL: "CoqQ: Foundational Verification ..." CoqQ: Foundational Verification of Quantum Programs Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, and Mingsheng Ying (MPI-SP, Germany; Institute of Software at Chinese Academy of Sciences, China; IMDEA Software Institute, Spain; Meta, France; University of Chinese Academy of Sciences, China; Tsinghua University, China) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p163-p doi:10.1145/3571222
	Zhou, Litao	Proc. ACM Program. Lang., vol. 7, issue POPL: "Recursive Subtyping for All ..." Recursive Subtyping for All Litao Zhou, Yaoda Zhou, and Bruno C. d. S. Oliveira (University of Hong Kong, China) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p335-p doi:10.1145/3571241
	Zhou, Yaoda	Proc. ACM Program. Lang., vol. 7, issue POPL: "Recursive Subtyping for All ..." Recursive Subtyping for All Litao Zhou, Yaoda Zhou, and Bruno C. d. S. Oliveira (University of Hong Kong, China) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p335-p doi:10.1145/3571241
	Zhu, Shaowei	Proc. ACM Program. Lang., vol. 7, issue POPL: "When Less Is More: Consequence-Finding ..." When Less Is More: Consequence-Finding in a Weak Theory of Arithmetic Zachary Kincaid, Nicolas Koh, and Shaowei Zhu (Princeton University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl23main-p305-p doi:10.1145/3571237