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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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 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 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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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 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
	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
	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
	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
	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
	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
	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
	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
	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 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 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 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
	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 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
	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
	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
	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
	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
	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
	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 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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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 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 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
	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
	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 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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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 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
	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 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
	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
	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
	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
	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 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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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 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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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 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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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 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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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 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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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