POPL 2020 – Author Index

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

	Abadi, Martín	Proc. ACM Program. Lang., vol. 4, issue POPL: "A Simple Differentiable Programming ..." A Simple Differentiable Programming Language Martín Abadi and Gordon D. Plotkin (Google Research, USA) Publisher's Version Article: popl20main-p129-p doi:10.1145/3371106
	Abdulla, Parosh Aziz	Proc. ACM Program. Lang., vol. 4, issue POPL: "Parameterized Verification ..." Parameterized Verification under TSO is PSPACE-Complete Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Rojin Rezvan (Uppsala University, Sweden; Sharif University of Technology, Iran) Publisher's Version Article: popl20main-p97-p doi:10.1145/3371094
	Acar, Umut A.	Proc. ACM Program. Lang., vol. 4, issue POPL: "Disentanglement in Nested-Parallel ..." Disentanglement in Nested-Parallel Programs Sam Westrick, Rohan Yadav, Matthew Fluet, and Umut A. Acar (Carnegie Mellon University, USA; Rochester Institute of Technology, USA) Publisher's Version Article: popl20main-p169-p doi:10.1145/3371115
	Ahmed, Amal	Proc. ACM Program. Lang., vol. 4, issue POPL: "Graduality and Parametricity: ..." Graduality and Parametricity: Together Again for the First Time Max S. New, Dustin Jamner, and Amal Ahmed (Northeastern University, USA) Publisher's Version Article: popl20main-p167-p doi:10.1145/3371114
	Ahrens, Benedikt	Proc. ACM Program. Lang., vol. 4, issue POPL: "Reduction Monads and Their ..." Reduction Monads and Their Signatures Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, and Marco Maggesi (University of Birmingham, UK; University of Côte d'Azur, France; IMT Atlantique, France; University of Florence, Italy) Publisher's Version Article: popl20main-p112-p doi:10.1145/3371099
	Aldrich, Jonathan	Proc. ACM Program. Lang., vol. 4, issue POPL: "Decidable Subtyping for Path ..." Decidable Subtyping for Path Dependent Types Julian Mackay, Alex Potanin, Jonathan Aldrich, and Lindsay Groves (Victoria University of Wellington, New Zealand; Carnegie Mellon University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p248-p doi:10.1145/3371134
	An, Shengwei	Proc. ACM Program. Lang., vol. 4, issue POPL: "Augmented Example-Based Synthesis ..." Augmented Example-Based Synthesis using Relational Perturbation Properties Shengwei An, Rishabh Singh, Sasa Misailovic, and Roopsha Samanta (Purdue University, USA; Google, USA; University of Illinois at Urbana-Champaign, USA) Publisher's Version Article: popl20main-p204-p doi:10.1145/3371124
	Arntzenius, Michael	Proc. ACM Program. Lang., vol. 4, issue POPL: "Seminaïve Evaluation for ..." Seminaïve Evaluation for a Higher-Order Functional Language Michael Arntzenius and Neel Krishnaswami (University of Birmingham, UK; University of Cambridge, UK) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl20main-p91-p doi:10.1145/3371090
	Aschieri, Federico	Proc. ACM Program. Lang., vol. 4, issue POPL: "Par Means Parallel: Multiplicative ..." Par Means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs Federico Aschieri and Francesco A. Genco (TU Vienna, Austria; University of Paris 1, France) Publisher's Version Article: popl20main-p62-p doi:10.1145/3371086
	Atig, Mohamed Faouzi	Proc. ACM Program. Lang., vol. 4, issue POPL: "Parameterized Verification ..." Parameterized Verification under TSO is PSPACE-Complete Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Rojin Rezvan (Uppsala University, Sweden; Sharif University of Technology, Iran) Publisher's Version Article: popl20main-p97-p doi:10.1145/3371094
	Ballantyne, Michael	Proc. ACM Program. Lang., vol. 4, issue POPL: "Dependent Type Systems as ..." Dependent Type Systems as Macros Stephen Chang, Michael Ballantyne, Milo Turner, and William J. Bowman (Northeastern University, USA; PLT Group, USA; University of British Columbia, Canada) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p18-p doi:10.1145/3371071
	Bansal, Suguman	Proc. ACM Program. Lang., vol. 4, issue POPL: "Synthesis of Coordination ..." Synthesis of Coordination Programs from Linear Temporal Specifications Suguman Bansal, Kedar S. Namjoshi, and Yaniv Sa'ar (Rice University, USA; Nokia Bell Labs, USA; Nokia Bell Labs, Israel) Publisher's Version Artifacts Functional Article: popl20main-p194-p doi:10.1145/3371122
	Barbarossa, Davide	Proc. ACM Program. Lang., vol. 4, issue POPL: "Taylor Subsumes Scott, Berry, ..." Taylor Subsumes Scott, Berry, Kahn and Plotkin Davide Barbarossa and Giulio Manzonetto (University of Paris 13, France) Publisher's Version Article: popl20main-p6-p doi:10.1145/3371069
	Barthe, Gilles	Proc. ACM Program. Lang., vol. 4, issue POPL: "Relational Proofs for Quantum ..." Relational Proofs for Quantum Programs Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, and Li Zhou (MPI for Security and Privacy, Germany; IMDEA Software Institute, Spain; University of Wisconsin-Madison, USA; University of Technology Sydney, Australia; Institute of Software at Chinese Academy of Sciences, China; Tsinghua University, China) Publisher's Version Article: popl20main-p78-p doi:10.1145/3371089 Proc. ACM Program. Lang., vol. 4, issue POPL: "A Probabilistic Separation ..." A Probabilistic Separation Logic Gilles Barthe, Justin Hsu, and Kevin Liao (MPI for Security and Privacy, Germany; IMDEA Software Institute, Spain; University of Wisconsin-Madison, USA; University of Illinois at Urbana-Champaign, USA) Publisher's Version Article: popl20main-p202-p doi:10.1145/3371123 Proc. ACM Program. Lang., vol. 4, issue POPL: "Formal Verification of a Constant-Time ..." Formal Verification of a Constant-Time Preserving C Compiler Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, and Alix Trieu (MPI for Security and Privacy, Germany; IMDEA Software Institute, Spain; University of Rennes, France; Inria, France; CNRS, France; IRISA, France; Aarhus University, Denmark) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p31-p doi:10.1145/3371075
	Beckett, Ryan	Proc. ACM Program. Lang., vol. 4, issue POPL: "Abstract Interpretation of ..." Abstract Interpretation of Distributed Network Control Planes Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker (Microsoft Research, USA; Princeton University, USA; University of Washington, USA; Intentionet, USA) Publisher's Version Article: popl20main-p150-p doi:10.1145/3371110
	Bengtson, Jesper	Proc. ACM Program. Lang., vol. 4, issue POPL: "Actris: Session-Type Based ..." Actris: Session-Type Based Reasoning in Separation Logic Jonas Kastberg Hinrichsen, Jesper Bengtson, and Robbert Krebbers (IT University of Copenhagen, Denmark; Delft University of Technology, Netherlands) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p29-p doi:10.1145/3371074
	Biernacki, Dariusz	Proc. ACM Program. Lang., vol. 4, issue POPL: "Binders by Day, Labels by ..." Binders by Day, Labels by Night: Effect Instances via Lexically Scoped Handlers Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski (University of Wrocław, Poland) Publisher's Version Artifacts Functional Article: popl20main-p171-p doi:10.1145/3371116
	Binder, David	Proc. ACM Program. Lang., vol. 4, issue POPL: "Decomposition Diversity with ..." Decomposition Diversity with Symmetric Data and Codata David Binder, Julian Jabs, Ingo Skupin, and Klaus Ostermann (University of Tübingen, Germany) Publisher's Version Artifacts Functional Article: popl20main-p105-p doi:10.1145/3371098
	Blatt, Austin J.	Proc. ACM Program. Lang., vol. 4, issue POPL: "Executable Formal Semantics ..." Executable Formal Semantics for the POSIX Shell Michael Greenberg and Austin J. Blatt (Pomona College, USA; Puppet Labs, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p153-p doi:10.1145/3371111
	Blazy, Sandrine	Proc. ACM Program. Lang., vol. 4, issue POPL: "Formal Verification of a Constant-Time ..." Formal Verification of a Constant-Time Preserving C Compiler Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, and Alix Trieu (MPI for Security and Privacy, Germany; IMDEA Software Institute, Spain; University of Rennes, France; Inria, France; CNRS, France; IRISA, France; Aarhus University, Denmark) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p31-p doi:10.1145/3371075
	Bodik, Rastislav	Proc. ACM Program. Lang., vol. 4, issue POPL: "Visualization by Example ..." Visualization by Example Chenglong Wang, Yu Feng, Rastislav Bodik, Alvin Cheung, and Isil Dillig (University of Washington, USA; University of California at Santa Barbara, USA; University of California at Berkeley, USA; University of Texas at Austin, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl20main-p174-p doi:10.1145/3371117
	Boulier, Simon	Proc. ACM Program. Lang., vol. 4, issue POPL: "Coq Coq Correct! Verification ..." Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, and Théo Winterhalter (Inria, France; IRIF, France; CNRS, France; University of Paris Diderot, France; Saarland University, Germany) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p34-p doi:10.1145/3371076
	Bourke, Timothy	Proc. ACM Program. Lang., vol. 4, issue POPL: "Mechanized Semantics and Verified ..." Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset Timothy Bourke, Lélio Brun, and Marc Pouzet (Inria, France; ENS, France; PSL University, France; Sorbonne University, France) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p155-p doi:10.1145/3371112
	Bowman, William J.	Proc. ACM Program. Lang., vol. 4, issue POPL: "Dependent Type Systems as ..." Dependent Type Systems as Macros Stephen Chang, Michael Ballantyne, Milo Turner, and William J. Bowman (Northeastern University, USA; PLT Group, USA; University of British Columbia, Canada) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p18-p doi:10.1145/3371071
	Brun, Lélio	Proc. ACM Program. Lang., vol. 4, issue POPL: "Mechanized Semantics and Verified ..." Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset Timothy Bourke, Lélio Brun, and Marc Pouzet (Inria, France; ENS, France; PSL University, France; Sorbonne University, France) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p155-p doi:10.1145/3371112
	Brunel, Aloïs	Proc. ACM Program. Lang., vol. 4, issue POPL: "Backpropagation in the Simply ..." Backpropagation in the Simply Typed Lambda-Calculus with Linear Negation Aloïs Brunel, Damiano Mazza, and Michele Pagani (Deepomatic, France; CNRS, France; IRIF, France; University of Paris Diderot, France) Publisher's Version Article: popl20main-p243-p doi:10.1145/3371132
	Bruni, Roberto	Proc. ACM Program. Lang., vol. 4, issue POPL: "Abstract Extensionality: On ..." Abstract Extensionality: On the Properties of Incomplete Abstract Interpretations Roberto Bruni, Roberto Giacobazzi, Roberta Gori, Isabel Garcia-Contreras, and Dusko Pavlovic (University of Pisa, Italy; University of Verona, Italy; IMDEA Software Institute, Spain; Universidad Politécnica de Madrid, Spain; University of Hawaii, USA) Publisher's Version Article: popl20main-p99-p doi:10.1145/3371096
	Carbin, Michael	Proc. ACM Program. Lang., vol. 4, issue POPL: "Trace Types and Denotational ..." Trace Types and Denotational Semantics for Sound Programmable Inference in Probabilistic Languages Alexander K. Lew, Marco F. Cusumano-Towner, Benjamin Sherman, Michael Carbin, and Vikash K. Mansinghka (Massachusetts Institute of Technology, USA) Publisher's Version Article: popl20main-p69-p doi:10.1145/3371087
	Chang, Stephen	Proc. ACM Program. Lang., vol. 4, issue POPL: "Dependent Type Systems as ..." Dependent Type Systems as Macros Stephen Chang, Michael Ballantyne, Milo Turner, and William J. Bowman (Northeastern University, USA; PLT Group, USA; University of British Columbia, Canada) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p18-p doi:10.1145/3371071
	Chatterjee, Krishnendu	Proc. ACM Program. Lang., vol. 4, issue POPL: "Proving Expected Sensitivity ..." Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time Peixin Wang, Hongfei Fu, Krishnendu Chatterjee, Yuxin Deng, and Ming Xu (Shanghai Jiao Tong University, China; IST Austria, Austria; East China Normal University, China; Pengcheng Laboratory, China) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl20main-p96-p doi:10.1145/3371093
	Cheung, Alvin	Proc. ACM Program. Lang., vol. 4, issue POPL: "Visualization by Example ..." Visualization by Example Chenglong Wang, Yu Feng, Rastislav Bodik, Alvin Cheung, and Isil Dillig (University of Washington, USA; University of California at Santa Barbara, USA; University of California at Berkeley, USA; University of Texas at Austin, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl20main-p174-p doi:10.1145/3371117
	Cho, Minki	Proc. ACM Program. Lang., vol. 4, issue POPL: "CompCertM: CompCert with C-Assembly ..." CompCertM: CompCert with C-Assembly Linking and Lightweight Modular Verification Youngju Song, Minki Cho, Dongjoo Kim, Yonghyun Kim, Jeehoon Kang, and Chung-Kil Hur (Seoul National University, South Korea; KAIST, South Korea) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p93-p doi:10.1145/3371091
	Clairambault, Pierre	Proc. ACM Program. Lang., vol. 4, issue POPL: "Full Abstraction for the Quantum ..." Full Abstraction for the Quantum Lambda-Calculus Pierre Clairambault and Marc de Visme (University of Lyon, France; ENS Lyon, France; CNRS, France; LIP, France) Publisher's Version Article: popl20main-p242-p doi:10.1145/3371131
	Clochard, Martin	Proc. ACM Program. Lang., vol. 4, issue POPL: "Deductive Verification with ..." Deductive Verification with Ghost Monitors Martin Clochard, Claude Marché, and Andrei Paskevich (ETH Zurich, Switzerland; Inria, France; University of Paris-Saclay, France; LRI, France; University of Paris-Sud, France; CNRS, France) Publisher's Version Article: popl20main-p7-p doi:10.1145/3371070
	Costanzo, David	Proc. ACM Program. Lang., vol. 4, issue POPL: "Virtual Timeline: A Formal ..." Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation Mengqi Liu, Lionel Rieg, Zhong Shao, Ronghui Gu, David Costanzo, Jung-Eun Kim, and Man-Ki Yoon (Yale University, USA; Grenoble Alps University, France; CNRS, France; Grenoble INP, France; VERIMAG, France; Columbia University, USA) Publisher's Version Artifacts Functional Article: popl20main-p73-p doi:10.1145/3371088
	Cusumano-Towner, Marco F.	Proc. ACM Program. Lang., vol. 4, issue POPL: "Trace Types and Denotational ..." Trace Types and Denotational Semantics for Sound Programmable Inference in Probabilistic Languages Alexander K. Lew, Marco F. Cusumano-Towner, Benjamin Sherman, Michael Carbin, and Vikash K. Mansinghka (Massachusetts Institute of Technology, USA) Publisher's Version Article: popl20main-p69-p doi:10.1145/3371087
	Dahlqvist, Fredrik	Proc. ACM Program. Lang., vol. 4, issue POPL: "Semantics of Higher-Order ..." Semantics of Higher-Order Probabilistic Programs with Conditioning Fredrik Dahlqvist and Dexter Kozen (University College London, UK; Imperial College London, UK; Cornell University, USA) Publisher's Version Article: popl20main-p213-p doi:10.1145/3371125
	Dang, Hoang-Hai	Proc. ACM Program. Lang., vol. 4, issue POPL: "RustBelt Meets Relaxed Memory ..." RustBelt Meets Relaxed Memory Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser, and Derek Dreyer (MPI-SWS, Germany; LRI, France; CNRS, France; University of Paris-Saclay, France) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p124-p doi:10.1145/3371102 Proc. ACM Program. Lang., vol. 4, issue POPL: "Stacked Borrows: An Aliasing ..." Stacked Borrows: An Aliasing Model for Rust Ralf Jung, Hoang-Hai Dang, Jeehoon Kang, and Derek Dreyer (MPI-SWS, Germany; Mozilla, USA; KAIST, South Korea) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p147-p doi:10.1145/3371109
	Danner, Norman	Proc. ACM Program. Lang., vol. 4, issue POPL: "Recurrence Extraction for ..." Recurrence Extraction for Functional Programs through Call-by-Push-Value G. A. Kavvos, Edward Morehouse, Daniel R. Licata, and Norman Danner (Wesleyan University, USA) Publisher's Version Article: popl20main-p46-p doi:10.1145/3371083
	Darais, David	Proc. ACM Program. Lang., vol. 4, issue POPL: "A Language for Probabilistically ..." A Language for Probabilistically Oblivious Computation David Darais, Ian Sweet, Chang Liu, and Michael Hicks (University of Vermont, USA; University of Maryland, USA; Citadel Securities, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl20main-p175-p doi:10.1145/3371118
	Deng, Yuxin	Proc. ACM Program. Lang., vol. 4, issue POPL: "Proving Expected Sensitivity ..." Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time Peixin Wang, Hongfei Fu, Krishnendu Chatterjee, Yuxin Deng, and Ming Xu (Shanghai Jiao Tong University, China; IST Austria, Austria; East China Normal University, China; Pengcheng Laboratory, China) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl20main-p96-p doi:10.1145/3371093
	De Vilhena, Paulo Emílio	Proc. ACM Program. Lang., vol. 4, issue POPL: "Spy Game: Verifying a Local ..." Spy Game: Verifying a Local Generic Solver in Iris Paulo Emílio de Vilhena, François Pottier, and Jacques-Henri Jourdan (Inria, France; CNRS, France; LRI, France; University of Paris-Saclay, France) Publisher's Version Article: popl20main-p117-p doi:10.1145/3371101
	De Visme, Marc	Proc. ACM Program. Lang., vol. 4, issue POPL: "Full Abstraction for the Quantum ..." Full Abstraction for the Quantum Lambda-Calculus Pierre Clairambault and Marc de Visme (University of Lyon, France; ENS Lyon, France; CNRS, France; LIP, France) Publisher's Version Article: popl20main-p242-p doi:10.1145/3371131
	Dillig, Isil	Proc. ACM Program. Lang., vol. 4, issue POPL: "Visualization by Example ..." Visualization by Example Chenglong Wang, Yu Feng, Rastislav Bodik, Alvin Cheung, and Isil Dillig (University of Washington, USA; University of California at Santa Barbara, USA; University of California at Berkeley, USA; University of Texas at Austin, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl20main-p174-p doi:10.1145/3371117
	Dimoulas, Christos	Proc. ACM Program. Lang., vol. 4, issue POPL: "Does Blame Shifting Work? ..." Does Blame Shifting Work? Lukas Lazarek, Alexis King, Samanvitha Sundar, Robert Bruce Findler, and Christos Dimoulas (Northwestern University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl20main-p246-p doi:10.1145/3371133
	Dreyer, Derek	Proc. ACM Program. Lang., vol. 4, issue POPL: "The High-Level Benefits of ..." The High-Level Benefits of Low-Level Sandboxing Michael Sammler, Deepak Garg, Derek Dreyer, and Tadeusz Litak (MPI-SWS, Germany; Friedrich-Alexander University Erlangen-Nürnberg, Germany) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p114-p doi:10.1145/3371100 Proc. ACM Program. Lang., vol. 4, issue POPL: "RustBelt Meets Relaxed Memory ..." RustBelt Meets Relaxed Memory Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser, and Derek Dreyer (MPI-SWS, Germany; LRI, France; CNRS, France; University of Paris-Saclay, France) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p124-p doi:10.1145/3371102 Proc. ACM Program. Lang., vol. 4, issue POPL: "Stacked Borrows: An Aliasing ..." Stacked Borrows: An Aliasing Model for Rust Ralf Jung, Hoang-Hai Dang, Jeehoon Kang, and Derek Dreyer (MPI-SWS, Germany; Mozilla, USA; KAIST, South Korea) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p147-p doi:10.1145/3371109 Proc. ACM Program. Lang., vol. 4, issue POPL: "The Future is Ours: Prophecy ..." The Future is Ours: Prophecy Variables in Separation Logic Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, and Bart Jacobs (MPI-SWS, Germany; ETH Zurich, Switzerland; University of Waterloo, Canada; KU Leuven, Belgium) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p157-p doi:10.1145/3371113
	Eisenberg, Richard A.	Proc. ACM Program. Lang., vol. 4, issue POPL: "Partial Type Constructors: ..." Partial Type Constructors: Or, Making Ad Hoc Datatypes Less Ad Hoc Mark P. Jones, J. Garrett Morris, and Richard A. Eisenberg (Portland State University, USA; University of Kansas, USA; Bryn Mawr College, USA; Tweag I/O, UK) Publisher's Version Article: popl20main-p136-p doi:10.1145/3371108 Proc. ACM Program. Lang., vol. 4, issue POPL: "Kind Inference for Datatypes ..." Kind Inference for Datatypes Ningning Xie, Richard A. Eisenberg, and Bruno C. d. S. Oliveira (University of Hong Kong, China; Bryn Mawr College, USA; Tweag I/O, UK) Publisher's Version Article: popl20main-p189-p doi:10.1145/3371121
	Farzan, Azadeh	Proc. ACM Program. Lang., vol. 4, issue POPL: "Reductions for Safety Proofs ..." Reductions for Safety Proofs Azadeh Farzan and Anthony Vandikas (University of Toronto, Canada) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p42-p doi:10.1145/3371081
	Feldman, Yotam M. Y.	Proc. ACM Program. Lang., vol. 4, issue POPL: "Complexity and Information ..." Complexity and Information in Invariant Inference Yotam M. Y. Feldman, Neil Immerman, Mooly Sagiv, and Sharon Shoham (Tel Aviv University, Israel; University of Massachusetts, USA) Publisher's Version Article: popl20main-p25-p doi:10.1145/3371073
	Feng, Yu	Proc. ACM Program. Lang., vol. 4, issue POPL: "Visualization by Example ..." Visualization by Example Chenglong Wang, Yu Feng, Rastislav Bodik, Alvin Cheung, and Isil Dillig (University of Washington, USA; University of California at Santa Barbara, USA; University of California at Berkeley, USA; University of Texas at Austin, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl20main-p174-p doi:10.1145/3371117
	Findler, Robert Bruce	Proc. ACM Program. Lang., vol. 4, issue POPL: "Does Blame Shifting Work? ..." Does Blame Shifting Work? Lukas Lazarek, Alexis King, Samanvitha Sundar, Robert Bruce Findler, and Christos Dimoulas (Northwestern University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl20main-p246-p doi:10.1145/3371133
	Fluet, Matthew	Proc. ACM Program. Lang., vol. 4, issue POPL: "Disentanglement in Nested-Parallel ..." Disentanglement in Nested-Parallel Programs Sam Westrick, Rohan Yadav, Matthew Fluet, and Umut A. Acar (Carnegie Mellon University, USA; Rochester Institute of Technology, USA) Publisher's Version Article: popl20main-p169-p doi:10.1145/3371115
	Forster, Yannick	Proc. ACM Program. Lang., vol. 4, issue POPL: "The Weak Call-by-Value λ-Calculus ..." The Weak Call-by-Value λ-Calculus Is Reasonable for Both Time and Space Yannick Forster, Fabian Kunze, and Marc Roth (Saarland University, Germany; M2CI, Germany; University of Oxford, UK) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p98-p doi:10.1145/3371095 Proc. ACM Program. Lang., vol. 4, issue POPL: "Coq Coq Correct! Verification ..." Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, and Théo Winterhalter (Inria, France; IRIF, France; CNRS, France; University of Paris Diderot, France; Saarland University, Germany) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p34-p doi:10.1145/3371076
	Foster, Nate	Proc. ACM Program. Lang., vol. 4, issue POPL: "Guarded Kleene Algebra with ..." Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time Steffen Smolka, Nate Foster, Justin Hsu, Tobias Kappé, Dexter Kozen, and Alexandra Silva (Cornell University, USA; University of Wisconsin-Madison, USA; University College London, UK) Publisher's Version Article: popl20main-p229-p doi:10.1145/3371129
	Freer, Cameron E.	Proc. ACM Program. Lang., vol. 4, issue POPL: "Optimal Approximate Sampling ..." Optimal Approximate Sampling from Discrete Probability Distributions Feras A. Saad, Cameron E. Freer, Martin C. Rinard, and Vikash K. Mansinghka (Massachusetts Institute of Technology, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl20main-p126-p doi:10.1145/3371104
	Fu, Hongfei	Proc. ACM Program. Lang., vol. 4, issue POPL: "Proving Expected Sensitivity ..." Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time Peixin Wang, Hongfei Fu, Krishnendu Chatterjee, Yuxin Deng, and Ming Xu (Shanghai Jiao Tong University, China; IST Austria, Austria; East China Normal University, China; Pengcheng Laboratory, China) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl20main-p96-p doi:10.1145/3371093
	Fu, Zhoulai	Proc. ACM Program. Lang., vol. 4, issue POPL: "Detecting Floating-Point Errors ..." Detecting Floating-Point Errors via Atomic Conditions Daming Zou, Muhan Zeng, Yingfei Xiong, Zhoulai Fu, Lu Zhang, and Zhendong Su (Peking University, China; IT University of Copenhagen, Denmark; ETH Zurich, Switzerland) Publisher's Version Article: popl20main-p222-p doi:10.1145/3371128
	Garcia-Contreras, Isabel	Proc. ACM Program. Lang., vol. 4, issue POPL: "Abstract Extensionality: On ..." Abstract Extensionality: On the Properties of Incomplete Abstract Interpretations Roberto Bruni, Roberto Giacobazzi, Roberta Gori, Isabel Garcia-Contreras, and Dusko Pavlovic (University of Pisa, Italy; University of Verona, Italy; IMDEA Software Institute, Spain; Universidad Politécnica de Madrid, Spain; University of Hawaii, USA) Publisher's Version Article: popl20main-p99-p doi:10.1145/3371096
	Garg, Deepak	Proc. ACM Program. Lang., vol. 4, issue POPL: "The High-Level Benefits of ..." The High-Level Benefits of Low-Level Sandboxing Michael Sammler, Deepak Garg, Derek Dreyer, and Tadeusz Litak (MPI-SWS, Germany; Friedrich-Alexander University Erlangen-Nürnberg, Germany) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p114-p doi:10.1145/3371100
	Genco, Francesco A.	Proc. ACM Program. Lang., vol. 4, issue POPL: "Par Means Parallel: Multiplicative ..." Par Means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs Federico Aschieri and Francesco A. Genco (TU Vienna, Austria; University of Paris 1, France) Publisher's Version Article: popl20main-p62-p doi:10.1145/3371086
	Giacobazzi, Roberto	Proc. ACM Program. Lang., vol. 4, issue POPL: "Abstract Extensionality: On ..." Abstract Extensionality: On the Properties of Incomplete Abstract Interpretations Roberto Bruni, Roberto Giacobazzi, Roberta Gori, Isabel Garcia-Contreras, and Dusko Pavlovic (University of Pisa, Italy; University of Verona, Italy; IMDEA Software Institute, Spain; Universidad Politécnica de Madrid, Spain; University of Hawaii, USA) Publisher's Version Article: popl20main-p99-p doi:10.1145/3371096
	Giesl, Jürgen	Proc. ACM Program. Lang., vol. 4, issue POPL: "Aiming Low Is Harder: Induction ..." Aiming Low Is Harder: Induction for Lower Bounds in Probabilistic Program Verification Marcel Hark, Benjamin Lucien Kaminski, Jürgen Giesl, and Joost-Pieter Katoen (RWTH Aachen University, Germany) Publisher's Version Article: popl20main-p127-p doi:10.1145/3371105
	Gori, Roberta	Proc. ACM Program. Lang., vol. 4, issue POPL: "Abstract Extensionality: On ..." Abstract Extensionality: On the Properties of Incomplete Abstract Interpretations Roberto Bruni, Roberto Giacobazzi, Roberta Gori, Isabel Garcia-Contreras, and Dusko Pavlovic (University of Pisa, Italy; University of Verona, Italy; IMDEA Software Institute, Spain; Universidad Politécnica de Madrid, Spain; University of Hawaii, USA) Publisher's Version Article: popl20main-p99-p doi:10.1145/3371096
	Greenberg, Michael	Proc. ACM Program. Lang., vol. 4, issue POPL: "Executable Formal Semantics ..." Executable Formal Semantics for the POSIX Shell Michael Greenberg and Austin J. Blatt (Pomona College, USA; Puppet Labs, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p153-p doi:10.1145/3371111
	Grégoire, Benjamin	Proc. ACM Program. Lang., vol. 4, issue POPL: "Formal Verification of a Constant-Time ..." Formal Verification of a Constant-Time Preserving C Compiler Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, and Alix Trieu (MPI for Security and Privacy, Germany; IMDEA Software Institute, Spain; University of Rennes, France; Inria, France; CNRS, France; IRISA, France; Aarhus University, Denmark) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p31-p doi:10.1145/3371075
	Groves, Lindsay	Proc. ACM Program. Lang., vol. 4, issue POPL: "Decidable Subtyping for Path ..." Decidable Subtyping for Path Dependent Types Julian Mackay, Alex Potanin, Jonathan Aldrich, and Lindsay Groves (Victoria University of Wellington, New Zealand; Carnegie Mellon University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p248-p doi:10.1145/3371134
	Gu, Ronghui	Proc. ACM Program. Lang., vol. 4, issue POPL: "Virtual Timeline: A Formal ..." Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation Mengqi Liu, Lionel Rieg, Zhong Shao, Ronghui Gu, David Costanzo, Jung-Eun Kim, and Man-Ki Yoon (Yale University, USA; Grenoble Alps University, France; CNRS, France; Grenoble INP, France; VERIMAG, France; Columbia University, USA) Publisher's Version Artifacts Functional Article: popl20main-p73-p doi:10.1145/3371088
	Guo, Zheng	Proc. ACM Program. Lang., vol. 4, issue POPL: "Program Synthesis by Type-Guided ..." Program Synthesis by Type-Guided Abstraction Refinement Zheng Guo, Michael James, David Justo, Jiaxiao Zhou, Ziteng Wang, Ranjit Jhala, and Nadia Polikarpova (University of California at San Diego, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p40-p doi:10.1145/3371080
	Gupta, Aarti	Proc. ACM Program. Lang., vol. 4, issue POPL: "Abstract Interpretation of ..." Abstract Interpretation of Distributed Network Control Planes Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker (Microsoft Research, USA; Princeton University, USA; University of Washington, USA; Intentionet, USA) Publisher's Version Article: popl20main-p150-p doi:10.1145/3371110
	Handley, Martin A. T.	Proc. ACM Program. Lang., vol. 4, issue POPL: "Liquidate Your Assets: Reasoning ..." Liquidate Your Assets: Reasoning about Resource Usage in Liquid Haskell Martin A. T. Handley, Niki Vazou, and Graham Hutton (University of Nottingham, UK; IMDEA Software Institute, Spain) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p94-p doi:10.1145/3371092
	Hark, Marcel	Proc. ACM Program. Lang., vol. 4, issue POPL: "Aiming Low Is Harder: Induction ..." Aiming Low Is Harder: Induction for Lower Bounds in Probabilistic Program Verification Marcel Hark, Benjamin Lucien Kaminski, Jürgen Giesl, and Joost-Pieter Katoen (RWTH Aachen University, Germany) Publisher's Version Article: popl20main-p127-p doi:10.1145/3371105
	He, Paul	Proc. ACM Program. Lang., vol. 4, issue POPL: "Interaction Trees: Representing ..." Interaction Trees: Representing Recursive and Impure Programs in Coq Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic (University of Pennsylvania, USA; Seoul National University, South Korea; BedRock Systems, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p177-p doi:10.1145/3371119
	Hicks, Michael	Proc. ACM Program. Lang., vol. 4, issue POPL: "A Language for Probabilistically ..." A Language for Probabilistically Oblivious Computation David Darais, Ian Sweet, Chang Liu, and Michael Hicks (University of Vermont, USA; University of Maryland, USA; Citadel Securities, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl20main-p175-p doi:10.1145/3371118
	Hinrichsen, Jonas Kastberg	Proc. ACM Program. Lang., vol. 4, issue POPL: "Actris: Session-Type Based ..." Actris: Session-Type Based Reasoning in Separation Logic Jonas Kastberg Hinrichsen, Jesper Bengtson, and Robbert Krebbers (IT University of Copenhagen, Denmark; Delft University of Technology, Netherlands) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p29-p doi:10.1145/3371074
	Hirschowitz, André	Proc. ACM Program. Lang., vol. 4, issue POPL: "Reduction Monads and Their ..." Reduction Monads and Their Signatures Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, and Marco Maggesi (University of Birmingham, UK; University of Côte d'Azur, France; IMT Atlantique, France; University of Florence, Italy) Publisher's Version Article: popl20main-p112-p doi:10.1145/3371099
	Hriţcu, Cătălin	Proc. ACM Program. Lang., vol. 4, issue POPL: "The Next 700 Relational Program ..." The Next 700 Relational Program Logics Kenji Maillard, Cătălin Hriţcu, Exequiel Rivas, and Antoine Van Muylder (Inria, France; ENS, France; University of Paris, France) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p24-p doi:10.1145/3371072
	Hsu, Justin	Proc. ACM Program. Lang., vol. 4, issue POPL: "Relational Proofs for Quantum ..." Relational Proofs for Quantum Programs Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, and Li Zhou (MPI for Security and Privacy, Germany; IMDEA Software Institute, Spain; University of Wisconsin-Madison, USA; University of Technology Sydney, Australia; Institute of Software at Chinese Academy of Sciences, China; Tsinghua University, China) Publisher's Version Article: popl20main-p78-p doi:10.1145/3371089 Proc. ACM Program. Lang., vol. 4, issue POPL: "A Probabilistic Separation ..." A Probabilistic Separation Logic Gilles Barthe, Justin Hsu, and Kevin Liao (MPI for Security and Privacy, Germany; IMDEA Software Institute, Spain; University of Wisconsin-Madison, USA; University of Illinois at Urbana-Champaign, USA) Publisher's Version Article: popl20main-p202-p doi:10.1145/3371123 Proc. ACM Program. Lang., vol. 4, issue POPL: "Guarded Kleene Algebra with ..." Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time Steffen Smolka, Nate Foster, Justin Hsu, Tobias Kappé, Dexter Kozen, and Alexandra Silva (Cornell University, USA; University of Wisconsin-Madison, USA; University College London, UK) Publisher's Version Article: popl20main-p229-p doi:10.1145/3371129
	Hu, Jason Z. S.	Proc. ACM Program. Lang., vol. 4, issue POPL: "Undecidability of D<: ..." Undecidability of D<: and Its Decidable Fragments Jason Z. S. Hu and Ondřej Lhoták (McGill University, Canada; University of Waterloo, Canada) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p35-p doi:10.1145/3371077
	Hur, Chung-Kil	Proc. ACM Program. Lang., vol. 4, issue POPL: "CompCertM: CompCert with C-Assembly ..." CompCertM: CompCert with C-Assembly Linking and Lightweight Modular Verification Youngju Song, Minki Cho, Dongjoo Kim, Yonghyun Kim, Jeehoon Kang, and Chung-Kil Hur (Seoul National University, South Korea; KAIST, South Korea) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p93-p doi:10.1145/3371091 Proc. ACM Program. Lang., vol. 4, issue POPL: "Interaction Trees: Representing ..." Interaction Trees: Representing Recursive and Impure Programs in Coq Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic (University of Pennsylvania, USA; Seoul National University, South Korea; BedRock Systems, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p177-p doi:10.1145/3371119
	Hutin, Rémi	Proc. ACM Program. Lang., vol. 4, issue POPL: "Formal Verification of a Constant-Time ..." Formal Verification of a Constant-Time Preserving C Compiler Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, and Alix Trieu (MPI for Security and Privacy, Germany; IMDEA Software Institute, Spain; University of Rennes, France; Inria, France; CNRS, France; IRISA, France; Aarhus University, Denmark) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p31-p doi:10.1145/3371075
	Hutton, Graham	Proc. ACM Program. Lang., vol. 4, issue POPL: "Liquidate Your Assets: Reasoning ..." Liquidate Your Assets: Reasoning about Resource Usage in Liquid Haskell Martin A. T. Handley, Niki Vazou, and Graham Hutton (University of Nottingham, UK; IMDEA Software Institute, Spain) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p94-p doi:10.1145/3371092
	Immerman, Neil	Proc. ACM Program. Lang., vol. 4, issue POPL: "Complexity and Information ..." Complexity and Information in Invariant Inference Yotam M. Y. Feldman, Neil Immerman, Mooly Sagiv, and Sharon Shoham (Tel Aviv University, Israel; University of Massachusetts, USA) Publisher's Version Article: popl20main-p25-p doi:10.1145/3371073
	Jaber, Guilhem	Proc. ACM Program. Lang., vol. 4, issue POPL: "SyTeCi: Automating Contextual ..." SyTeCi: Automating Contextual Equivalence for Higher-Order Programs with References Guilhem Jaber (University of Nantes, France; LS2N CNRS, France; Inria, France) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl20main-p219-p doi:10.1145/3371127
	Jabs, Julian	Proc. ACM Program. Lang., vol. 4, issue POPL: "Decomposition Diversity with ..." Decomposition Diversity with Symmetric Data and Codata David Binder, Julian Jabs, Ingo Skupin, and Klaus Ostermann (University of Tübingen, Germany) Publisher's Version Artifacts Functional Article: popl20main-p105-p doi:10.1145/3371098
	Jacobs, Bart	Proc. ACM Program. Lang., vol. 4, issue POPL: "The Future is Ours: Prophecy ..." The Future is Ours: Prophecy Variables in Separation Logic Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, and Bart Jacobs (MPI-SWS, Germany; ETH Zurich, Switzerland; University of Waterloo, Canada; KU Leuven, Belgium) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p157-p doi:10.1145/3371113
	James, Michael	Proc. ACM Program. Lang., vol. 4, issue POPL: "Program Synthesis by Type-Guided ..." Program Synthesis by Type-Guided Abstraction Refinement Zheng Guo, Michael James, David Justo, Jiaxiao Zhou, Ziteng Wang, Ranjit Jhala, and Nadia Polikarpova (University of California at San Diego, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p40-p doi:10.1145/3371080
	Jamner, Dustin	Proc. ACM Program. Lang., vol. 4, issue POPL: "Graduality and Parametricity: ..." Graduality and Parametricity: Together Again for the First Time Max S. New, Dustin Jamner, and Amal Ahmed (Northeastern University, USA) Publisher's Version Article: popl20main-p167-p doi:10.1145/3371114
	Jhala, Ranjit	Proc. ACM Program. Lang., vol. 4, issue POPL: "Program Synthesis by Type-Guided ..." Program Synthesis by Type-Guided Abstraction Refinement Zheng Guo, Michael James, David Justo, Jiaxiao Zhou, Ziteng Wang, Ranjit Jhala, and Nadia Polikarpova (University of California at San Diego, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p40-p doi:10.1145/3371080
	Jones, Mark P.	Proc. ACM Program. Lang., vol. 4, issue POPL: "Partial Type Constructors: ..." Partial Type Constructors: Or, Making Ad Hoc Datatypes Less Ad Hoc Mark P. Jones, J. Garrett Morris, and Richard A. Eisenberg (Portland State University, USA; University of Kansas, USA; Bryn Mawr College, USA; Tweag I/O, UK) Publisher's Version Article: popl20main-p136-p doi:10.1145/3371108
	Jourdan, Jacques-Henri	Proc. ACM Program. Lang., vol. 4, issue POPL: "Spy Game: Verifying a Local ..." Spy Game: Verifying a Local Generic Solver in Iris Paulo Emílio de Vilhena, François Pottier, and Jacques-Henri Jourdan (Inria, France; CNRS, France; LRI, France; University of Paris-Saclay, France) Publisher's Version Article: popl20main-p117-p doi:10.1145/3371101 Proc. ACM Program. Lang., vol. 4, issue POPL: "RustBelt Meets Relaxed Memory ..." RustBelt Meets Relaxed Memory Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser, and Derek Dreyer (MPI-SWS, Germany; LRI, France; CNRS, France; University of Paris-Saclay, France) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p124-p doi:10.1145/3371102
	Jung, Ralf	Proc. ACM Program. Lang., vol. 4, issue POPL: "Stacked Borrows: An Aliasing ..." Stacked Borrows: An Aliasing Model for Rust Ralf Jung, Hoang-Hai Dang, Jeehoon Kang, and Derek Dreyer (MPI-SWS, Germany; Mozilla, USA; KAIST, South Korea) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p147-p doi:10.1145/3371109 Proc. ACM Program. Lang., vol. 4, issue POPL: "The Future is Ours: Prophecy ..." The Future is Ours: Prophecy Variables in Separation Logic Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, and Bart Jacobs (MPI-SWS, Germany; ETH Zurich, Switzerland; University of Waterloo, Canada; KU Leuven, Belgium) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p157-p doi:10.1145/3371113
	Justo, David	Proc. ACM Program. Lang., vol. 4, issue POPL: "Program Synthesis by Type-Guided ..." Program Synthesis by Type-Guided Abstraction Refinement Zheng Guo, Michael James, David Justo, Jiaxiao Zhou, Ziteng Wang, Ranjit Jhala, and Nadia Polikarpova (University of California at San Diego, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p40-p doi:10.1145/3371080
	Kaiser, Jan-Oliver	Proc. ACM Program. Lang., vol. 4, issue POPL: "RustBelt Meets Relaxed Memory ..." RustBelt Meets Relaxed Memory Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser, and Derek Dreyer (MPI-SWS, Germany; LRI, France; CNRS, France; University of Paris-Saclay, France) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p124-p doi:10.1145/3371102
	Kaminski, Benjamin Lucien	Proc. ACM Program. Lang., vol. 4, issue POPL: "Aiming Low Is Harder: Induction ..." Aiming Low Is Harder: Induction for Lower Bounds in Probabilistic Program Verification Marcel Hark, Benjamin Lucien Kaminski, Jürgen Giesl, and Joost-Pieter Katoen (RWTH Aachen University, Germany) Publisher's Version Article: popl20main-p127-p doi:10.1145/3371105
	Kang, Jeehoon	Proc. ACM Program. Lang., vol. 4, issue POPL: "CompCertM: CompCert with C-Assembly ..." CompCertM: CompCert with C-Assembly Linking and Lightweight Modular Verification Youngju Song, Minki Cho, Dongjoo Kim, Yonghyun Kim, Jeehoon Kang, and Chung-Kil Hur (Seoul National University, South Korea; KAIST, South Korea) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p93-p doi:10.1145/3371091 Proc. ACM Program. Lang., vol. 4, issue POPL: "Stacked Borrows: An Aliasing ..." Stacked Borrows: An Aliasing Model for Rust Ralf Jung, Hoang-Hai Dang, Jeehoon Kang, and Derek Dreyer (MPI-SWS, Germany; Mozilla, USA; KAIST, South Korea) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p147-p doi:10.1145/3371109
	Kappé, Tobias	Proc. ACM Program. Lang., vol. 4, issue POPL: "Guarded Kleene Algebra with ..." Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time Steffen Smolka, Nate Foster, Justin Hsu, Tobias Kappé, Dexter Kozen, and Alexandra Silva (Cornell University, USA; University of Wisconsin-Madison, USA; University College London, UK) Publisher's Version Article: popl20main-p229-p doi:10.1145/3371129
	Katoen, Joost-Pieter	Proc. ACM Program. Lang., vol. 4, issue POPL: "Aiming Low Is Harder: Induction ..." Aiming Low Is Harder: Induction for Lower Bounds in Probabilistic Program Verification Marcel Hark, Benjamin Lucien Kaminski, Jürgen Giesl, and Joost-Pieter Katoen (RWTH Aachen University, Germany) Publisher's Version Article: popl20main-p127-p doi:10.1145/3371105
	Kavvos, G. A.	Proc. ACM Program. Lang., vol. 4, issue POPL: "Recurrence Extraction for ..." Recurrence Extraction for Functional Programs through Call-by-Push-Value G. A. Kavvos, Edward Morehouse, Daniel R. Licata, and Norman Danner (Wesleyan University, USA) Publisher's Version Article: popl20main-p46-p doi:10.1145/3371083
	Kim, Deokhwan	Proc. ACM Program. Lang., vol. 4, issue POPL: "Synthesizing Replacement Classes ..." Synthesizing Replacement Classes Malavika Samak, Deokhwan Kim, and Martin C. Rinard (Massachusetts Institute of Technology, USA) Publisher's Version Article: popl20main-p186-p doi:10.1145/3371120
	Kim, Dongjoo	Proc. ACM Program. Lang., vol. 4, issue POPL: "CompCertM: CompCert with C-Assembly ..." CompCertM: CompCert with C-Assembly Linking and Lightweight Modular Verification Youngju Song, Minki Cho, Dongjoo Kim, Yonghyun Kim, Jeehoon Kang, and Chung-Kil Hur (Seoul National University, South Korea; KAIST, South Korea) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p93-p doi:10.1145/3371091
	Kim, Jung-Eun	Proc. ACM Program. Lang., vol. 4, issue POPL: "Virtual Timeline: A Formal ..." Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation Mengqi Liu, Lionel Rieg, Zhong Shao, Ronghui Gu, David Costanzo, Jung-Eun Kim, and Man-Ki Yoon (Yale University, USA; Grenoble Alps University, France; CNRS, France; Grenoble INP, France; VERIMAG, France; Columbia University, USA) Publisher's Version Artifacts Functional Article: popl20main-p73-p doi:10.1145/3371088
	Kim, Sung Kook	Proc. ACM Program. Lang., vol. 4, issue POPL: "Deterministic Parallel Fixpoint ..." Deterministic Parallel Fixpoint Computation Sung Kook Kim, Arnaud J. Venet, and Aditya V. Thakur (University of California at Davis, USA; Facebook, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p45-p doi:10.1145/3371082
	Kim, Yonghyun	Proc. ACM Program. Lang., vol. 4, issue POPL: "CompCertM: CompCert with C-Assembly ..." CompCertM: CompCert with C-Assembly Linking and Lightweight Modular Verification Youngju Song, Minki Cho, Dongjoo Kim, Yonghyun Kim, Jeehoon Kang, and Chung-Kil Hur (Seoul National University, South Korea; KAIST, South Korea) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p93-p doi:10.1145/3371091
	King, Alexis	Proc. ACM Program. Lang., vol. 4, issue POPL: "Does Blame Shifting Work? ..." Does Blame Shifting Work? Lukas Lazarek, Alexis King, Samanvitha Sundar, Robert Bruce Findler, and Christos Dimoulas (Northwestern University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl20main-p246-p doi:10.1145/3371133
	Kozen, Dexter	Proc. ACM Program. Lang., vol. 4, issue POPL: "Semantics of Higher-Order ..." Semantics of Higher-Order Probabilistic Programs with Conditioning Fredrik Dahlqvist and Dexter Kozen (University College London, UK; Imperial College London, UK; Cornell University, USA) Publisher's Version Article: popl20main-p213-p doi:10.1145/3371125 Proc. ACM Program. Lang., vol. 4, issue POPL: "Guarded Kleene Algebra with ..." Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time Steffen Smolka, Nate Foster, Justin Hsu, Tobias Kappé, Dexter Kozen, and Alexandra Silva (Cornell University, USA; University of Wisconsin-Madison, USA; University College London, UK) Publisher's Version Article: popl20main-p229-p doi:10.1145/3371129
	Krebbers, Robbert	Proc. ACM Program. Lang., vol. 4, issue POPL: "Actris: Session-Type Based ..." Actris: Session-Type Based Reasoning in Separation Logic Jonas Kastberg Hinrichsen, Jesper Bengtson, and Robbert Krebbers (IT University of Copenhagen, Denmark; Delft University of Technology, Netherlands) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p29-p doi:10.1145/3371074
	Krishnaswami, Neel	Proc. ACM Program. Lang., vol. 4, issue POPL: "Seminaïve Evaluation for ..." Seminaïve Evaluation for a Higher-Order Functional Language Michael Arntzenius and Neel Krishnaswami (University of Birmingham, UK; University of Cambridge, UK) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl20main-p91-p doi:10.1145/3371090
	Krogmeier, Paul	Proc. ACM Program. Lang., vol. 4, issue POPL: "Deciding Memory Safety for ..." Deciding Memory Safety for Single-Pass Heap-Manipulating Programs Umang Mathur, Adithya Murali, Paul Krogmeier, P. Madhusudan, and Mahesh Viswanathan (University of Illinois at Urbana-Champaign, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p125-p doi:10.1145/3371103
	Kunze, Fabian	Proc. ACM Program. Lang., vol. 4, issue POPL: "The Weak Call-by-Value λ-Calculus ..." The Weak Call-by-Value λ-Calculus Is Reasonable for Both Time and Space Yannick Forster, Fabian Kunze, and Marc Roth (Saarland University, Germany; M2CI, Germany; University of Oxford, UK) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p98-p doi:10.1145/3371095
	Lafont, Ambroise	Proc. ACM Program. Lang., vol. 4, issue POPL: "Reduction Monads and Their ..." Reduction Monads and Their Signatures Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, and Marco Maggesi (University of Birmingham, UK; University of Côte d'Azur, France; IMT Atlantique, France; University of Florence, Italy) Publisher's Version Article: popl20main-p112-p doi:10.1145/3371099
	Laporte, Vincent	Proc. ACM Program. Lang., vol. 4, issue POPL: "Formal Verification of a Constant-Time ..." Formal Verification of a Constant-Time Preserving C Compiler Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, and Alix Trieu (MPI for Security and Privacy, Germany; IMDEA Software Institute, Spain; University of Rennes, France; Inria, France; CNRS, France; IRISA, France; Aarhus University, Denmark) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p31-p doi:10.1145/3371075
	Lazarek, Lukas	Proc. ACM Program. Lang., vol. 4, issue POPL: "Does Blame Shifting Work? ..." Does Blame Shifting Work? Lukas Lazarek, Alexis King, Samanvitha Sundar, Robert Bruce Findler, and Christos Dimoulas (Northwestern University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl20main-p246-p doi:10.1145/3371133
	Lee, Wonyeol	Proc. ACM Program. Lang., vol. 4, issue POPL: "Towards Verified Stochastic ..." Towards Verified Stochastic Variational Inference for Probabilistic Programs Wonyeol Lee, Hangyeol Yu, Xavier Rival, and Hongseok Yang (KAIST, South Korea; Inria, France; ENS, France; CNRS, France; PSL University, France) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p48-p doi:10.1145/3371084
	Lepigre, Rodolphe	Proc. ACM Program. Lang., vol. 4, issue POPL: "The Future is Ours: Prophecy ..." The Future is Ours: Prophecy Variables in Separation Logic Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, and Bart Jacobs (MPI-SWS, Germany; ETH Zurich, Switzerland; University of Waterloo, Canada; KU Leuven, Belgium) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p157-p doi:10.1145/3371113
	Lew, Alexander K.	Proc. ACM Program. Lang., vol. 4, issue POPL: "Trace Types and Denotational ..." Trace Types and Denotational Semantics for Sound Programmable Inference in Probabilistic Languages Alexander K. Lew, Marco F. Cusumano-Towner, Benjamin Sherman, Michael Carbin, and Vikash K. Mansinghka (Massachusetts Institute of Technology, USA) Publisher's Version Article: popl20main-p69-p doi:10.1145/3371087
	Lhoták, Ondřej	Proc. ACM Program. Lang., vol. 4, issue POPL: "Undecidability of D<: ..." Undecidability of D<: and Its Decidable Fragments Jason Z. S. Hu and Ondřej Lhoták (McGill University, Canada; University of Waterloo, Canada) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p35-p doi:10.1145/3371077
	Liao, Kevin	Proc. ACM Program. Lang., vol. 4, issue POPL: "A Probabilistic Separation ..." A Probabilistic Separation Logic Gilles Barthe, Justin Hsu, and Kevin Liao (MPI for Security and Privacy, Germany; IMDEA Software Institute, Spain; University of Wisconsin-Madison, USA; University of Illinois at Urbana-Champaign, USA) Publisher's Version Article: popl20main-p202-p doi:10.1145/3371123
	Licata, Daniel R.	Proc. ACM Program. Lang., vol. 4, issue POPL: "Recurrence Extraction for ..." Recurrence Extraction for Functional Programs through Call-by-Push-Value G. A. Kavvos, Edward Morehouse, Daniel R. Licata, and Norman Danner (Wesleyan University, USA) Publisher's Version Article: popl20main-p46-p doi:10.1145/3371083
	Litak, Tadeusz	Proc. ACM Program. Lang., vol. 4, issue POPL: "The High-Level Benefits of ..." The High-Level Benefits of Low-Level Sandboxing Michael Sammler, Deepak Garg, Derek Dreyer, and Tadeusz Litak (MPI-SWS, Germany; Friedrich-Alexander University Erlangen-Nürnberg, Germany) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p114-p doi:10.1145/3371100
	Liu, Chang	Proc. ACM Program. Lang., vol. 4, issue POPL: "A Language for Probabilistically ..." A Language for Probabilistically Oblivious Computation David Darais, Ian Sweet, Chang Liu, and Michael Hicks (University of Vermont, USA; University of Maryland, USA; Citadel Securities, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl20main-p175-p doi:10.1145/3371118
	Liu, Mengqi	Proc. ACM Program. Lang., vol. 4, issue POPL: "Virtual Timeline: A Formal ..." Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation Mengqi Liu, Lionel Rieg, Zhong Shao, Ronghui Gu, David Costanzo, Jung-Eun Kim, and Man-Ki Yoon (Yale University, USA; Grenoble Alps University, France; CNRS, France; Grenoble INP, France; VERIMAG, France; Columbia University, USA) Publisher's Version Artifacts Functional Article: popl20main-p73-p doi:10.1145/3371088
	Mackay, Julian	Proc. ACM Program. Lang., vol. 4, issue POPL: "Decidable Subtyping for Path ..." Decidable Subtyping for Path Dependent Types Julian Mackay, Alex Potanin, Jonathan Aldrich, and Lindsay Groves (Victoria University of Wellington, New Zealand; Carnegie Mellon University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p248-p doi:10.1145/3371134
	Madhusudan, P.	Proc. ACM Program. Lang., vol. 4, issue POPL: "Deciding Memory Safety for ..." Deciding Memory Safety for Single-Pass Heap-Manipulating Programs Umang Mathur, Adithya Murali, Paul Krogmeier, P. Madhusudan, and Mahesh Viswanathan (University of Illinois at Urbana-Champaign, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p125-p doi:10.1145/3371103
	Maggesi, Marco	Proc. ACM Program. Lang., vol. 4, issue POPL: "Reduction Monads and Their ..." Reduction Monads and Their Signatures Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, and Marco Maggesi (University of Birmingham, UK; University of Côte d'Azur, France; IMT Atlantique, France; University of Florence, Italy) Publisher's Version Article: popl20main-p112-p doi:10.1145/3371099
	Mahajan, Ratul	Proc. ACM Program. Lang., vol. 4, issue POPL: "Abstract Interpretation of ..." Abstract Interpretation of Distributed Network Control Planes Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker (Microsoft Research, USA; Princeton University, USA; University of Washington, USA; Intentionet, USA) Publisher's Version Article: popl20main-p150-p doi:10.1145/3371110
	Maillard, Kenji	Proc. ACM Program. Lang., vol. 4, issue POPL: "The Next 700 Relational Program ..." The Next 700 Relational Program Logics Kenji Maillard, Cătălin Hriţcu, Exequiel Rivas, and Antoine Van Muylder (Inria, France; ENS, France; University of Paris, France) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p24-p doi:10.1145/3371072
	Malecha, Gregory	Proc. ACM Program. Lang., vol. 4, issue POPL: "Interaction Trees: Representing ..." Interaction Trees: Representing Recursive and Impure Programs in Coq Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic (University of Pennsylvania, USA; Seoul National University, South Korea; BedRock Systems, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p177-p doi:10.1145/3371119
	Mansinghka, Vikash K.	Proc. ACM Program. Lang., vol. 4, issue POPL: "Trace Types and Denotational ..." Trace Types and Denotational Semantics for Sound Programmable Inference in Probabilistic Languages Alexander K. Lew, Marco F. Cusumano-Towner, Benjamin Sherman, Michael Carbin, and Vikash K. Mansinghka (Massachusetts Institute of Technology, USA) Publisher's Version Article: popl20main-p69-p doi:10.1145/3371087 Proc. ACM Program. Lang., vol. 4, issue POPL: "Optimal Approximate Sampling ..." Optimal Approximate Sampling from Discrete Probability Distributions Feras A. Saad, Cameron E. Freer, Martin C. Rinard, and Vikash K. Mansinghka (Massachusetts Institute of Technology, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl20main-p126-p doi:10.1145/3371104
	Manzonetto, Giulio	Proc. ACM Program. Lang., vol. 4, issue POPL: "Taylor Subsumes Scott, Berry, ..." Taylor Subsumes Scott, Berry, Kahn and Plotkin Davide Barbarossa and Giulio Manzonetto (University of Paris 13, France) Publisher's Version Article: popl20main-p6-p doi:10.1145/3371069
	Marché, Claude	Proc. ACM Program. Lang., vol. 4, issue POPL: "Deductive Verification with ..." Deductive Verification with Ghost Monitors Martin Clochard, Claude Marché, and Andrei Paskevich (ETH Zurich, Switzerland; Inria, France; University of Paris-Saclay, France; LRI, France; University of Paris-Sud, France; CNRS, France) Publisher's Version Article: popl20main-p7-p doi:10.1145/3371070
	Mathur, Umang	Proc. ACM Program. Lang., vol. 4, issue POPL: "Deciding Memory Safety for ..." Deciding Memory Safety for Single-Pass Heap-Manipulating Programs Umang Mathur, Adithya Murali, Paul Krogmeier, P. Madhusudan, and Mahesh Viswanathan (University of Illinois at Urbana-Champaign, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p125-p doi:10.1145/3371103
	Mazza, Damiano	Proc. ACM Program. Lang., vol. 4, issue POPL: "Backpropagation in the Simply ..." Backpropagation in the Simply Typed Lambda-Calculus with Linear Negation Aloïs Brunel, Damiano Mazza, and Michele Pagani (Deepomatic, France; CNRS, France; IRIF, France; University of Paris Diderot, France) Publisher's Version Article: popl20main-p243-p doi:10.1145/3371132
	Mendelson, Jonathan	Proc. ACM Program. Lang., vol. 4, issue POPL: "Provenance-Guided Synthesis ..." Provenance-Guided Synthesis of Datalog Programs Mukund Raghothaman, Jonathan Mendelson, David Zhao, Mayur Naik, and Bernhard Scholz (University of Southern California, USA; University of Pennsylvania, USA; University of Sydney, Australia) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p236-p doi:10.1145/3371130
	Meyer, Roland	Proc. ACM Program. Lang., vol. 4, issue POPL: "Pointer Life Cycle Types for ..." Pointer Life Cycle Types for Lock-Free Data Structures with Memory Reclamation Roland Meyer and Sebastian Wolff (TU Braunschweig, Germany) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p265-p doi:10.1145/3371136
	Migeed, Zeina	Proc. ACM Program. Lang., vol. 4, issue POPL: "What Is Decidable about Gradual ..." What Is Decidable about Gradual Types? Zeina Migeed and Jens Palsberg (University of California at Los Angeles, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p104-p doi:10.1145/3371097
	Misailovic, Sasa	Proc. ACM Program. Lang., vol. 4, issue POPL: "Augmented Example-Based Synthesis ..." Augmented Example-Based Synthesis using Relational Perturbation Properties Shengwei An, Rishabh Singh, Sasa Misailovic, and Roopsha Samanta (Purdue University, USA; Google, USA; University of Illinois at Urbana-Champaign, USA) Publisher's Version Article: popl20main-p204-p doi:10.1145/3371124
	Morehouse, Edward	Proc. ACM Program. Lang., vol. 4, issue POPL: "Recurrence Extraction for ..." Recurrence Extraction for Functional Programs through Call-by-Push-Value G. A. Kavvos, Edward Morehouse, Daniel R. Licata, and Norman Danner (Wesleyan University, USA) Publisher's Version Article: popl20main-p46-p doi:10.1145/3371083
	Morris, J. Garrett	Proc. ACM Program. Lang., vol. 4, issue POPL: "Partial Type Constructors: ..." Partial Type Constructors: Or, Making Ad Hoc Datatypes Less Ad Hoc Mark P. Jones, J. Garrett Morris, and Richard A. Eisenberg (Portland State University, USA; University of Kansas, USA; Bryn Mawr College, USA; Tweag I/O, UK) Publisher's Version Article: popl20main-p136-p doi:10.1145/3371108
	Murali, Adithya	Proc. ACM Program. Lang., vol. 4, issue POPL: "Deciding Memory Safety for ..." Deciding Memory Safety for Single-Pass Heap-Manipulating Programs Umang Mathur, Adithya Murali, Paul Krogmeier, P. Madhusudan, and Mahesh Viswanathan (University of Illinois at Urbana-Champaign, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p125-p doi:10.1145/3371103
	Naik, Mayur	Proc. ACM Program. Lang., vol. 4, issue POPL: "Provenance-Guided Synthesis ..." Provenance-Guided Synthesis of Datalog Programs Mukund Raghothaman, Jonathan Mendelson, David Zhao, Mayur Naik, and Bernhard Scholz (University of Southern California, USA; University of Pennsylvania, USA; University of Sydney, Australia) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p236-p doi:10.1145/3371130
	Namjoshi, Kedar S.	Proc. ACM Program. Lang., vol. 4, issue POPL: "Synthesis of Coordination ..." Synthesis of Coordination Programs from Linear Temporal Specifications Suguman Bansal, Kedar S. Namjoshi, and Yaniv Sa'ar (Rice University, USA; Nokia Bell Labs, USA; Nokia Bell Labs, Israel) Publisher's Version Artifacts Functional Article: popl20main-p194-p doi:10.1145/3371122
	Neiger, Gil	Proc. ACM Program. Lang., vol. 4, issue POPL: "Persistency Semantics of the ..." Persistency Semantics of the Intel-x86 Architecture Azalea Raad, John Wickerson, Gil Neiger, and Viktor Vafeiadis (MPI-SWS, Germany; Imperial College London, UK; Intel Labs, USA) Publisher's Version Article: popl20main-p39-p doi:10.1145/3371079
	New, Max S.	Proc. ACM Program. Lang., vol. 4, issue POPL: "Graduality and Parametricity: ..." Graduality and Parametricity: Together Again for the First Time Max S. New, Dustin Jamner, and Amal Ahmed (Northeastern University, USA) Publisher's Version Article: popl20main-p167-p doi:10.1145/3371114
	O'Hearn, Peter W.	Proc. ACM Program. Lang., vol. 4, issue POPL: "Incorrectness Logic ..." Incorrectness Logic Peter W. O'Hearn (Facebook, UK; University College London, UK) Publisher's Version Article: popl20main-p36-p doi:10.1145/3371078
	Oliveira, Bruno C. d. S.	Proc. ACM Program. Lang., vol. 4, issue POPL: "Kind Inference for Datatypes ..." Kind Inference for Datatypes Ningning Xie, Richard A. Eisenberg, and Bruno C. d. S. Oliveira (University of Hong Kong, China; Bryn Mawr College, USA; Tweag I/O, UK) Publisher's Version Article: popl20main-p189-p doi:10.1145/3371121
	Ostermann, Klaus	Proc. ACM Program. Lang., vol. 4, issue POPL: "Decomposition Diversity with ..." Decomposition Diversity with Symmetric Data and Codata David Binder, Julian Jabs, Ingo Skupin, and Klaus Ostermann (University of Tübingen, Germany) Publisher's Version Artifacts Functional Article: popl20main-p105-p doi:10.1145/3371098
	Pagani, Michele	Proc. ACM Program. Lang., vol. 4, issue POPL: "Backpropagation in the Simply ..." Backpropagation in the Simply Typed Lambda-Calculus with Linear Negation Aloïs Brunel, Damiano Mazza, and Michele Pagani (Deepomatic, France; CNRS, France; IRIF, France; University of Paris Diderot, France) Publisher's Version Article: popl20main-p243-p doi:10.1145/3371132
	Palsberg, Jens	Proc. ACM Program. Lang., vol. 4, issue POPL: "What Is Decidable about Gradual ..." What Is Decidable about Gradual Types? Zeina Migeed and Jens Palsberg (University of California at Los Angeles, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p104-p doi:10.1145/3371097
	Parthasarathy, Gaurav	Proc. ACM Program. Lang., vol. 4, issue POPL: "The Future is Ours: Prophecy ..." The Future is Ours: Prophecy Variables in Separation Logic Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, and Bart Jacobs (MPI-SWS, Germany; ETH Zurich, Switzerland; University of Waterloo, Canada; KU Leuven, Belgium) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p157-p doi:10.1145/3371113
	Paskevich, Andrei	Proc. ACM Program. Lang., vol. 4, issue POPL: "Deductive Verification with ..." Deductive Verification with Ghost Monitors Martin Clochard, Claude Marché, and Andrei Paskevich (ETH Zurich, Switzerland; Inria, France; University of Paris-Saclay, France; LRI, France; University of Paris-Sud, France; CNRS, France) Publisher's Version Article: popl20main-p7-p doi:10.1145/3371070
	Pavlogiannis, Andreas	Proc. ACM Program. Lang., vol. 4, issue POPL: "Fast, Sound, and Effectively ..." Fast, Sound, and Effectively Complete Dynamic Race Prediction Andreas Pavlogiannis (Aarhus University, Denmark) Publisher's Version Article: popl20main-p50-p doi:10.1145/3371085
	Pavlovic, Dusko	Proc. ACM Program. Lang., vol. 4, issue POPL: "Abstract Extensionality: On ..." Abstract Extensionality: On the Properties of Incomplete Abstract Interpretations Roberto Bruni, Roberto Giacobazzi, Roberta Gori, Isabel Garcia-Contreras, and Dusko Pavlovic (University of Pisa, Italy; University of Verona, Italy; IMDEA Software Institute, Spain; Universidad Politécnica de Madrid, Spain; University of Hawaii, USA) Publisher's Version Article: popl20main-p99-p doi:10.1145/3371096
	Pédrot, Pierre-Marie	Proc. ACM Program. Lang., vol. 4, issue POPL: "The Fire Triangle: How to ..." The Fire Triangle: How to Mix Substitution, Dependent Elimination, and Effects Pierre-Marie Pédrot and Nicolas Tabareau (Inria, France) Publisher's Version Article: popl20main-p216-p doi:10.1145/3371126
	Pichardie, David	Proc. ACM Program. Lang., vol. 4, issue POPL: "Formal Verification of a Constant-Time ..." Formal Verification of a Constant-Time Preserving C Compiler Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, and Alix Trieu (MPI for Security and Privacy, Germany; IMDEA Software Institute, Spain; University of Rennes, France; Inria, France; CNRS, France; IRISA, France; Aarhus University, Denmark) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p31-p doi:10.1145/3371075
	Pierce, Benjamin C.	Proc. ACM Program. Lang., vol. 4, issue POPL: "Interaction Trees: Representing ..." Interaction Trees: Representing Recursive and Impure Programs in Coq Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic (University of Pennsylvania, USA; Seoul National University, South Korea; BedRock Systems, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p177-p doi:10.1145/3371119
	Piróg, Maciej	Proc. ACM Program. Lang., vol. 4, issue POPL: "Binders by Day, Labels by ..." Binders by Day, Labels by Night: Effect Instances via Lexically Scoped Handlers Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski (University of Wrocław, Poland) Publisher's Version Artifacts Functional Article: popl20main-p171-p doi:10.1145/3371116
	Plotkin, Gordon D.	Proc. ACM Program. Lang., vol. 4, issue POPL: "A Simple Differentiable Programming ..." A Simple Differentiable Programming Language Martín Abadi and Gordon D. Plotkin (Google Research, USA) Publisher's Version Article: popl20main-p129-p doi:10.1145/3371106
	Polesiuk, Piotr	Proc. ACM Program. Lang., vol. 4, issue POPL: "Binders by Day, Labels by ..." Binders by Day, Labels by Night: Effect Instances via Lexically Scoped Handlers Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski (University of Wrocław, Poland) Publisher's Version Artifacts Functional Article: popl20main-p171-p doi:10.1145/3371116
	Polikarpova, Nadia	Proc. ACM Program. Lang., vol. 4, issue POPL: "Program Synthesis by Type-Guided ..." Program Synthesis by Type-Guided Abstraction Refinement Zheng Guo, Michael James, David Justo, Jiaxiao Zhou, Ziteng Wang, Ranjit Jhala, and Nadia Polikarpova (University of California at San Diego, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p40-p doi:10.1145/3371080
	Potanin, Alex	Proc. ACM Program. Lang., vol. 4, issue POPL: "Decidable Subtyping for Path ..." Decidable Subtyping for Path Dependent Types Julian Mackay, Alex Potanin, Jonathan Aldrich, and Lindsay Groves (Victoria University of Wellington, New Zealand; Carnegie Mellon University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p248-p doi:10.1145/3371134
	Pottier, François	Proc. ACM Program. Lang., vol. 4, issue POPL: "Spy Game: Verifying a Local ..." Spy Game: Verifying a Local Generic Solver in Iris Paulo Emílio de Vilhena, François Pottier, and Jacques-Henri Jourdan (Inria, France; CNRS, France; LRI, France; University of Paris-Saclay, France) Publisher's Version Article: popl20main-p117-p doi:10.1145/3371101
	Pouzet, Marc	Proc. ACM Program. Lang., vol. 4, issue POPL: "Mechanized Semantics and Verified ..." Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset Timothy Bourke, Lélio Brun, and Marc Pouzet (Inria, France; ENS, France; PSL University, France; Sorbonne University, France) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p155-p doi:10.1145/3371112
	Raad, Azalea	Proc. ACM Program. Lang., vol. 4, issue POPL: "Persistency Semantics of the ..." Persistency Semantics of the Intel-x86 Architecture Azalea Raad, John Wickerson, Gil Neiger, and Viktor Vafeiadis (MPI-SWS, Germany; Imperial College London, UK; Intel Labs, USA) Publisher's Version Article: popl20main-p39-p doi:10.1145/3371079
	Raghothaman, Mukund	Proc. ACM Program. Lang., vol. 4, issue POPL: "Provenance-Guided Synthesis ..." Provenance-Guided Synthesis of Datalog Programs Mukund Raghothaman, Jonathan Mendelson, David Zhao, Mayur Naik, and Bernhard Scholz (University of Southern California, USA; University of Pennsylvania, USA; University of Sydney, Australia) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p236-p doi:10.1145/3371130
	Rapoport, Marianna	Proc. ACM Program. Lang., vol. 4, issue POPL: "The Future is Ours: Prophecy ..." The Future is Ours: Prophecy Variables in Separation Logic Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, and Bart Jacobs (MPI-SWS, Germany; ETH Zurich, Switzerland; University of Waterloo, Canada; KU Leuven, Belgium) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p157-p doi:10.1145/3371113
	Rezvan, Rojin	Proc. ACM Program. Lang., vol. 4, issue POPL: "Parameterized Verification ..." Parameterized Verification under TSO is PSPACE-Complete Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Rojin Rezvan (Uppsala University, Sweden; Sharif University of Technology, Iran) Publisher's Version Article: popl20main-p97-p doi:10.1145/3371094
	Rieg, Lionel	Proc. ACM Program. Lang., vol. 4, issue POPL: "Virtual Timeline: A Formal ..." Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation Mengqi Liu, Lionel Rieg, Zhong Shao, Ronghui Gu, David Costanzo, Jung-Eun Kim, and Man-Ki Yoon (Yale University, USA; Grenoble Alps University, France; CNRS, France; Grenoble INP, France; VERIMAG, France; Columbia University, USA) Publisher's Version Artifacts Functional Article: popl20main-p73-p doi:10.1145/3371088
	Rinard, Martin C.	Proc. ACM Program. Lang., vol. 4, issue POPL: "Optimal Approximate Sampling ..." Optimal Approximate Sampling from Discrete Probability Distributions Feras A. Saad, Cameron E. Freer, Martin C. Rinard, and Vikash K. Mansinghka (Massachusetts Institute of Technology, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl20main-p126-p doi:10.1145/3371104 Proc. ACM Program. Lang., vol. 4, issue POPL: "Synthesizing Replacement Classes ..." Synthesizing Replacement Classes Malavika Samak, Deokhwan Kim, and Martin C. Rinard (Massachusetts Institute of Technology, USA) Publisher's Version Article: popl20main-p186-p doi:10.1145/3371120
	Rival, Xavier	Proc. ACM Program. Lang., vol. 4, issue POPL: "Towards Verified Stochastic ..." Towards Verified Stochastic Variational Inference for Probabilistic Programs Wonyeol Lee, Hangyeol Yu, Xavier Rival, and Hongseok Yang (KAIST, South Korea; Inria, France; ENS, France; CNRS, France; PSL University, France) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p48-p doi:10.1145/3371084
	Rivas, Exequiel	Proc. ACM Program. Lang., vol. 4, issue POPL: "The Next 700 Relational Program ..." The Next 700 Relational Program Logics Kenji Maillard, Cătălin Hriţcu, Exequiel Rivas, and Antoine Van Muylder (Inria, France; ENS, France; University of Paris, France) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p24-p doi:10.1145/3371072
	Roth, Marc	Proc. ACM Program. Lang., vol. 4, issue POPL: "The Weak Call-by-Value λ-Calculus ..." The Weak Call-by-Value λ-Calculus Is Reasonable for Both Time and Space Yannick Forster, Fabian Kunze, and Marc Roth (Saarland University, Germany; M2CI, Germany; University of Oxford, UK) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p98-p doi:10.1145/3371095
	Saad, Feras A.	Proc. ACM Program. Lang., vol. 4, issue POPL: "Optimal Approximate Sampling ..." Optimal Approximate Sampling from Discrete Probability Distributions Feras A. Saad, Cameron E. Freer, Martin C. Rinard, and Vikash K. Mansinghka (Massachusetts Institute of Technology, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl20main-p126-p doi:10.1145/3371104
	Sa'ar, Yaniv	Proc. ACM Program. Lang., vol. 4, issue POPL: "Synthesis of Coordination ..." Synthesis of Coordination Programs from Linear Temporal Specifications Suguman Bansal, Kedar S. Namjoshi, and Yaniv Sa'ar (Rice University, USA; Nokia Bell Labs, USA; Nokia Bell Labs, Israel) Publisher's Version Artifacts Functional Article: popl20main-p194-p doi:10.1145/3371122
	Sagiv, Mooly	Proc. ACM Program. Lang., vol. 4, issue POPL: "Complexity and Information ..." Complexity and Information in Invariant Inference Yotam M. Y. Feldman, Neil Immerman, Mooly Sagiv, and Sharon Shoham (Tel Aviv University, Israel; University of Massachusetts, USA) Publisher's Version Article: popl20main-p25-p doi:10.1145/3371073
	Samak, Malavika	Proc. ACM Program. Lang., vol. 4, issue POPL: "Synthesizing Replacement Classes ..." Synthesizing Replacement Classes Malavika Samak, Deokhwan Kim, and Martin C. Rinard (Massachusetts Institute of Technology, USA) Publisher's Version Article: popl20main-p186-p doi:10.1145/3371120
	Samanta, Roopsha	Proc. ACM Program. Lang., vol. 4, issue POPL: "Augmented Example-Based Synthesis ..." Augmented Example-Based Synthesis using Relational Perturbation Properties Shengwei An, Rishabh Singh, Sasa Misailovic, and Roopsha Samanta (Purdue University, USA; Google, USA; University of Illinois at Urbana-Champaign, USA) Publisher's Version Article: popl20main-p204-p doi:10.1145/3371124
	Sammler, Michael	Proc. ACM Program. Lang., vol. 4, issue POPL: "The High-Level Benefits of ..." The High-Level Benefits of Low-Level Sandboxing Michael Sammler, Deepak Garg, Derek Dreyer, and Tadeusz Litak (MPI-SWS, Germany; Friedrich-Alexander University Erlangen-Nürnberg, Germany) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p114-p doi:10.1145/3371100
	Scholz, Bernhard	Proc. ACM Program. Lang., vol. 4, issue POPL: "Provenance-Guided Synthesis ..." Provenance-Guided Synthesis of Datalog Programs Mukund Raghothaman, Jonathan Mendelson, David Zhao, Mayur Naik, and Bernhard Scholz (University of Southern California, USA; University of Pennsylvania, USA; University of Sydney, Australia) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p236-p doi:10.1145/3371130
	Schrijvers, Tom	Proc. ACM Program. Lang., vol. 4, issue POPL: "PλωNK: Functional Probabilistic ..." PλωNK: Functional Probabilistic NetKAT Alexander Vandenbroucke and Tom Schrijvers (KU Leuven, Belgium) Publisher's Version Article: popl20main-p131-p doi:10.1145/3371107
	Shao, Zhong	Proc. ACM Program. Lang., vol. 4, issue POPL: "Virtual Timeline: A Formal ..." Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation Mengqi Liu, Lionel Rieg, Zhong Shao, Ronghui Gu, David Costanzo, Jung-Eun Kim, and Man-Ki Yoon (Yale University, USA; Grenoble Alps University, France; CNRS, France; Grenoble INP, France; VERIMAG, France; Columbia University, USA) Publisher's Version Artifacts Functional Article: popl20main-p73-p doi:10.1145/3371088
	Sherman, Benjamin	Proc. ACM Program. Lang., vol. 4, issue POPL: "Trace Types and Denotational ..." Trace Types and Denotational Semantics for Sound Programmable Inference in Probabilistic Languages Alexander K. Lew, Marco F. Cusumano-Towner, Benjamin Sherman, Michael Carbin, and Vikash K. Mansinghka (Massachusetts Institute of Technology, USA) Publisher's Version Article: popl20main-p69-p doi:10.1145/3371087
	Shoham, Sharon	Proc. ACM Program. Lang., vol. 4, issue POPL: "Complexity and Information ..." Complexity and Information in Invariant Inference Yotam M. Y. Feldman, Neil Immerman, Mooly Sagiv, and Sharon Shoham (Tel Aviv University, Israel; University of Massachusetts, USA) Publisher's Version Article: popl20main-p25-p doi:10.1145/3371073
	Sieczkowski, Filip	Proc. ACM Program. Lang., vol. 4, issue POPL: "Binders by Day, Labels by ..." Binders by Day, Labels by Night: Effect Instances via Lexically Scoped Handlers Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski (University of Wrocław, Poland) Publisher's Version Artifacts Functional Article: popl20main-p171-p doi:10.1145/3371116
	Silva, Alexandra	Proc. ACM Program. Lang., vol. 4, issue POPL: "Guarded Kleene Algebra with ..." Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time Steffen Smolka, Nate Foster, Justin Hsu, Tobias Kappé, Dexter Kozen, and Alexandra Silva (Cornell University, USA; University of Wisconsin-Madison, USA; University College London, UK) Publisher's Version Article: popl20main-p229-p doi:10.1145/3371129
	Singh, Rishabh	Proc. ACM Program. Lang., vol. 4, issue POPL: "Augmented Example-Based Synthesis ..." Augmented Example-Based Synthesis using Relational Perturbation Properties Shengwei An, Rishabh Singh, Sasa Misailovic, and Roopsha Samanta (Purdue University, USA; Google, USA; University of Illinois at Urbana-Champaign, USA) Publisher's Version Article: popl20main-p204-p doi:10.1145/3371124
	Skupin, Ingo	Proc. ACM Program. Lang., vol. 4, issue POPL: "Decomposition Diversity with ..." Decomposition Diversity with Symmetric Data and Codata David Binder, Julian Jabs, Ingo Skupin, and Klaus Ostermann (University of Tübingen, Germany) Publisher's Version Artifacts Functional Article: popl20main-p105-p doi:10.1145/3371098
	Smolka, Steffen	Proc. ACM Program. Lang., vol. 4, issue POPL: "Guarded Kleene Algebra with ..." Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time Steffen Smolka, Nate Foster, Justin Hsu, Tobias Kappé, Dexter Kozen, and Alexandra Silva (Cornell University, USA; University of Wisconsin-Madison, USA; University College London, UK) Publisher's Version Article: popl20main-p229-p doi:10.1145/3371129
	Song, Youngju	Proc. ACM Program. Lang., vol. 4, issue POPL: "CompCertM: CompCert with C-Assembly ..." CompCertM: CompCert with C-Assembly Linking and Lightweight Modular Verification Youngju Song, Minki Cho, Dongjoo Kim, Yonghyun Kim, Jeehoon Kang, and Chung-Kil Hur (Seoul National University, South Korea; KAIST, South Korea) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p93-p doi:10.1145/3371091
	Sozeau, Matthieu	Proc. ACM Program. Lang., vol. 4, issue POPL: "Coq Coq Correct! Verification ..." Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, and Théo Winterhalter (Inria, France; IRIF, France; CNRS, France; University of Paris Diderot, France; Saarland University, Germany) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p34-p doi:10.1145/3371076
	Su, Zhendong	Proc. ACM Program. Lang., vol. 4, issue POPL: "Detecting Floating-Point Errors ..." Detecting Floating-Point Errors via Atomic Conditions Daming Zou, Muhan Zeng, Yingfei Xiong, Zhoulai Fu, Lu Zhang, and Zhendong Su (Peking University, China; IT University of Copenhagen, Denmark; ETH Zurich, Switzerland) Publisher's Version Article: popl20main-p222-p doi:10.1145/3371128
	Sundar, Samanvitha	Proc. ACM Program. Lang., vol. 4, issue POPL: "Does Blame Shifting Work? ..." Does Blame Shifting Work? Lukas Lazarek, Alexis King, Samanvitha Sundar, Robert Bruce Findler, and Christos Dimoulas (Northwestern University, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl20main-p246-p doi:10.1145/3371133
	Sweet, Ian	Proc. ACM Program. Lang., vol. 4, issue POPL: "A Language for Probabilistically ..." A Language for Probabilistically Oblivious Computation David Darais, Ian Sweet, Chang Liu, and Michael Hicks (University of Vermont, USA; University of Maryland, USA; Citadel Securities, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl20main-p175-p doi:10.1145/3371118
	Tabareau, Nicolas	Proc. ACM Program. Lang., vol. 4, issue POPL: "The Fire Triangle: How to ..." The Fire Triangle: How to Mix Substitution, Dependent Elimination, and Effects Pierre-Marie Pédrot and Nicolas Tabareau (Inria, France) Publisher's Version Article: popl20main-p216-p doi:10.1145/3371126 Proc. ACM Program. Lang., vol. 4, issue POPL: "Coq Coq Correct! Verification ..." Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, and Théo Winterhalter (Inria, France; IRIF, France; CNRS, France; University of Paris Diderot, France; Saarland University, Germany) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p34-p doi:10.1145/3371076
	Thakur, Aditya V.	Proc. ACM Program. Lang., vol. 4, issue POPL: "Deterministic Parallel Fixpoint ..." Deterministic Parallel Fixpoint Computation Sung Kook Kim, Arnaud J. Venet, and Aditya V. Thakur (University of California at Davis, USA; Facebook, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p45-p doi:10.1145/3371082
	Thiemann, Peter	Proc. ACM Program. Lang., vol. 4, issue POPL: "Label-Dependent Session Types ..." Label-Dependent Session Types Peter Thiemann and Vasco T. Vasconcelos (University of Freiburg, Germany; University of Lisbon, Portugal) Publisher's Version Article: popl20main-p257-p doi:10.1145/3371135
	Timany, Amin	Proc. ACM Program. Lang., vol. 4, issue POPL: "The Future is Ours: Prophecy ..." The Future is Ours: Prophecy Variables in Separation Logic Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, and Bart Jacobs (MPI-SWS, Germany; ETH Zurich, Switzerland; University of Waterloo, Canada; KU Leuven, Belgium) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p157-p doi:10.1145/3371113
	Trieu, Alix	Proc. ACM Program. Lang., vol. 4, issue POPL: "Formal Verification of a Constant-Time ..." Formal Verification of a Constant-Time Preserving C Compiler Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, and Alix Trieu (MPI for Security and Privacy, Germany; IMDEA Software Institute, Spain; University of Rennes, France; Inria, France; CNRS, France; IRISA, France; Aarhus University, Denmark) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p31-p doi:10.1145/3371075
	Turner, Milo	Proc. ACM Program. Lang., vol. 4, issue POPL: "Dependent Type Systems as ..." Dependent Type Systems as Macros Stephen Chang, Michael Ballantyne, Milo Turner, and William J. Bowman (Northeastern University, USA; PLT Group, USA; University of British Columbia, Canada) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p18-p doi:10.1145/3371071
	Vafeiadis, Viktor	Proc. ACM Program. Lang., vol. 4, issue POPL: "Persistency Semantics of the ..." Persistency Semantics of the Intel-x86 Architecture Azalea Raad, John Wickerson, Gil Neiger, and Viktor Vafeiadis (MPI-SWS, Germany; Imperial College London, UK; Intel Labs, USA) Publisher's Version Article: popl20main-p39-p doi:10.1145/3371079
	Vandenbroucke, Alexander	Proc. ACM Program. Lang., vol. 4, issue POPL: "PλωNK: Functional Probabilistic ..." PλωNK: Functional Probabilistic NetKAT Alexander Vandenbroucke and Tom Schrijvers (KU Leuven, Belgium) Publisher's Version Article: popl20main-p131-p doi:10.1145/3371107
	Vandikas, Anthony	Proc. ACM Program. Lang., vol. 4, issue POPL: "Reductions for Safety Proofs ..." Reductions for Safety Proofs Azadeh Farzan and Anthony Vandikas (University of Toronto, Canada) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p42-p doi:10.1145/3371081
	Van Muylder, Antoine	Proc. ACM Program. Lang., vol. 4, issue POPL: "The Next 700 Relational Program ..." The Next 700 Relational Program Logics Kenji Maillard, Cătălin Hriţcu, Exequiel Rivas, and Antoine Van Muylder (Inria, France; ENS, France; University of Paris, France) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p24-p doi:10.1145/3371072
	Vasconcelos, Vasco T.	Proc. ACM Program. Lang., vol. 4, issue POPL: "Label-Dependent Session Types ..." Label-Dependent Session Types Peter Thiemann and Vasco T. Vasconcelos (University of Freiburg, Germany; University of Lisbon, Portugal) Publisher's Version Article: popl20main-p257-p doi:10.1145/3371135
	Vazou, Niki	Proc. ACM Program. Lang., vol. 4, issue POPL: "Liquidate Your Assets: Reasoning ..." Liquidate Your Assets: Reasoning about Resource Usage in Liquid Haskell Martin A. T. Handley, Niki Vazou, and Graham Hutton (University of Nottingham, UK; IMDEA Software Institute, Spain) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p94-p doi:10.1145/3371092
	Venet, Arnaud J.	Proc. ACM Program. Lang., vol. 4, issue POPL: "Deterministic Parallel Fixpoint ..." Deterministic Parallel Fixpoint Computation Sung Kook Kim, Arnaud J. Venet, and Aditya V. Thakur (University of California at Davis, USA; Facebook, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p45-p doi:10.1145/3371082
	Viswanathan, Mahesh	Proc. ACM Program. Lang., vol. 4, issue POPL: "Deciding Memory Safety for ..." Deciding Memory Safety for Single-Pass Heap-Manipulating Programs Umang Mathur, Adithya Murali, Paul Krogmeier, P. Madhusudan, and Mahesh Viswanathan (University of Illinois at Urbana-Champaign, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p125-p doi:10.1145/3371103
	Walker, David	Proc. ACM Program. Lang., vol. 4, issue POPL: "Abstract Interpretation of ..." Abstract Interpretation of Distributed Network Control Planes Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker (Microsoft Research, USA; Princeton University, USA; University of Washington, USA; Intentionet, USA) Publisher's Version Article: popl20main-p150-p doi:10.1145/3371110
	Wang, Chenglong	Proc. ACM Program. Lang., vol. 4, issue POPL: "Visualization by Example ..." Visualization by Example Chenglong Wang, Yu Feng, Rastislav Bodik, Alvin Cheung, and Isil Dillig (University of Washington, USA; University of California at Santa Barbara, USA; University of California at Berkeley, USA; University of Texas at Austin, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl20main-p174-p doi:10.1145/3371117
	Wang, Peixin	Proc. ACM Program. Lang., vol. 4, issue POPL: "Proving Expected Sensitivity ..." Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time Peixin Wang, Hongfei Fu, Krishnendu Chatterjee, Yuxin Deng, and Ming Xu (Shanghai Jiao Tong University, China; IST Austria, Austria; East China Normal University, China; Pengcheng Laboratory, China) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl20main-p96-p doi:10.1145/3371093
	Wang, Ziteng	Proc. ACM Program. Lang., vol. 4, issue POPL: "Program Synthesis by Type-Guided ..." Program Synthesis by Type-Guided Abstraction Refinement Zheng Guo, Michael James, David Justo, Jiaxiao Zhou, Ziteng Wang, Ranjit Jhala, and Nadia Polikarpova (University of California at San Diego, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p40-p doi:10.1145/3371080
	Westrick, Sam	Proc. ACM Program. Lang., vol. 4, issue POPL: "Disentanglement in Nested-Parallel ..." Disentanglement in Nested-Parallel Programs Sam Westrick, Rohan Yadav, Matthew Fluet, and Umut A. Acar (Carnegie Mellon University, USA; Rochester Institute of Technology, USA) Publisher's Version Article: popl20main-p169-p doi:10.1145/3371115
	Wickerson, John	Proc. ACM Program. Lang., vol. 4, issue POPL: "Persistency Semantics of the ..." Persistency Semantics of the Intel-x86 Architecture Azalea Raad, John Wickerson, Gil Neiger, and Viktor Vafeiadis (MPI-SWS, Germany; Imperial College London, UK; Intel Labs, USA) Publisher's Version Article: popl20main-p39-p doi:10.1145/3371079
	Winterhalter, Théo	Proc. ACM Program. Lang., vol. 4, issue POPL: "Coq Coq Correct! Verification ..." Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, and Théo Winterhalter (Inria, France; IRIF, France; CNRS, France; University of Paris Diderot, France; Saarland University, Germany) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p34-p doi:10.1145/3371076
	Wolff, Sebastian	Proc. ACM Program. Lang., vol. 4, issue POPL: "Pointer Life Cycle Types for ..." Pointer Life Cycle Types for Lock-Free Data Structures with Memory Reclamation Roland Meyer and Sebastian Wolff (TU Braunschweig, Germany) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p265-p doi:10.1145/3371136
	Xia, Li-yao	Proc. ACM Program. Lang., vol. 4, issue POPL: "Interaction Trees: Representing ..." Interaction Trees: Representing Recursive and Impure Programs in Coq Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic (University of Pennsylvania, USA; Seoul National University, South Korea; BedRock Systems, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p177-p doi:10.1145/3371119
	Xie, Ningning	Proc. ACM Program. Lang., vol. 4, issue POPL: "Kind Inference for Datatypes ..." Kind Inference for Datatypes Ningning Xie, Richard A. Eisenberg, and Bruno C. d. S. Oliveira (University of Hong Kong, China; Bryn Mawr College, USA; Tweag I/O, UK) Publisher's Version Article: popl20main-p189-p doi:10.1145/3371121
	Xiong, Yingfei	Proc. ACM Program. Lang., vol. 4, issue POPL: "Detecting Floating-Point Errors ..." Detecting Floating-Point Errors via Atomic Conditions Daming Zou, Muhan Zeng, Yingfei Xiong, Zhoulai Fu, Lu Zhang, and Zhendong Su (Peking University, China; IT University of Copenhagen, Denmark; ETH Zurich, Switzerland) Publisher's Version Article: popl20main-p222-p doi:10.1145/3371128
	Xu, Ming	Proc. ACM Program. Lang., vol. 4, issue POPL: "Proving Expected Sensitivity ..." Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time Peixin Wang, Hongfei Fu, Krishnendu Chatterjee, Yuxin Deng, and Ming Xu (Shanghai Jiao Tong University, China; IST Austria, Austria; East China Normal University, China; Pengcheng Laboratory, China) Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: popl20main-p96-p doi:10.1145/3371093
	Yadav, Rohan	Proc. ACM Program. Lang., vol. 4, issue POPL: "Disentanglement in Nested-Parallel ..." Disentanglement in Nested-Parallel Programs Sam Westrick, Rohan Yadav, Matthew Fluet, and Umut A. Acar (Carnegie Mellon University, USA; Rochester Institute of Technology, USA) Publisher's Version Article: popl20main-p169-p doi:10.1145/3371115
	Yang, Hongseok	Proc. ACM Program. Lang., vol. 4, issue POPL: "Towards Verified Stochastic ..." Towards Verified Stochastic Variational Inference for Probabilistic Programs Wonyeol Lee, Hangyeol Yu, Xavier Rival, and Hongseok Yang (KAIST, South Korea; Inria, France; ENS, France; CNRS, France; PSL University, France) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p48-p doi:10.1145/3371084
	Ying, Mingsheng	Proc. ACM Program. Lang., vol. 4, issue POPL: "Relational Proofs for Quantum ..." Relational Proofs for Quantum Programs Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, and Li Zhou (MPI for Security and Privacy, Germany; IMDEA Software Institute, Spain; University of Wisconsin-Madison, USA; University of Technology Sydney, Australia; Institute of Software at Chinese Academy of Sciences, China; Tsinghua University, China) Publisher's Version Article: popl20main-p78-p doi:10.1145/3371089
	Yoon, Man-Ki	Proc. ACM Program. Lang., vol. 4, issue POPL: "Virtual Timeline: A Formal ..." Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation Mengqi Liu, Lionel Rieg, Zhong Shao, Ronghui Gu, David Costanzo, Jung-Eun Kim, and Man-Ki Yoon (Yale University, USA; Grenoble Alps University, France; CNRS, France; Grenoble INP, France; VERIMAG, France; Columbia University, USA) Publisher's Version Artifacts Functional Article: popl20main-p73-p doi:10.1145/3371088
	Yu, Hangyeol	Proc. ACM Program. Lang., vol. 4, issue POPL: "Towards Verified Stochastic ..." Towards Verified Stochastic Variational Inference for Probabilistic Programs Wonyeol Lee, Hangyeol Yu, Xavier Rival, and Hongseok Yang (KAIST, South Korea; Inria, France; ENS, France; CNRS, France; PSL University, France) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p48-p doi:10.1145/3371084
	Yu, Nengkun	Proc. ACM Program. Lang., vol. 4, issue POPL: "Relational Proofs for Quantum ..." Relational Proofs for Quantum Programs Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, and Li Zhou (MPI for Security and Privacy, Germany; IMDEA Software Institute, Spain; University of Wisconsin-Madison, USA; University of Technology Sydney, Australia; Institute of Software at Chinese Academy of Sciences, China; Tsinghua University, China) Publisher's Version Article: popl20main-p78-p doi:10.1145/3371089
	Zakowski, Yannick	Proc. ACM Program. Lang., vol. 4, issue POPL: "Interaction Trees: Representing ..." Interaction Trees: Representing Recursive and Impure Programs in Coq Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic (University of Pennsylvania, USA; Seoul National University, South Korea; BedRock Systems, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p177-p doi:10.1145/3371119
	Zdancewic, Steve	Proc. ACM Program. Lang., vol. 4, issue POPL: "Interaction Trees: Representing ..." Interaction Trees: Representing Recursive and Impure Programs in Coq Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic (University of Pennsylvania, USA; Seoul National University, South Korea; BedRock Systems, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p177-p doi:10.1145/3371119
	Zeng, Muhan	Proc. ACM Program. Lang., vol. 4, issue POPL: "Detecting Floating-Point Errors ..." Detecting Floating-Point Errors via Atomic Conditions Daming Zou, Muhan Zeng, Yingfei Xiong, Zhoulai Fu, Lu Zhang, and Zhendong Su (Peking University, China; IT University of Copenhagen, Denmark; ETH Zurich, Switzerland) Publisher's Version Article: popl20main-p222-p doi:10.1145/3371128
	Zhang, Lu	Proc. ACM Program. Lang., vol. 4, issue POPL: "Detecting Floating-Point Errors ..." Detecting Floating-Point Errors via Atomic Conditions Daming Zou, Muhan Zeng, Yingfei Xiong, Zhoulai Fu, Lu Zhang, and Zhendong Su (Peking University, China; IT University of Copenhagen, Denmark; ETH Zurich, Switzerland) Publisher's Version Article: popl20main-p222-p doi:10.1145/3371128
	Zhao, David	Proc. ACM Program. Lang., vol. 4, issue POPL: "Provenance-Guided Synthesis ..." Provenance-Guided Synthesis of Datalog Programs Mukund Raghothaman, Jonathan Mendelson, David Zhao, Mayur Naik, and Bernhard Scholz (University of Southern California, USA; University of Pennsylvania, USA; University of Sydney, Australia) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p236-p doi:10.1145/3371130
	Zhou, Jiaxiao	Proc. ACM Program. Lang., vol. 4, issue POPL: "Program Synthesis by Type-Guided ..." Program Synthesis by Type-Guided Abstraction Refinement Zheng Guo, Michael James, David Justo, Jiaxiao Zhou, Ziteng Wang, Ranjit Jhala, and Nadia Polikarpova (University of California at San Diego, USA) Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: popl20main-p40-p doi:10.1145/3371080
	Zhou, Li	Proc. ACM Program. Lang., vol. 4, issue POPL: "Relational Proofs for Quantum ..." Relational Proofs for Quantum Programs Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, and Li Zhou (MPI for Security and Privacy, Germany; IMDEA Software Institute, Spain; University of Wisconsin-Madison, USA; University of Technology Sydney, Australia; Institute of Software at Chinese Academy of Sciences, China; Tsinghua University, China) Publisher's Version Article: popl20main-p78-p doi:10.1145/3371089
	Zou, Daming	Proc. ACM Program. Lang., vol. 4, issue POPL: "Detecting Floating-Point Errors ..." Detecting Floating-Point Errors via Atomic Conditions Daming Zou, Muhan Zeng, Yingfei Xiong, Zhoulai Fu, Lu Zhang, and Zhendong Su (Peking University, China; IT University of Copenhagen, Denmark; ETH Zurich, Switzerland) Publisher's Version Article: popl20main-p222-p doi:10.1145/3371128