POPL 2018 – Author Index

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

	Abel, Andreas	Proc. ACM Program. Lang., vol. 2, issue POPL: "Decidability of Conversion ..." Decidability of Conversion for Type Theory in Type Theory Andreas Abel, Joakim Öhman, and Andrea Vezzosi (University of Gothenburg, Sweden; IMDEA Software Institute, Spain; Chalmers University of Technology, Sweden) Artifacts Functional
	Abraham, Ittai	Proc. ACM Program. Lang., vol. 2, issue POPL: "Online Detection of Effectively ..." Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, and Yoni Zohar (Tel Aviv University, Israel; VMware, USA; Stanford University, USA) Artifacts Functional
	Agrawal, Sheshansh	Proc. ACM Program. Lang., vol. 2, issue POPL: "Lexicographic Ranking Supermartingales: ..." Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs Sheshansh Agrawal, Krishnendu Chatterjee, and Petr Novotný (IIT Bombay, India; IST Austria, Austria) Artifacts Functional
	Ahman, Danel	Proc. ACM Program. Lang., vol. 2, issue POPL: "Recalling a Witness: Foundations ..." Recalling a Witness: Foundations and Applications of Monotonic State Danel Ahman, Cédric Fournet, Cătălin Hriţcu, Kenji Maillard, Aseem Rastogi, and Nikhil Swamy (Inria, France; Microsoft Research, UK; ENS Paris, France; Microsoft Research, India; Microsoft Research, USA) Artifacts Functional Proc. ACM Program. Lang., vol. 2, issue POPL: "Handling Fibred Algebraic ..." Handling Fibred Algebraic Effects Danel Ahman (Inria, France)
	Ahmed, Amal	Proc. ACM Program. Lang., vol. 2, issue POPL: "Type-Preserving CPS Translation ..." Type-Preserving CPS Translation of Σ and Π Types Is Not Not Possible William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed (Northeastern University, USA; Ochanomizu University, Japan) Proc. ACM Program. Lang., vol. 2, issue POPL: "Correctness of Speculative ..." Correctness of Speculative Optimizations with Dynamic Deoptimization Olivier Flückiger, Gabriel Scherer, Ming-Ho Yee, Aviral Goel, Amal Ahmed, and Jan Vitek (Northeastern University, USA; Inria, France; Czech Technical University, Czechia)
	Aiken, Alex	Proc. ACM Program. Lang., vol. 2, issue POPL: "On Automatically Proving the ..." On Automatically Proving the Correctness of math.h Implementations Wonyeol Lee, Rahul Sharma, and Alex Aiken (Stanford University, USA; Microsoft Research, India)
	Albarghouthi, Aws	Proc. ACM Program. Lang., vol. 2, issue POPL: "Synthesizing Coupling Proofs ..." Synthesizing Coupling Proofs of Differential Privacy Aws Albarghouthi and Justin Hsu (University of Wisconsin-Madison, USA; University College London, UK)
	Amin, Nada	Proc. ACM Program. Lang., vol. 2, issue POPL: "Collapsing Towers of Interpreters ..." Collapsing Towers of Interpreters Nada Amin and Tiark Rompf (University of Cambridge, UK; Purdue University, USA) Artifacts Functional
	Bach Poulsen, Casper	Proc. ACM Program. Lang., vol. 2, issue POPL: "Intrinsically-Typed Definitional ..." Intrinsically-Typed Definitional Interpreters for Imperative Languages Casper Bach Poulsen, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers, and Eelco Visser (Delft University of Technology, Netherlands; Portland State University, USA) Artifacts Functional
	Bao, Wenlei	Proc. ACM Program. Lang., vol. 2, issue POPL: "Analytical Modeling of Cache ..." Analytical Modeling of Cache Behavior for Affine Programs Wenlei Bao, Sriram Krishnamoorthy, Louis-Noel Pouchet, and P. Sadayappan (Ohio State University, USA; Pacific Northwest National Laboratory, USA; Colorado State University, USA)
	Barthe, Gilles	Proc. ACM Program. Lang., vol. 2, issue POPL: "Monadic Refinements for Relational ..." Monadic Refinements for Relational Cost Analysis Ivan Radiček, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Florian Zuleger (Vienna University of Technology, Austria; IMDEA Software Institute, Spain; SUNY Buffalo, USA; MPI-SWS, Germany) Proc. ACM Program. Lang., vol. 2, issue POPL: "Proving Expected Sensitivity ..." Proving Expected Sensitivity of Probabilistic Programs Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub (IMDEA Software Institute, Spain; UPMC, France; Inria, France; University College London, UK; École Polytechnique, France) Artifacts Functional
	Bernardy, Jean-Philippe	Proc. ACM Program. Lang., vol. 2, issue POPL: "Linear Haskell: Practical ..." Linear Haskell: Practical Linearity in a Higher-Order Polymorphic Language Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, and Arnaud Spiwack (University of Gothenburg, Sweden; Tweag I/O, France; Indiana University, USA; Microsoft Research, UK) Artifacts Functional
	Biboudis, Aggelos	Proc. ACM Program. Lang., vol. 2, issue POPL: "Simplicitly: Foundations and ..." Simplicitly: Foundations and Applications of Implicit Function Types Martin Odersky, Olivier Blanvillain, Fengyun Liu, Aggelos Biboudis, Heather Miller, and Sandro Stucki (EPFL, Switzerland; Northeastern University, USA) Artifacts Functional
	Biernacki, Dariusz	Proc. ACM Program. Lang., vol. 2, issue POPL: "Handle with Care: Relational ..." Handle with Care: Relational Interpretation of Algebraic Effects and Handlers Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski (University of Wrocław, Poland) Artifacts Functional
	Birkedal, Lars	Proc. ACM Program. Lang., vol. 2, issue POPL: "A Logical Relation for Monadic ..." A Logical Relation for Monadic Encapsulation of State: Proving Contextual Equivalences in the Presence of runST Amin Timany, Léo Stefanesco, Morten Krogh-Jespersen, and Lars Birkedal (KU Leuven, Belgium; IRIF, France; CNRS, France; University of Paris Diderot, France; Aarhus University, Denmark) Artifacts Functional
	Blanvillain, Olivier	Proc. ACM Program. Lang., vol. 2, issue POPL: "Simplicitly: Foundations and ..." Simplicitly: Foundations and Applications of Implicit Function Types Martin Odersky, Olivier Blanvillain, Fengyun Liu, Aggelos Biboudis, Heather Miller, and Sandro Stucki (EPFL, Switzerland; Northeastern University, USA) Artifacts Functional
	Bodik, Rastislav	Proc. ACM Program. Lang., vol. 2, issue POPL: "Bonsai: Synthesis-Based Reasoning ..." Bonsai: Synthesis-Based Reasoning for Type Systems Kartik Chandra and Rastislav Bodik (Henry M. Gunn High School, USA; Stanford University, USA; University of Washington, USA) Artifacts Functional
	Boespflug, Mathieu	Proc. ACM Program. Lang., vol. 2, issue POPL: "Linear Haskell: Practical ..." Linear Haskell: Practical Linearity in a Higher-Order Polymorphic Language Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, and Arnaud Spiwack (University of Gothenburg, Sweden; Tweag I/O, France; Indiana University, USA; Microsoft Research, UK) Artifacts Functional
	Bowman, William J.	Proc. ACM Program. Lang., vol. 2, issue POPL: "Type-Preserving CPS Translation ..." Type-Preserving CPS Translation of Σ and Π Types Is Not Not Possible William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed (Northeastern University, USA; Ochanomizu University, Japan)
	Breck, Jason	Proc. ACM Program. Lang., vol. 2, issue POPL: "Non-linear Reasoning for Invariant ..." Non-linear Reasoning for Invariant Synthesis Zachary Kincaid, John Cyphert, Jason Breck, and Thomas Reps (Princeton University, USA; University of Wisconsin-Madison, USA; GrammaTech, USA) Artifacts Functional
	Brown, Matt	Proc. ACM Program. Lang., vol. 2, issue POPL: "Jones-Optimal Partial Evaluation ..." Jones-Optimal Partial Evaluation by Specialization-Safe Normalization Matt Brown and Jens Palsberg (University of California at Los Angeles, USA) Artifacts Functional
	Cai, Yufei	Proc. ACM Program. Lang., vol. 2, issue POPL: "Denotational Validation of ..." Denotational Validation of Higher-Order Bayesian Inference Adam Ścibior, Ohad Kammar, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Sean K. Moss, Chris Heunen, and Zoubin Ghahramani (University of Cambridge, UK; MPI Tübingen, Germany; University of Oxford, UK; KAIST, South Korea; University of Tübingen, Germany; University of Edinburgh, UK; Uber AI Labs, USA)
	Campora, John Peter	Proc. ACM Program. Lang., vol. 2, issue POPL: "Migrating Gradual Types ..." Migrating Gradual Types John Peter Campora, Sheng Chen, Martin Erwig, and Eric Walkingshaw (University of Louisiana at Lafayette, USA; Oregon State University, USA) Artifacts Functional
	Capriotti, Paolo	Proc. ACM Program. Lang., vol. 2, issue POPL: "Univalent Higher Categories ..." Univalent Higher Categories via Complete Semi-Segal Types Paolo Capriotti and Nicolai Kraus (University of Nottingham, UK) Artifacts Functional
	Cathcart Burn, Toby	Proc. ACM Program. Lang., vol. 2, issue POPL: "Higher-Order Constrained Horn ..." Higher-Order Constrained Horn Clauses for Verification Toby Cathcart Burn, C.-H. Luke Ong, and Steven J. Ramsay (University of Oxford, UK; University of Bristol, UK) Artifacts Functional
	Chalupa, Marek	Proc. ACM Program. Lang., vol. 2, issue POPL: "Data-Centric Dynamic Partial ..." Data-Centric Dynamic Partial Order Reduction Marek Chalupa, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya (Masaryk University, Czechia; IST Austria, Austria; Kena Labs, India; IIT Bombay, India)
	Chandra, Kartik	Proc. ACM Program. Lang., vol. 2, issue POPL: "Bonsai: Synthesis-Based Reasoning ..." Bonsai: Synthesis-Based Reasoning for Type Systems Kartik Chandra and Rastislav Bodik (Henry M. Gunn High School, USA; Stanford University, USA; University of Washington, USA) Artifacts Functional
	Chang, Stephen	Proc. ACM Program. Lang., vol. 2, issue POPL: "Symbolic Types for Lenient ..." Symbolic Types for Lenient Symbolic Execution Stephen Chang, Alex Knauth, and Emina Torlak (Northeastern University, USA; University of Washington, USA) Artifacts Functional
	Chatterjee, Krishnendu	Proc. ACM Program. Lang., vol. 2, issue POPL: "Optimal Dyck Reachability ..." Optimal Dyck Reachability for Data-Dependence and Alias Analysis Krishnendu Chatterjee, Bhavya Choudhary, and Andreas Pavlogiannis (IST Austria, Austria; IIT Bombay, India) Artifacts Functional Proc. ACM Program. Lang., vol. 2, issue POPL: "Data-Centric Dynamic Partial ..." Data-Centric Dynamic Partial Order Reduction Marek Chalupa, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya (Masaryk University, Czechia; IST Austria, Austria; Kena Labs, India; IIT Bombay, India) Proc. ACM Program. Lang., vol. 2, issue POPL: "Lexicographic Ranking Supermartingales: ..." Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs Sheshansh Agrawal, Krishnendu Chatterjee, and Petr Novotný (IIT Bombay, India; IST Austria, Austria) Artifacts Functional
	Chen, Sheng	Proc. ACM Program. Lang., vol. 2, issue POPL: "Migrating Gradual Types ..." Migrating Gradual Types John Peter Campora, Sheng Chen, Martin Erwig, and Eric Walkingshaw (University of Louisiana at Lafayette, USA; Oregon State University, USA) Artifacts Functional
	Chen, Taolue	Proc. ACM Program. Lang., vol. 2, issue POPL: "What Is Decidable about String ..." What Is Decidable about String Constraints with the ReplaceAll Function Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu (University of London, UK; Institute of Software at Chinese Academy of Sciences, China; University at Chinese Academy of Sciences, China; Royal Holloway University of London, UK; University of Oxford, UK)
	Chen, Yan	Proc. ACM Program. Lang., vol. 2, issue POPL: "What Is Decidable about String ..." What Is Decidable about String Constraints with the ReplaceAll Function Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu (University of London, UK; Institute of Software at Chinese Academy of Sciences, China; University at Chinese Academy of Sciences, China; Royal Holloway University of London, UK; University of Oxford, UK)
	Chin, Wei-Ngan	Proc. ACM Program. Lang., vol. 2, issue POPL: "Automated Lemma Synthesis ..." Automated Lemma Synthesis in Symbolic-Heap Separation Logic Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin (National University of Singapore, Singapore) Artifacts Functional
	Choudhary, Bhavya	Proc. ACM Program. Lang., vol. 2, issue POPL: "Optimal Dyck Reachability ..." Optimal Dyck Reachability for Data-Dependence and Alias Analysis Krishnendu Chatterjee, Bhavya Choudhary, and Andreas Pavlogiannis (IST Austria, Austria; IIT Bombay, India) Artifacts Functional
	Choudhury, Vikraman	Proc. ACM Program. Lang., vol. 2, issue POPL: "Refinement Reflection: Complete ..." Refinement Reflection: Complete Verification with SMT Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, and Ranjit Jhala (University of Maryland, USA; University of California at San Diego, USA; Indiana University, USA; University of Edinburgh, UK; Input Output HK, UK) Artifacts Functional
	Clairambault, Pierre	Proc. ACM Program. Lang., vol. 2, issue POPL: "Linearity in Higher-Order ..." Linearity in Higher-Order Recursion Schemes Pierre Clairambault, Charles Grellois, and Andrzej S. Murawski (University of Lyon, France; CNRS, France; ENS Lyon, France; Claude Bernard University Lyon 1, France; LIP, France; Inria, France; Aix-Marseille University, France; ENSAM, France; University of Toulon, France; University of Oxford, UK)
	Cong, Youyou	Proc. ACM Program. Lang., vol. 2, issue POPL: "Type-Preserving CPS Translation ..." Type-Preserving CPS Translation of Σ and Π Types Is Not Not Possible William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed (Northeastern University, USA; Ochanomizu University, Japan)
	Cook, William R.	Proc. ACM Program. Lang., vol. 2, issue POPL: "Verifying Equivalence of Database-Driven ..." Verifying Equivalence of Database-Driven Applications Yuepeng Wang, Isil Dillig, Shuvendu K. Lahiri, and William R. Cook (University of Texas at Austin, USA; Microsoft Research, USA)
	Cyphert, John	Proc. ACM Program. Lang., vol. 2, issue POPL: "Non-linear Reasoning for Invariant ..." Non-linear Reasoning for Invariant Synthesis Zachary Kincaid, John Cyphert, Jason Breck, and Thomas Reps (Princeton University, USA; University of Wisconsin-Madison, USA; GrammaTech, USA) Artifacts Functional
	Danielsson, Nils Anders	Proc. ACM Program. Lang., vol. 2, issue POPL: "Up-to Techniques using Sized ..." Up-to Techniques using Sized Types Nils Anders Danielsson (University of Gothenburg, Sweden; Chalmers University of Technology, Sweden) Artifacts Functional
	Deacon, Will	Proc. ACM Program. Lang., vol. 2, issue POPL: "Simplifying ARM Concurrency: ..." Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8 Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell (University of Cambridge, UK; ARM, UK; University of St. Andrews, UK) Artifacts Functional
	De Araújo, Marcus R.	Proc. ACM Program. Lang., vol. 2, issue POPL: "Inference of Static Semantics ..." Inference of Static Semantics for Incomplete C Programs Leandro T. C. Melo, Rodrigo G. Ribeiro, Marcus R. de Araújo, and Fernando Magno Quintão Pereira (Federal University of Minas Gerais, Brazil; Federal University of Ouro Preto, Brazil) Artifacts Functional
	Devriese, Dominique	Proc. ACM Program. Lang., vol. 2, issue POPL: "Parametricity versus the Universal ..." Parametricity versus the Universal Type Dominique Devriese, Marco Patrignani, and Frank Piessens (KU Leuven, Belgium; MPI-SWS, Germany; CISPA, Germany)
	Dillig, Isil	Proc. ACM Program. Lang., vol. 2, issue POPL: "Verifying Equivalence of Database-Driven ..." Verifying Equivalence of Database-Driven Applications Yuepeng Wang, Isil Dillig, Shuvendu K. Lahiri, and William R. Cook (University of Texas at Austin, USA; Microsoft Research, USA) Proc. ACM Program. Lang., vol. 2, issue POPL: "Program Synthesis using Abstraction ..." Program Synthesis using Abstraction Refinement Xinyu Wang, Isil Dillig, and Rishabh Singh (University of Texas at Austin, USA; Microsoft Research, USA)
	Dongol, Brijesh	Proc. ACM Program. Lang., vol. 2, issue POPL: "Transactions in Relaxed Memory ..." Transactions in Relaxed Memory Architectures Brijesh Dongol, Radha Jagadeesan, and James Riely (Brunel University London, UK; DePaul University, USA)
	Dreyer, Derek	Proc. ACM Program. Lang., vol. 2, issue POPL: "RustBelt: Securing the Foundations ..." RustBelt: Securing the Foundations of the Rust Programming Language Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer (MPI-SWS, Germany; Delft University of Technology, Netherlands) Artifacts Functional
	Ehrhard, Thomas	Proc. ACM Program. Lang., vol. 2, issue POPL: "Measurable Cones and Stable, ..." Measurable Cones and Stable, Measurable Functions: A Model for Probabilistic Higher-Order Programming Thomas Ehrhard, Michele Pagani, and Christine Tasson (University of Paris Diderot, France; CNRS, France)
	Emmi, Michael	Proc. ACM Program. Lang., vol. 2, issue POPL: "Sound, Complete, and Tractable ..." Sound, Complete, and Tractable Linearizability Monitoring for Concurrent Collections Michael Emmi and Constantin Enea (SRI International, USA; University of Paris Diderot, France; CNRS, France)
	Enea, Constantin	Proc. ACM Program. Lang., vol. 2, issue POPL: "Sound, Complete, and Tractable ..." Sound, Complete, and Tractable Linearizability Monitoring for Concurrent Collections Michael Emmi and Constantin Enea (SRI International, USA; University of Paris Diderot, France; CNRS, France)
	Erwig, Martin	Proc. ACM Program. Lang., vol. 2, issue POPL: "Migrating Gradual Types ..." Migrating Gradual Types John Peter Campora, Sheng Chen, Martin Erwig, and Eric Walkingshaw (University of Louisiana at Lafayette, USA; Oregon State University, USA) Artifacts Functional
	Espitau, Thomas	Proc. ACM Program. Lang., vol. 2, issue POPL: "Proving Expected Sensitivity ..." Proving Expected Sensitivity of Probabilistic Programs Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub (IMDEA Software Institute, Spain; UPMC, France; Inria, France; University College London, UK; École Polytechnique, France) Artifacts Functional
	Farzan, Azadeh	Proc. ACM Program. Lang., vol. 2, issue POPL: "Strategy Synthesis for Linear ..." Strategy Synthesis for Linear Arithmetic Games Azadeh Farzan and Zachary Kincaid (University of Toronto, Canada; Princeton University, USA) Artifacts Functional
	Feng, Xinyu	Proc. ACM Program. Lang., vol. 2, issue POPL: "Progress of Concurrent Objects ..." Progress of Concurrent Objects with Partial Methods Hongjin Liang and Xinyu Feng (Nanjing University, China; University of Science and Technology of China, China)
	Fisher, Kathleen	Proc. ACM Program. Lang., vol. 2, issue POPL: "Synthesizing Bijective Lenses ..." Synthesizing Bijective Lenses Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve Zdancewic (Princeton University, USA; Tufts University, USA; University of Pennsylvania, USA) Artifacts Functional
	Flückiger, Olivier	Proc. ACM Program. Lang., vol. 2, issue POPL: "Correctness of Speculative ..." Correctness of Speculative Optimizations with Dynamic Deoptimization Olivier Flückiger, Gabriel Scherer, Ming-Ho Yee, Aviral Goel, Amal Ahmed, and Jan Vitek (Northeastern University, USA; Inria, France; Czech Technical University, Czechia)
	Flur, Shaked	Proc. ACM Program. Lang., vol. 2, issue POPL: "Simplifying ARM Concurrency: ..." Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8 Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell (University of Cambridge, UK; ARM, UK; University of St. Andrews, UK) Artifacts Functional
	Fournet, Cédric	Proc. ACM Program. Lang., vol. 2, issue POPL: "Recalling a Witness: Foundations ..." Recalling a Witness: Foundations and Applications of Monotonic State Danel Ahman, Cédric Fournet, Cătălin Hriţcu, Kenji Maillard, Aseem Rastogi, and Nikhil Swamy (Inria, France; Microsoft Research, UK; ENS Paris, France; Microsoft Research, India; Microsoft Research, USA) Artifacts Functional
	Fragoso Santos, José	Proc. ACM Program. Lang., vol. 2, issue POPL: "JaVerT: JavaScript Verification ..." JaVerT: JavaScript Verification Toolchain José Fragoso Santos, Petar Maksimović, Daiva Naudžiūnienė, Thomas Wood, and Philippa Gardner (Imperial College London, UK; Mathematical Institute SASA, Serbia) Artifacts Functional
	French, Jon	Proc. ACM Program. Lang., vol. 2, issue POPL: "Simplifying ARM Concurrency: ..." Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8 Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell (University of Cambridge, UK; ARM, UK; University of St. Andrews, UK) Artifacts Functional
	Gaboardi, Marco	Proc. ACM Program. Lang., vol. 2, issue POPL: "Monadic Refinements for Relational ..." Monadic Refinements for Relational Cost Analysis Ivan Radiček, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Florian Zuleger (Vienna University of Technology, Austria; IMDEA Software Institute, Spain; SUNY Buffalo, USA; MPI-SWS, Germany)
	Gardner, Philippa	Proc. ACM Program. Lang., vol. 2, issue POPL: "JaVerT: JavaScript Verification ..." JaVerT: JavaScript Verification Toolchain José Fragoso Santos, Petar Maksimović, Daiva Naudžiūnienė, Thomas Wood, and Philippa Gardner (Imperial College London, UK; Mathematical Institute SASA, Serbia) Artifacts Functional
	Garg, Deepak	Proc. ACM Program. Lang., vol. 2, issue POPL: "Monadic Refinements for Relational ..." Monadic Refinements for Relational Cost Analysis Ivan Radiček, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Florian Zuleger (Vienna University of Technology, Austria; IMDEA Software Institute, Spain; SUNY Buffalo, USA; MPI-SWS, Germany)
	Ghahramani, Zoubin	Proc. ACM Program. Lang., vol. 2, issue POPL: "Denotational Validation of ..." Denotational Validation of Higher-Order Bayesian Inference Adam Ścibior, Ohad Kammar, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Sean K. Moss, Chris Heunen, and Zoubin Ghahramani (University of Cambridge, UK; MPI Tübingen, Germany; University of Oxford, UK; KAIST, South Korea; University of Tübingen, Germany; University of Edinburgh, UK; Uber AI Labs, USA)
	Gilray, Thomas	Proc. ACM Program. Lang., vol. 2, issue POPL: "Soft Contract Verification ..." Soft Contract Verification for Higher-Order Stateful Programs Phúc C. Nguyễn, Thomas Gilray, Sam Tobin-Hochstadt, and David Van Horn (University of Maryland, USA; Indiana University, USA) Artifacts Functional
	Goel, Aviral	Proc. ACM Program. Lang., vol. 2, issue POPL: "Correctness of Speculative ..." Correctness of Speculative Optimizations with Dynamic Deoptimization Olivier Flückiger, Gabriel Scherer, Ming-Ho Yee, Aviral Goel, Amal Ahmed, and Jan Vitek (Northeastern University, USA; Inria, France; Czech Technical University, Czechia)
	Golan-Gueta, Guy	Proc. ACM Program. Lang., vol. 2, issue POPL: "Online Detection of Effectively ..." Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, and Yoni Zohar (Tel Aviv University, Israel; VMware, USA; Stanford University, USA) Artifacts Functional
	Grégoire, Benjamin	Proc. ACM Program. Lang., vol. 2, issue POPL: "Proving Expected Sensitivity ..." Proving Expected Sensitivity of Probabilistic Programs Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub (IMDEA Software Institute, Spain; UPMC, France; Inria, France; University College London, UK; École Polytechnique, France) Artifacts Functional
	Grellois, Charles	Proc. ACM Program. Lang., vol. 2, issue POPL: "Linearity in Higher-Order ..." Linearity in Higher-Order Recursion Schemes Pierre Clairambault, Charles Grellois, and Andrzej S. Murawski (University of Lyon, France; CNRS, France; ENS Lyon, France; Claude Bernard University Lyon 1, France; LIP, France; Inria, France; Aix-Marseille University, France; ENSAM, France; University of Toulon, France; University of Oxford, UK)
	Grossman, Shelly	Proc. ACM Program. Lang., vol. 2, issue POPL: "Online Detection of Effectively ..." Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, and Yoni Zohar (Tel Aviv University, Israel; VMware, USA; Stanford University, USA) Artifacts Functional
	Hague, Matthew	Proc. ACM Program. Lang., vol. 2, issue POPL: "What Is Decidable about String ..." What Is Decidable about String Constraints with the ReplaceAll Function Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu (University of London, UK; Institute of Software at Chinese Academy of Sciences, China; University at Chinese Academy of Sciences, China; Royal Holloway University of London, UK; University of Oxford, UK)
	Heunen, Chris	Proc. ACM Program. Lang., vol. 2, issue POPL: "Denotational Validation of ..." Denotational Validation of Higher-Order Bayesian Inference Adam Ścibior, Ohad Kammar, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Sean K. Moss, Chris Heunen, and Zoubin Ghahramani (University of Cambridge, UK; MPI Tübingen, Germany; University of Oxford, UK; KAIST, South Korea; University of Tübingen, Germany; University of Edinburgh, UK; Uber AI Labs, USA)
	Hoenicke, Jochen	Proc. ACM Program. Lang., vol. 2, issue POPL: "Reducing Liveness to Safety ..." Reducing Liveness to Safety in First-Order Logic Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, and Sharon Shoham (Tel Aviv University, Israel; University of Freiburg, Germany; University of California at Los Angeles, USA) Artifacts Functional
	Holík, Lukáš	Proc. ACM Program. Lang., vol. 2, issue POPL: "String Constraints with Concatenation ..." String Constraints with Concatenation and Transducers Solved Efficiently Lukáš Holík, Petr Janků, Anthony W. Lin, Philipp Rümmer, and Tomáš Vojnar (Brno University of Technology, Czechia; University of Oxford, UK; Uppsala University, Sweden) Artifacts Functional
	Hriţcu, Cătălin	Proc. ACM Program. Lang., vol. 2, issue POPL: "Recalling a Witness: Foundations ..." Recalling a Witness: Foundations and Applications of Monotonic State Danel Ahman, Cédric Fournet, Cătălin Hriţcu, Kenji Maillard, Aseem Rastogi, and Nikhil Swamy (Inria, France; Microsoft Research, UK; ENS Paris, France; Microsoft Research, India; Microsoft Research, USA) Artifacts Functional
	Hsu, Justin	Proc. ACM Program. Lang., vol. 2, issue POPL: "Proving Expected Sensitivity ..." Proving Expected Sensitivity of Probabilistic Programs Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub (IMDEA Software Institute, Spain; UPMC, France; Inria, France; University College London, UK; École Polytechnique, France) Artifacts Functional Proc. ACM Program. Lang., vol. 2, issue POPL: "Synthesizing Coupling Proofs ..." Synthesizing Coupling Proofs of Differential Privacy Aws Albarghouthi and Justin Hsu (University of Wisconsin-Madison, USA; University College London, UK)
	Hu, Zhenjiang	Proc. ACM Program. Lang., vol. 2, issue POPL: "An Axiomatic Basis for Bidirectional ..." An Axiomatic Basis for Bidirectional Programming Hsiang-Shang Ko and Zhenjiang Hu (National Institute of Informatics, Japan) Artifacts Functional
	Inala, Jeevana Priya	Proc. ACM Program. Lang., vol. 2, issue POPL: "WebRelate: Integrating Web ..." WebRelate: Integrating Web Data with Spreadsheets using Examples Jeevana Priya Inala and Rishabh Singh (Massachusetts Institute of Technology, USA; Microsoft Research, USA) Artifacts Functional
	Jagadeesan, Radha	Proc. ACM Program. Lang., vol. 2, issue POPL: "Transactions in Relaxed Memory ..." Transactions in Relaxed Memory Architectures Brijesh Dongol, Radha Jagadeesan, and James Riely (Brunel University London, UK; DePaul University, USA)
	Jagannathan, Suresh	Proc. ACM Program. Lang., vol. 2, issue POPL: "Alone Together: Compositional ..." Alone Together: Compositional Reasoning and Inference for Weak Isolation Gowtham Kaki, Kartik Nagar, Mahsa Najafzadeh, and Suresh Jagannathan (Purdue University, USA)
	Janků, Petr	Proc. ACM Program. Lang., vol. 2, issue POPL: "String Constraints with Concatenation ..." String Constraints with Concatenation and Transducers Solved Efficiently Lukáš Holík, Petr Janků, Anthony W. Lin, Philipp Rümmer, and Tomáš Vojnar (Brno University of Technology, Czechia; University of Oxford, UK; Uppsala University, Sweden) Artifacts Functional
	Jhala, Ranjit	Proc. ACM Program. Lang., vol. 2, issue POPL: "Refinement Reflection: Complete ..." Refinement Reflection: Complete Verification with SMT Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, and Ranjit Jhala (University of Maryland, USA; University of California at San Diego, USA; Indiana University, USA; University of Edinburgh, UK; Input Output HK, UK) Artifacts Functional
	Jourdan, Jacques-Henri	Proc. ACM Program. Lang., vol. 2, issue POPL: "RustBelt: Securing the Foundations ..." RustBelt: Securing the Foundations of the Rust Programming Language Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer (MPI-SWS, Germany; Delft University of Technology, Netherlands) Artifacts Functional
	Jung, Ralf	Proc. ACM Program. Lang., vol. 2, issue POPL: "RustBelt: Securing the Foundations ..." RustBelt: Securing the Foundations of the Rust Programming Language Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer (MPI-SWS, Germany; Delft University of Technology, Netherlands) Artifacts Functional
	Kaki, Gowtham	Proc. ACM Program. Lang., vol. 2, issue POPL: "Alone Together: Compositional ..." Alone Together: Compositional Reasoning and Inference for Weak Isolation Gowtham Kaki, Kartik Nagar, Mahsa Najafzadeh, and Suresh Jagannathan (Purdue University, USA)
	Kaminski, Benjamin Lucien	Proc. ACM Program. Lang., vol. 2, issue POPL: "A New Proof Rule for Almost-Sure ..." A New Proof Rule for Almost-Sure Termination Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, and Joost-Pieter Katoen (Macquarie University, Australia; UNSW, Australia; Data61 at CSIRO, Australia; RWTH Aachen University, Germany; University College London, UK; IST Austria, Austria)
	Kammar, Ohad	Proc. ACM Program. Lang., vol. 2, issue POPL: "Denotational Validation of ..." Denotational Validation of Higher-Order Bayesian Inference Adam Ścibior, Ohad Kammar, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Sean K. Moss, Chris Heunen, and Zoubin Ghahramani (University of Cambridge, UK; MPI Tübingen, Germany; University of Oxford, UK; KAIST, South Korea; University of Tübingen, Germany; University of Edinburgh, UK; Uber AI Labs, USA)
	Katoen, Joost-Pieter	Proc. ACM Program. Lang., vol. 2, issue POPL: "A New Proof Rule for Almost-Sure ..." A New Proof Rule for Almost-Sure Termination Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, and Joost-Pieter Katoen (Macquarie University, Australia; UNSW, Australia; Data61 at CSIRO, Australia; RWTH Aachen University, Germany; University College London, UK; IST Austria, Austria)
	Khoo, Siau-Cheng	Proc. ACM Program. Lang., vol. 2, issue POPL: "Automated Lemma Synthesis ..." Automated Lemma Synthesis in Symbolic-Heap Separation Logic Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin (National University of Singapore, Singapore) Artifacts Functional
	Kincaid, Zachary	Proc. ACM Program. Lang., vol. 2, issue POPL: "Non-linear Reasoning for Invariant ..." Non-linear Reasoning for Invariant Synthesis Zachary Kincaid, John Cyphert, Jason Breck, and Thomas Reps (Princeton University, USA; University of Wisconsin-Madison, USA; GrammaTech, USA) Artifacts Functional Proc. ACM Program. Lang., vol. 2, issue POPL: "Strategy Synthesis for Linear ..." Strategy Synthesis for Linear Arithmetic Games Azadeh Farzan and Zachary Kincaid (University of Toronto, Canada; Princeton University, USA) Artifacts Functional
	Knauth, Alex	Proc. ACM Program. Lang., vol. 2, issue POPL: "Symbolic Types for Lenient ..." Symbolic Types for Lenient Symbolic Execution Stephen Chang, Alex Knauth, and Emina Torlak (Northeastern University, USA; University of Washington, USA) Artifacts Functional
	Ko, Hsiang-Shang	Proc. ACM Program. Lang., vol. 2, issue POPL: "An Axiomatic Basis for Bidirectional ..." An Axiomatic Basis for Bidirectional Programming Hsiang-Shang Ko and Zhenjiang Hu (National Institute of Informatics, Japan) Artifacts Functional
	Koch, Christoph E.	Proc. ACM Program. Lang., vol. 2, issue POPL: "Unifying Analytic and Statically-Typed ..." Unifying Analytic and Statically-Typed Quasiquotes Lionel Parreaux, Antoine Voizard, Amir Shaikhha, and Christoph E. Koch (EPFL, Switzerland; University of Pennsylvania, USA) Artifacts Functional
	Kokologiannakis, Michalis	Proc. ACM Program. Lang., vol. 2, issue POPL: "Effective Stateless Model ..." Effective Stateless Model Checking for C/C++ Concurrency Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, and Viktor Vafeiadis (National Technical University of Athens, Greece; Tel Aviv University, Israel; Uppsala University, Sweden; MPI-SWS, Germany) Artifacts Functional
	Kraus, Nicolai	Proc. ACM Program. Lang., vol. 2, issue POPL: "Univalent Higher Categories ..." Univalent Higher Categories via Complete Semi-Segal Types Paolo Capriotti and Nicolai Kraus (University of Nottingham, UK) Artifacts Functional
	Krebbers, Robbert	Proc. ACM Program. Lang., vol. 2, issue POPL: "Intrinsically-Typed Definitional ..." Intrinsically-Typed Definitional Interpreters for Imperative Languages Casper Bach Poulsen, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers, and Eelco Visser (Delft University of Technology, Netherlands; Portland State University, USA) Artifacts Functional Proc. ACM Program. Lang., vol. 2, issue POPL: "RustBelt: Securing the Foundations ..." RustBelt: Securing the Foundations of the Rust Programming Language Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer (MPI-SWS, Germany; Delft University of Technology, Netherlands) Artifacts Functional
	Krishna, Siddharth	Proc. ACM Program. Lang., vol. 2, issue POPL: "Go with the Flow: Compositional ..." Go with the Flow: Compositional Abstractions for Concurrent Data Structures Siddharth Krishna, Dennis Shasha, and Thomas Wies (New York University, USA)
	Krishnamoorthy, Sriram	Proc. ACM Program. Lang., vol. 2, issue POPL: "Analytical Modeling of Cache ..." Analytical Modeling of Cache Behavior for Affine Programs Wenlei Bao, Sriram Krishnamoorthy, Louis-Noel Pouchet, and P. Sadayappan (Ohio State University, USA; Pacific Northwest National Laboratory, USA; Colorado State University, USA)
	Krogh-Jespersen, Morten	Proc. ACM Program. Lang., vol. 2, issue POPL: "A Logical Relation for Monadic ..." A Logical Relation for Monadic Encapsulation of State: Proving Contextual Equivalences in the Presence of runST Amin Timany, Léo Stefanesco, Morten Krogh-Jespersen, and Lars Birkedal (KU Leuven, Belgium; IRIF, France; CNRS, France; University of Paris Diderot, France; Aarhus University, Denmark) Artifacts Functional
	Kunčar, Ondřej	Proc. ACM Program. Lang., vol. 2, issue POPL: "Safety and Conservativity ..." Safety and Conservativity of Definitions in HOL and Isabelle/HOL Ondřej Kunčar and Andrei Popescu (TU Munich, Germany; Middlesex University, UK; Institute of Mathematics at Romanian Academy, Romania)
	Lahav, Ori	Proc. ACM Program. Lang., vol. 2, issue POPL: "Effective Stateless Model ..." Effective Stateless Model Checking for C/C++ Concurrency Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, and Viktor Vafeiadis (National Technical University of Athens, Greece; Tel Aviv University, Israel; Uppsala University, Sweden; MPI-SWS, Germany) Artifacts Functional
	Lahiri, Shuvendu K.	Proc. ACM Program. Lang., vol. 2, issue POPL: "Verifying Equivalence of Database-Driven ..." Verifying Equivalence of Database-Driven Applications Yuepeng Wang, Isil Dillig, Shuvendu K. Lahiri, and William R. Cook (University of Texas at Austin, USA; Microsoft Research, USA)
	Lampropoulos, Leonidas	Proc. ACM Program. Lang., vol. 2, issue POPL: "Generating Good Generators ..." Generating Good Generators for Inductive Relations Leonidas Lampropoulos, Zoe Paraskevopoulou, and Benjamin C. Pierce (University of Pennsylvania, USA; Princeton University, USA) Artifacts Functional
	Le, Ton Chanh	Proc. ACM Program. Lang., vol. 2, issue POPL: "Automated Lemma Synthesis ..." Automated Lemma Synthesis in Symbolic-Heap Separation Logic Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin (National University of Singapore, Singapore) Artifacts Functional
	Lee, Wonyeol	Proc. ACM Program. Lang., vol. 2, issue POPL: "On Automatically Proving the ..." On Automatically Proving the Correctness of math.h Implementations Wonyeol Lee, Rahul Sharma, and Alex Aiken (Stanford University, USA; Microsoft Research, India)
	Li, Yangjia	Proc. ACM Program. Lang., vol. 2, issue POPL: "Algorithmic Analysis of Termination ..." Algorithmic Analysis of Termination Problems for Quantum Programs Yangjia Li and Mingsheng Ying (Institute of Software at Chinese Academy of Sciences, China; University of Technology Sydney, Australia; Tsinghua University, China)
	Liang, Hongjin	Proc. ACM Program. Lang., vol. 2, issue POPL: "Progress of Concurrent Objects ..." Progress of Concurrent Objects with Partial Methods Hongjin Liang and Xinyu Feng (Nanjing University, China; University of Science and Technology of China, China)
	Lin, Anthony W.	Proc. ACM Program. Lang., vol. 2, issue POPL: "What Is Decidable about String ..." What Is Decidable about String Constraints with the ReplaceAll Function Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu (University of London, UK; Institute of Software at Chinese Academy of Sciences, China; University at Chinese Academy of Sciences, China; Royal Holloway University of London, UK; University of Oxford, UK) Proc. ACM Program. Lang., vol. 2, issue POPL: "String Constraints with Concatenation ..." String Constraints with Concatenation and Transducers Solved Efficiently Lukáš Holík, Petr Janků, Anthony W. Lin, Philipp Rümmer, and Tomáš Vojnar (Brno University of Technology, Czechia; University of Oxford, UK; Uppsala University, Sweden) Artifacts Functional
	Liu, Fengyun	Proc. ACM Program. Lang., vol. 2, issue POPL: "Simplicitly: Foundations and ..." Simplicitly: Foundations and Applications of Implicit Function Types Martin Odersky, Olivier Blanvillain, Fengyun Liu, Aggelos Biboudis, Heather Miller, and Sandro Stucki (EPFL, Switzerland; Northeastern University, USA) Artifacts Functional
	Löding, Christof	Proc. ACM Program. Lang., vol. 2, issue POPL: "Foundations for Natural Proofs ..." Foundations for Natural Proofs and Quantifier Instantiation Christof Löding, P. Madhusudan, and Lucas Peña (RWTH Aachen University, Germany; University of Illinois at Urbana-Champaign, USA) Artifacts Functional
	Losa, Giuliano	Proc. ACM Program. Lang., vol. 2, issue POPL: "Reducing Liveness to Safety ..." Reducing Liveness to Safety in First-Order Logic Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, and Sharon Shoham (Tel Aviv University, Israel; University of Freiburg, Germany; University of California at Los Angeles, USA) Artifacts Functional
	Madhusudan, P.	Proc. ACM Program. Lang., vol. 2, issue POPL: "Foundations for Natural Proofs ..." Foundations for Natural Proofs and Quantifier Instantiation Christof Löding, P. Madhusudan, and Lucas Peña (RWTH Aachen University, Germany; University of Illinois at Urbana-Champaign, USA) Artifacts Functional
	Maillard, Kenji	Proc. ACM Program. Lang., vol. 2, issue POPL: "Recalling a Witness: Foundations ..." Recalling a Witness: Foundations and Applications of Monotonic State Danel Ahman, Cédric Fournet, Cătălin Hriţcu, Kenji Maillard, Aseem Rastogi, and Nikhil Swamy (Inria, France; Microsoft Research, UK; ENS Paris, France; Microsoft Research, India; Microsoft Research, USA) Artifacts Functional
	Majumdar, Rupak	Proc. ACM Program. Lang., vol. 2, issue POPL: "Why Is Random Testing Effective ..." Why Is Random Testing Effective for Partition Tolerance Bugs? Rupak Majumdar and Filip Niksic (MPI-SWS, Germany)
	Maksimović, Petar	Proc. ACM Program. Lang., vol. 2, issue POPL: "JaVerT: JavaScript Verification ..." JaVerT: JavaScript Verification Toolchain José Fragoso Santos, Petar Maksimović, Daiva Naudžiūnienė, Thomas Wood, and Philippa Gardner (Imperial College London, UK; Mathematical Institute SASA, Serbia) Artifacts Functional
	Mazza, Damiano	Proc. ACM Program. Lang., vol. 2, issue POPL: "Polyadic Approximations, Fibrations ..." Polyadic Approximations, Fibrations and Intersection Types Damiano Mazza, Luc Pellissier, and Pierre Vial (CNRS, France; University of Paris 13, France; University of Paris Diderot, France)
	McIver, Annabelle	Proc. ACM Program. Lang., vol. 2, issue POPL: "A New Proof Rule for Almost-Sure ..." A New Proof Rule for Almost-Sure Termination Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, and Joost-Pieter Katoen (Macquarie University, Australia; UNSW, Australia; Data61 at CSIRO, Australia; RWTH Aachen University, Germany; University College London, UK; IST Austria, Austria)
	Melo, Leandro T. C.	Proc. ACM Program. Lang., vol. 2, issue POPL: "Inference of Static Semantics ..." Inference of Static Semantics for Incomplete C Programs Leandro T. C. Melo, Rodrigo G. Ribeiro, Marcus R. de Araújo, and Fernando Magno Quintão Pereira (Federal University of Minas Gerais, Brazil; Federal University of Ouro Preto, Brazil) Artifacts Functional
	Michalevsky, Yan	Proc. ACM Program. Lang., vol. 2, issue POPL: "Online Detection of Effectively ..." Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, and Yoni Zohar (Tel Aviv University, Israel; VMware, USA; Stanford University, USA) Artifacts Functional
	Miller, Heather	Proc. ACM Program. Lang., vol. 2, issue POPL: "Simplicitly: Foundations and ..." Simplicitly: Foundations and Applications of Implicit Function Types Martin Odersky, Olivier Blanvillain, Fengyun Liu, Aggelos Biboudis, Heather Miller, and Sandro Stucki (EPFL, Switzerland; Northeastern University, USA) Artifacts Functional
	Miltner, Anders	Proc. ACM Program. Lang., vol. 2, issue POPL: "Synthesizing Bijective Lenses ..." Synthesizing Bijective Lenses Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve Zdancewic (Princeton University, USA; Tufts University, USA; University of Pennsylvania, USA) Artifacts Functional
	Morgan, Carroll	Proc. ACM Program. Lang., vol. 2, issue POPL: "A New Proof Rule for Almost-Sure ..." A New Proof Rule for Almost-Sure Termination Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, and Joost-Pieter Katoen (Macquarie University, Australia; UNSW, Australia; Data61 at CSIRO, Australia; RWTH Aachen University, Germany; University College London, UK; IST Austria, Austria)
	Moss, Sean K.	Proc. ACM Program. Lang., vol. 2, issue POPL: "Denotational Validation of ..." Denotational Validation of Higher-Order Bayesian Inference Adam Ścibior, Ohad Kammar, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Sean K. Moss, Chris Heunen, and Zoubin Ghahramani (University of Cambridge, UK; MPI Tübingen, Germany; University of Oxford, UK; KAIST, South Korea; University of Tübingen, Germany; University of Edinburgh, UK; Uber AI Labs, USA)
	Murawski, Andrzej S.	Proc. ACM Program. Lang., vol. 2, issue POPL: "Linearity in Higher-Order ..." Linearity in Higher-Order Recursion Schemes Pierre Clairambault, Charles Grellois, and Andrzej S. Murawski (University of Lyon, France; CNRS, France; ENS Lyon, France; Claude Bernard University Lyon 1, France; LIP, France; Inria, France; Aix-Marseille University, France; ENSAM, France; University of Toulon, France; University of Oxford, UK)
	Nagar, Kartik	Proc. ACM Program. Lang., vol. 2, issue POPL: "Alone Together: Compositional ..." Alone Together: Compositional Reasoning and Inference for Weak Isolation Gowtham Kaki, Kartik Nagar, Mahsa Najafzadeh, and Suresh Jagannathan (Purdue University, USA)
	Najafzadeh, Mahsa	Proc. ACM Program. Lang., vol. 2, issue POPL: "Alone Together: Compositional ..." Alone Together: Compositional Reasoning and Inference for Weak Isolation Gowtham Kaki, Kartik Nagar, Mahsa Najafzadeh, and Suresh Jagannathan (Purdue University, USA)
	Naudžiūnienė, Daiva	Proc. ACM Program. Lang., vol. 2, issue POPL: "JaVerT: JavaScript Verification ..." JaVerT: JavaScript Verification Toolchain José Fragoso Santos, Petar Maksimović, Daiva Naudžiūnienė, Thomas Wood, and Philippa Gardner (Imperial College London, UK; Mathematical Institute SASA, Serbia) Artifacts Functional
	Newton, Ryan R.	Proc. ACM Program. Lang., vol. 2, issue POPL: "Refinement Reflection: Complete ..." Refinement Reflection: Complete Verification with SMT Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, and Ranjit Jhala (University of Maryland, USA; University of California at San Diego, USA; Indiana University, USA; University of Edinburgh, UK; Input Output HK, UK) Artifacts Functional Proc. ACM Program. Lang., vol. 2, issue POPL: "Linear Haskell: Practical ..." Linear Haskell: Practical Linearity in a Higher-Order Polymorphic Language Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, and Arnaud Spiwack (University of Gothenburg, Sweden; Tweag I/O, France; Indiana University, USA; Microsoft Research, UK) Artifacts Functional
	Nguyễn, Phúc C.	Proc. ACM Program. Lang., vol. 2, issue POPL: "Soft Contract Verification ..." Soft Contract Verification for Higher-Order Stateful Programs Phúc C. Nguyễn, Thomas Gilray, Sam Tobin-Hochstadt, and David Van Horn (University of Maryland, USA; Indiana University, USA) Artifacts Functional
	Niksic, Filip	Proc. ACM Program. Lang., vol. 2, issue POPL: "Why Is Random Testing Effective ..." Why Is Random Testing Effective for Partition Tolerance Bugs? Rupak Majumdar and Filip Niksic (MPI-SWS, Germany)
	Novotný, Petr	Proc. ACM Program. Lang., vol. 2, issue POPL: "Lexicographic Ranking Supermartingales: ..." Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs Sheshansh Agrawal, Krishnendu Chatterjee, and Petr Novotný (IIT Bombay, India; IST Austria, Austria) Artifacts Functional
	Odersky, Martin	Proc. ACM Program. Lang., vol. 2, issue POPL: "Simplicitly: Foundations and ..." Simplicitly: Foundations and Applications of Implicit Function Types Martin Odersky, Olivier Blanvillain, Fengyun Liu, Aggelos Biboudis, Heather Miller, and Sandro Stucki (EPFL, Switzerland; Northeastern University, USA) Artifacts Functional
	Öhman, Joakim	Proc. ACM Program. Lang., vol. 2, issue POPL: "Decidability of Conversion ..." Decidability of Conversion for Type Theory in Type Theory Andreas Abel, Joakim Öhman, and Andrea Vezzosi (University of Gothenburg, Sweden; IMDEA Software Institute, Spain; Chalmers University of Technology, Sweden) Artifacts Functional
	Ong, C.-H. Luke	Proc. ACM Program. Lang., vol. 2, issue POPL: "Higher-Order Constrained Horn ..." Higher-Order Constrained Horn Clauses for Verification Toby Cathcart Burn, C.-H. Luke Ong, and Steven J. Ramsay (University of Oxford, UK; University of Bristol, UK) Artifacts Functional
	Ostermann, Klaus	Proc. ACM Program. Lang., vol. 2, issue POPL: "Denotational Validation of ..." Denotational Validation of Higher-Order Bayesian Inference Adam Ścibior, Ohad Kammar, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Sean K. Moss, Chris Heunen, and Zoubin Ghahramani (University of Cambridge, UK; MPI Tübingen, Germany; University of Oxford, UK; KAIST, South Korea; University of Tübingen, Germany; University of Edinburgh, UK; Uber AI Labs, USA)
	Padon, Oded	Proc. ACM Program. Lang., vol. 2, issue POPL: "Reducing Liveness to Safety ..." Reducing Liveness to Safety in First-Order Logic Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, and Sharon Shoham (Tel Aviv University, Israel; University of Freiburg, Germany; University of California at Los Angeles, USA) Artifacts Functional
	Pagani, Michele	Proc. ACM Program. Lang., vol. 2, issue POPL: "Measurable Cones and Stable, ..." Measurable Cones and Stable, Measurable Functions: A Model for Probabilistic Higher-Order Programming Thomas Ehrhard, Michele Pagani, and Christine Tasson (University of Paris Diderot, France; CNRS, France)
	Palsberg, Jens	Proc. ACM Program. Lang., vol. 2, issue POPL: "Jones-Optimal Partial Evaluation ..." Jones-Optimal Partial Evaluation by Specialization-Safe Normalization Matt Brown and Jens Palsberg (University of California at Los Angeles, USA) Artifacts Functional
	Paraskevopoulou, Zoe	Proc. ACM Program. Lang., vol. 2, issue POPL: "Generating Good Generators ..." Generating Good Generators for Inductive Relations Leonidas Lampropoulos, Zoe Paraskevopoulou, and Benjamin C. Pierce (University of Pennsylvania, USA; Princeton University, USA) Artifacts Functional
	Parreaux, Lionel	Proc. ACM Program. Lang., vol. 2, issue POPL: "Unifying Analytic and Statically-Typed ..." Unifying Analytic and Statically-Typed Quasiquotes Lionel Parreaux, Antoine Voizard, Amir Shaikhha, and Christoph E. Koch (EPFL, Switzerland; University of Pennsylvania, USA) Artifacts Functional
	Patrignani, Marco	Proc. ACM Program. Lang., vol. 2, issue POPL: "Parametricity versus the Universal ..." Parametricity versus the Universal Type Dominique Devriese, Marco Patrignani, and Frank Piessens (KU Leuven, Belgium; MPI-SWS, Germany; CISPA, Germany)
	Pavlogiannis, Andreas	Proc. ACM Program. Lang., vol. 2, issue POPL: "Optimal Dyck Reachability ..." Optimal Dyck Reachability for Data-Dependence and Alias Analysis Krishnendu Chatterjee, Bhavya Choudhary, and Andreas Pavlogiannis (IST Austria, Austria; IIT Bombay, India) Artifacts Functional Proc. ACM Program. Lang., vol. 2, issue POPL: "Data-Centric Dynamic Partial ..." Data-Centric Dynamic Partial Order Reduction Marek Chalupa, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya (Masaryk University, Czechia; IST Austria, Austria; Kena Labs, India; IIT Bombay, India)
	Pellissier, Luc	Proc. ACM Program. Lang., vol. 2, issue POPL: "Polyadic Approximations, Fibrations ..." Polyadic Approximations, Fibrations and Intersection Types Damiano Mazza, Luc Pellissier, and Pierre Vial (CNRS, France; University of Paris 13, France; University of Paris Diderot, France)
	Peña, Lucas	Proc. ACM Program. Lang., vol. 2, issue POPL: "Foundations for Natural Proofs ..." Foundations for Natural Proofs and Quantifier Instantiation Christof Löding, P. Madhusudan, and Lucas Peña (RWTH Aachen University, Germany; University of Illinois at Urbana-Champaign, USA) Artifacts Functional
	Pereira, Fernando Magno Quintão	Proc. ACM Program. Lang., vol. 2, issue POPL: "Inference of Static Semantics ..." Inference of Static Semantics for Incomplete C Programs Leandro T. C. Melo, Rodrigo G. Ribeiro, Marcus R. de Araújo, and Fernando Magno Quintão Pereira (Federal University of Minas Gerais, Brazil; Federal University of Ouro Preto, Brazil) Artifacts Functional
	Peyton Jones, Simon	Proc. ACM Program. Lang., vol. 2, issue POPL: "Linear Haskell: Practical ..." Linear Haskell: Practical Linearity in a Higher-Order Polymorphic Language Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, and Arnaud Spiwack (University of Gothenburg, Sweden; Tweag I/O, France; Indiana University, USA; Microsoft Research, UK) Artifacts Functional
	Pierce, Benjamin C.	Proc. ACM Program. Lang., vol. 2, issue POPL: "Synthesizing Bijective Lenses ..." Synthesizing Bijective Lenses Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve Zdancewic (Princeton University, USA; Tufts University, USA; University of Pennsylvania, USA) Artifacts Functional Proc. ACM Program. Lang., vol. 2, issue POPL: "Generating Good Generators ..." Generating Good Generators for Inductive Relations Leonidas Lampropoulos, Zoe Paraskevopoulou, and Benjamin C. Pierce (University of Pennsylvania, USA; Princeton University, USA) Artifacts Functional
	Piessens, Frank	Proc. ACM Program. Lang., vol. 2, issue POPL: "Parametricity versus the Universal ..." Parametricity versus the Universal Type Dominique Devriese, Marco Patrignani, and Frank Piessens (KU Leuven, Belgium; MPI-SWS, Germany; CISPA, Germany)
	Piróg, Maciej	Proc. ACM Program. Lang., vol. 2, issue POPL: "Handle with Care: Relational ..." Handle with Care: Relational Interpretation of Algebraic Effects and Handlers Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski (University of Wrocław, Poland) Artifacts Functional
	Podelski, Andreas	Proc. ACM Program. Lang., vol. 2, issue POPL: "Reducing Liveness to Safety ..." Reducing Liveness to Safety in First-Order Logic Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, and Sharon Shoham (Tel Aviv University, Israel; University of Freiburg, Germany; University of California at Los Angeles, USA) Artifacts Functional
	Polesiuk, Piotr	Proc. ACM Program. Lang., vol. 2, issue POPL: "Handle with Care: Relational ..." Handle with Care: Relational Interpretation of Algebraic Effects and Handlers Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski (University of Wrocław, Poland) Artifacts Functional
	Popescu, Andrei	Proc. ACM Program. Lang., vol. 2, issue POPL: "Safety and Conservativity ..." Safety and Conservativity of Definitions in HOL and Isabelle/HOL Ondřej Kunčar and Andrei Popescu (TU Munich, Germany; Middlesex University, UK; Institute of Mathematics at Romanian Academy, Romania)
	Pouchet, Louis-Noel	Proc. ACM Program. Lang., vol. 2, issue POPL: "Analytical Modeling of Cache ..." Analytical Modeling of Cache Behavior for Affine Programs Wenlei Bao, Sriram Krishnamoorthy, Louis-Noel Pouchet, and P. Sadayappan (Ohio State University, USA; Pacific Northwest National Laboratory, USA; Colorado State University, USA)
	Pulte, Christopher	Proc. ACM Program. Lang., vol. 2, issue POPL: "Simplifying ARM Concurrency: ..." Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8 Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell (University of Cambridge, UK; ARM, UK; University of St. Andrews, UK) Artifacts Functional
	Püschel, Markus	Proc. ACM Program. Lang., vol. 2, issue POPL: "A Practical Construction for ..." A Practical Construction for Decomposing Numerical Abstract Domains Gagandeep Singh, Markus Püschel, and Martin Vechev (ETH Zurich, Switzerland) Artifacts Functional
	Radiček, Ivan	Proc. ACM Program. Lang., vol. 2, issue POPL: "Monadic Refinements for Relational ..." Monadic Refinements for Relational Cost Analysis Ivan Radiček, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Florian Zuleger (Vienna University of Technology, Austria; IMDEA Software Institute, Spain; SUNY Buffalo, USA; MPI-SWS, Germany)
	Ramsay, Steven J.	Proc. ACM Program. Lang., vol. 2, issue POPL: "Higher-Order Constrained Horn ..." Higher-Order Constrained Horn Clauses for Verification Toby Cathcart Burn, C.-H. Luke Ong, and Steven J. Ramsay (University of Oxford, UK; University of Bristol, UK) Artifacts Functional
	Rastogi, Aseem	Proc. ACM Program. Lang., vol. 2, issue POPL: "Recalling a Witness: Foundations ..." Recalling a Witness: Foundations and Applications of Monotonic State Danel Ahman, Cédric Fournet, Cătălin Hriţcu, Kenji Maillard, Aseem Rastogi, and Nikhil Swamy (Inria, France; Microsoft Research, UK; ENS Paris, France; Microsoft Research, India; Microsoft Research, USA) Artifacts Functional
	Rémy, Didier	Proc. ACM Program. Lang., vol. 2, issue POPL: "A Principled Approach to Ornamentation ..." A Principled Approach to Ornamentation in ML Thomas Williams and Didier Rémy (Inria, France) Artifacts Functional
	Reps, Thomas	Proc. ACM Program. Lang., vol. 2, issue POPL: "Non-linear Reasoning for Invariant ..." Non-linear Reasoning for Invariant Synthesis Zachary Kincaid, John Cyphert, Jason Breck, and Thomas Reps (Princeton University, USA; University of Wisconsin-Madison, USA; GrammaTech, USA) Artifacts Functional
	Ribeiro, Rodrigo G.	Proc. ACM Program. Lang., vol. 2, issue POPL: "Inference of Static Semantics ..." Inference of Static Semantics for Incomplete C Programs Leandro T. C. Melo, Rodrigo G. Ribeiro, Marcus R. de Araújo, and Fernando Magno Quintão Pereira (Federal University of Minas Gerais, Brazil; Federal University of Ouro Preto, Brazil) Artifacts Functional
	Riely, James	Proc. ACM Program. Lang., vol. 2, issue POPL: "Transactions in Relaxed Memory ..." Transactions in Relaxed Memory Architectures Brijesh Dongol, Radha Jagadeesan, and James Riely (Brunel University London, UK; DePaul University, USA)
	Rinetzky, Noam	Proc. ACM Program. Lang., vol. 2, issue POPL: "Online Detection of Effectively ..." Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, and Yoni Zohar (Tel Aviv University, Israel; VMware, USA; Stanford University, USA) Artifacts Functional
	Rioux, Nick	Proc. ACM Program. Lang., vol. 2, issue POPL: "Type-Preserving CPS Translation ..." Type-Preserving CPS Translation of Σ and Π Types Is Not Not Possible William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed (Northeastern University, USA; Ochanomizu University, Japan)
	Rompf, Tiark	Proc. ACM Program. Lang., vol. 2, issue POPL: "Collapsing Towers of Interpreters ..." Collapsing Towers of Interpreters Nada Amin and Tiark Rompf (University of Cambridge, UK; Purdue University, USA) Artifacts Functional
	Rouvoet, Arjen	Proc. ACM Program. Lang., vol. 2, issue POPL: "Intrinsically-Typed Definitional ..." Intrinsically-Typed Definitional Interpreters for Imperative Languages Casper Bach Poulsen, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers, and Eelco Visser (Delft University of Technology, Netherlands; Portland State University, USA) Artifacts Functional
	Rümmer, Philipp	Proc. ACM Program. Lang., vol. 2, issue POPL: "String Constraints with Concatenation ..." String Constraints with Concatenation and Transducers Solved Efficiently Lukáš Holík, Petr Janků, Anthony W. Lin, Philipp Rümmer, and Tomáš Vojnar (Brno University of Technology, Czechia; University of Oxford, UK; Uppsala University, Sweden) Artifacts Functional
	Sadayappan, P.	Proc. ACM Program. Lang., vol. 2, issue POPL: "Analytical Modeling of Cache ..." Analytical Modeling of Cache Behavior for Affine Programs Wenlei Bao, Sriram Krishnamoorthy, Louis-Noel Pouchet, and P. Sadayappan (Ohio State University, USA; Pacific Northwest National Laboratory, USA; Colorado State University, USA)
	Sagiv, Mooly	Proc. ACM Program. Lang., vol. 2, issue POPL: "Reducing Liveness to Safety ..." Reducing Liveness to Safety in First-Order Logic Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, and Sharon Shoham (Tel Aviv University, Israel; University of Freiburg, Germany; University of California at Los Angeles, USA) Artifacts Functional Proc. ACM Program. Lang., vol. 2, issue POPL: "Online Detection of Effectively ..." Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, and Yoni Zohar (Tel Aviv University, Israel; VMware, USA; Stanford University, USA) Artifacts Functional
	Sagonas, Konstantinos	Proc. ACM Program. Lang., vol. 2, issue POPL: "Effective Stateless Model ..." Effective Stateless Model Checking for C/C++ Concurrency Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, and Viktor Vafeiadis (National Technical University of Athens, Greece; Tel Aviv University, Israel; Uppsala University, Sweden; MPI-SWS, Germany) Artifacts Functional
	Sarkar, Susmit	Proc. ACM Program. Lang., vol. 2, issue POPL: "Simplifying ARM Concurrency: ..." Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8 Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell (University of Cambridge, UK; ARM, UK; University of St. Andrews, UK) Artifacts Functional
	Satake, Yuki	Proc. ACM Program. Lang., vol. 2, issue POPL: "Relatively Complete Refinement ..." Relatively Complete Refinement Type System for Verification of Higher-Order Non-deterministic Programs Hiroshi Unno, Yuki Satake, and Tachio Terauchi (University of Tsukuba, Japan; Waseda University, Japan)
	Scherer, Gabriel	Proc. ACM Program. Lang., vol. 2, issue POPL: "Correctness of Speculative ..." Correctness of Speculative Optimizations with Dynamic Deoptimization Olivier Flückiger, Gabriel Scherer, Ming-Ho Yee, Aviral Goel, Amal Ahmed, and Jan Vitek (Northeastern University, USA; Inria, France; Czech Technical University, Czechia)
	Ścibior, Adam	Proc. ACM Program. Lang., vol. 2, issue POPL: "Denotational Validation of ..." Denotational Validation of Higher-Order Bayesian Inference Adam Ścibior, Ohad Kammar, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Sean K. Moss, Chris Heunen, and Zoubin Ghahramani (University of Cambridge, UK; MPI Tübingen, Germany; University of Oxford, UK; KAIST, South Korea; University of Tübingen, Germany; University of Edinburgh, UK; Uber AI Labs, USA)
	Scott, Ryan G.	Proc. ACM Program. Lang., vol. 2, issue POPL: "Refinement Reflection: Complete ..." Refinement Reflection: Complete Verification with SMT Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, and Ranjit Jhala (University of Maryland, USA; University of California at San Diego, USA; Indiana University, USA; University of Edinburgh, UK; Input Output HK, UK) Artifacts Functional
	Sergey, Ilya	Proc. ACM Program. Lang., vol. 2, issue POPL: "Programming and Proving with ..." Programming and Proving with Distributed Protocols Ilya Sergey, James R. Wilcox, and Zachary Tatlock (University College London, UK; University of Washington, USA) Artifacts Functional
	Sewell, Peter	Proc. ACM Program. Lang., vol. 2, issue POPL: "Simplifying ARM Concurrency: ..." Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8 Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell (University of Cambridge, UK; ARM, UK; University of St. Andrews, UK) Artifacts Functional
	Shaikhha, Amir	Proc. ACM Program. Lang., vol. 2, issue POPL: "Unifying Analytic and Statically-Typed ..." Unifying Analytic and Statically-Typed Quasiquotes Lionel Parreaux, Antoine Voizard, Amir Shaikhha, and Christoph E. Koch (EPFL, Switzerland; University of Pennsylvania, USA) Artifacts Functional
	Sharma, Rahul	Proc. ACM Program. Lang., vol. 2, issue POPL: "On Automatically Proving the ..." On Automatically Proving the Correctness of math.h Implementations Wonyeol Lee, Rahul Sharma, and Alex Aiken (Stanford University, USA; Microsoft Research, India)
	Shasha, Dennis	Proc. ACM Program. Lang., vol. 2, issue POPL: "Go with the Flow: Compositional ..." Go with the Flow: Compositional Abstractions for Concurrent Data Structures Siddharth Krishna, Dennis Shasha, and Thomas Wies (New York University, USA)
	Shoham, Sharon	Proc. ACM Program. Lang., vol. 2, issue POPL: "Reducing Liveness to Safety ..." Reducing Liveness to Safety in First-Order Logic Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, and Sharon Shoham (Tel Aviv University, Israel; University of Freiburg, Germany; University of California at Los Angeles, USA) Artifacts Functional
	Sieczkowski, Filip	Proc. ACM Program. Lang., vol. 2, issue POPL: "Handle with Care: Relational ..." Handle with Care: Relational Interpretation of Algebraic Effects and Handlers Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski (University of Wrocław, Poland) Artifacts Functional
	Singh, Gagandeep	Proc. ACM Program. Lang., vol. 2, issue POPL: "A Practical Construction for ..." A Practical Construction for Decomposing Numerical Abstract Domains Gagandeep Singh, Markus Püschel, and Martin Vechev (ETH Zurich, Switzerland) Artifacts Functional
	Singh, Rishabh	Proc. ACM Program. Lang., vol. 2, issue POPL: "WebRelate: Integrating Web ..." WebRelate: Integrating Web Data with Spreadsheets using Examples Jeevana Priya Inala and Rishabh Singh (Massachusetts Institute of Technology, USA; Microsoft Research, USA) Artifacts Functional Proc. ACM Program. Lang., vol. 2, issue POPL: "Program Synthesis using Abstraction ..." Program Synthesis using Abstraction Refinement Xinyu Wang, Isil Dillig, and Rishabh Singh (University of Texas at Austin, USA; Microsoft Research, USA)
	Sinha, Nishant	Proc. ACM Program. Lang., vol. 2, issue POPL: "Data-Centric Dynamic Partial ..." Data-Centric Dynamic Partial Order Reduction Marek Chalupa, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya (Masaryk University, Czechia; IST Austria, Austria; Kena Labs, India; IIT Bombay, India)
	Spiwack, Arnaud	Proc. ACM Program. Lang., vol. 2, issue POPL: "Linear Haskell: Practical ..." Linear Haskell: Practical Linearity in a Higher-Order Polymorphic Language Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, and Arnaud Spiwack (University of Gothenburg, Sweden; Tweag I/O, France; Indiana University, USA; Microsoft Research, UK) Artifacts Functional
	Staton, Sam	Proc. ACM Program. Lang., vol. 2, issue POPL: "Denotational Validation of ..." Denotational Validation of Higher-Order Bayesian Inference Adam Ścibior, Ohad Kammar, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Sean K. Moss, Chris Heunen, and Zoubin Ghahramani (University of Cambridge, UK; MPI Tübingen, Germany; University of Oxford, UK; KAIST, South Korea; University of Tübingen, Germany; University of Edinburgh, UK; Uber AI Labs, USA)
	Stefanesco, Léo	Proc. ACM Program. Lang., vol. 2, issue POPL: "A Logical Relation for Monadic ..." A Logical Relation for Monadic Encapsulation of State: Proving Contextual Equivalences in the Presence of runST Amin Timany, Léo Stefanesco, Morten Krogh-Jespersen, and Lars Birkedal (KU Leuven, Belgium; IRIF, France; CNRS, France; University of Paris Diderot, France; Aarhus University, Denmark) Artifacts Functional
	Strub, Pierre-Yves	Proc. ACM Program. Lang., vol. 2, issue POPL: "Proving Expected Sensitivity ..." Proving Expected Sensitivity of Probabilistic Programs Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub (IMDEA Software Institute, Spain; UPMC, France; Inria, France; University College London, UK; École Polytechnique, France) Artifacts Functional
	Stucki, Sandro	Proc. ACM Program. Lang., vol. 2, issue POPL: "Simplicitly: Foundations and ..." Simplicitly: Foundations and Applications of Implicit Function Types Martin Odersky, Olivier Blanvillain, Fengyun Liu, Aggelos Biboudis, Heather Miller, and Sandro Stucki (EPFL, Switzerland; Northeastern University, USA) Artifacts Functional
	Swamy, Nikhil	Proc. ACM Program. Lang., vol. 2, issue POPL: "Recalling a Witness: Foundations ..." Recalling a Witness: Foundations and Applications of Monotonic State Danel Ahman, Cédric Fournet, Cătălin Hriţcu, Kenji Maillard, Aseem Rastogi, and Nikhil Swamy (Inria, France; Microsoft Research, UK; ENS Paris, France; Microsoft Research, India; Microsoft Research, USA) Artifacts Functional
	Ta, Quang-Trung	Proc. ACM Program. Lang., vol. 2, issue POPL: "Automated Lemma Synthesis ..." Automated Lemma Synthesis in Symbolic-Heap Separation Logic Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin (National University of Singapore, Singapore) Artifacts Functional
	Tasson, Christine	Proc. ACM Program. Lang., vol. 2, issue POPL: "Measurable Cones and Stable, ..." Measurable Cones and Stable, Measurable Functions: A Model for Probabilistic Higher-Order Programming Thomas Ehrhard, Michele Pagani, and Christine Tasson (University of Paris Diderot, France; CNRS, France)
	Tatlock, Zachary	Proc. ACM Program. Lang., vol. 2, issue POPL: "Programming and Proving with ..." Programming and Proving with Distributed Protocols Ilya Sergey, James R. Wilcox, and Zachary Tatlock (University College London, UK; University of Washington, USA) Artifacts Functional
	Terauchi, Tachio	Proc. ACM Program. Lang., vol. 2, issue POPL: "Relatively Complete Refinement ..." Relatively Complete Refinement Type System for Verification of Higher-Order Non-deterministic Programs Hiroshi Unno, Yuki Satake, and Tachio Terauchi (University of Tsukuba, Japan; Waseda University, Japan)
	Timany, Amin	Proc. ACM Program. Lang., vol. 2, issue POPL: "A Logical Relation for Monadic ..." A Logical Relation for Monadic Encapsulation of State: Proving Contextual Equivalences in the Presence of runST Amin Timany, Léo Stefanesco, Morten Krogh-Jespersen, and Lars Birkedal (KU Leuven, Belgium; IRIF, France; CNRS, France; University of Paris Diderot, France; Aarhus University, Denmark) Artifacts Functional
	Tobin-Hochstadt, Sam	Proc. ACM Program. Lang., vol. 2, issue POPL: "Soft Contract Verification ..." Soft Contract Verification for Higher-Order Stateful Programs Phúc C. Nguyễn, Thomas Gilray, Sam Tobin-Hochstadt, and David Van Horn (University of Maryland, USA; Indiana University, USA) Artifacts Functional
	Tolmach, Andrew	Proc. ACM Program. Lang., vol. 2, issue POPL: "Intrinsically-Typed Definitional ..." Intrinsically-Typed Definitional Interpreters for Imperative Languages Casper Bach Poulsen, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers, and Eelco Visser (Delft University of Technology, Netherlands; Portland State University, USA) Artifacts Functional
	Tondwalkar, Anish	Proc. ACM Program. Lang., vol. 2, issue POPL: "Refinement Reflection: Complete ..." Refinement Reflection: Complete Verification with SMT Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, and Ranjit Jhala (University of Maryland, USA; University of California at San Diego, USA; Indiana University, USA; University of Edinburgh, UK; Input Output HK, UK) Artifacts Functional
	Torlak, Emina	Proc. ACM Program. Lang., vol. 2, issue POPL: "Symbolic Types for Lenient ..." Symbolic Types for Lenient Symbolic Execution Stephen Chang, Alex Knauth, and Emina Torlak (Northeastern University, USA; University of Washington, USA) Artifacts Functional
	Unno, Hiroshi	Proc. ACM Program. Lang., vol. 2, issue POPL: "Relatively Complete Refinement ..." Relatively Complete Refinement Type System for Verification of Higher-Order Non-deterministic Programs Hiroshi Unno, Yuki Satake, and Tachio Terauchi (University of Tsukuba, Japan; Waseda University, Japan)
	Vafeiadis, Viktor	Proc. ACM Program. Lang., vol. 2, issue POPL: "Effective Stateless Model ..." Effective Stateless Model Checking for C/C++ Concurrency Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, and Viktor Vafeiadis (National Technical University of Athens, Greece; Tel Aviv University, Israel; Uppsala University, Sweden; MPI-SWS, Germany) Artifacts Functional
	Vaidya, Kapil	Proc. ACM Program. Lang., vol. 2, issue POPL: "Data-Centric Dynamic Partial ..." Data-Centric Dynamic Partial Order Reduction Marek Chalupa, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya (Masaryk University, Czechia; IST Austria, Austria; Kena Labs, India; IIT Bombay, India)
	Vákár, Matthijs	Proc. ACM Program. Lang., vol. 2, issue POPL: "Denotational Validation of ..." Denotational Validation of Higher-Order Bayesian Inference Adam Ścibior, Ohad Kammar, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Sean K. Moss, Chris Heunen, and Zoubin Ghahramani (University of Cambridge, UK; MPI Tübingen, Germany; University of Oxford, UK; KAIST, South Korea; University of Tübingen, Germany; University of Edinburgh, UK; Uber AI Labs, USA)
	Van Horn, David	Proc. ACM Program. Lang., vol. 2, issue POPL: "Soft Contract Verification ..." Soft Contract Verification for Higher-Order Stateful Programs Phúc C. Nguyễn, Thomas Gilray, Sam Tobin-Hochstadt, and David Van Horn (University of Maryland, USA; Indiana University, USA) Artifacts Functional
	Vazou, Niki	Proc. ACM Program. Lang., vol. 2, issue POPL: "Refinement Reflection: Complete ..." Refinement Reflection: Complete Verification with SMT Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, and Ranjit Jhala (University of Maryland, USA; University of California at San Diego, USA; Indiana University, USA; University of Edinburgh, UK; Input Output HK, UK) Artifacts Functional
	Vechev, Martin	Proc. ACM Program. Lang., vol. 2, issue POPL: "A Practical Construction for ..." A Practical Construction for Decomposing Numerical Abstract Domains Gagandeep Singh, Markus Püschel, and Martin Vechev (ETH Zurich, Switzerland) Artifacts Functional
	Vezzosi, Andrea	Proc. ACM Program. Lang., vol. 2, issue POPL: "Decidability of Conversion ..." Decidability of Conversion for Type Theory in Type Theory Andreas Abel, Joakim Öhman, and Andrea Vezzosi (University of Gothenburg, Sweden; IMDEA Software Institute, Spain; Chalmers University of Technology, Sweden) Artifacts Functional
	Vial, Pierre	Proc. ACM Program. Lang., vol. 2, issue POPL: "Polyadic Approximations, Fibrations ..." Polyadic Approximations, Fibrations and Intersection Types Damiano Mazza, Luc Pellissier, and Pierre Vial (CNRS, France; University of Paris 13, France; University of Paris Diderot, France)
	Visser, Eelco	Proc. ACM Program. Lang., vol. 2, issue POPL: "Intrinsically-Typed Definitional ..." Intrinsically-Typed Definitional Interpreters for Imperative Languages Casper Bach Poulsen, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers, and Eelco Visser (Delft University of Technology, Netherlands; Portland State University, USA) Artifacts Functional
	Vitek, Jan	Proc. ACM Program. Lang., vol. 2, issue POPL: "Correctness of Speculative ..." Correctness of Speculative Optimizations with Dynamic Deoptimization Olivier Flückiger, Gabriel Scherer, Ming-Ho Yee, Aviral Goel, Amal Ahmed, and Jan Vitek (Northeastern University, USA; Inria, France; Czech Technical University, Czechia)
	Voizard, Antoine	Proc. ACM Program. Lang., vol. 2, issue POPL: "Unifying Analytic and Statically-Typed ..." Unifying Analytic and Statically-Typed Quasiquotes Lionel Parreaux, Antoine Voizard, Amir Shaikhha, and Christoph E. Koch (EPFL, Switzerland; University of Pennsylvania, USA) Artifacts Functional
	Vojnar, Tomáš	Proc. ACM Program. Lang., vol. 2, issue POPL: "String Constraints with Concatenation ..." String Constraints with Concatenation and Transducers Solved Efficiently Lukáš Holík, Petr Janků, Anthony W. Lin, Philipp Rümmer, and Tomáš Vojnar (Brno University of Technology, Czechia; University of Oxford, UK; Uppsala University, Sweden) Artifacts Functional
	Wadler, Philip	Proc. ACM Program. Lang., vol. 2, issue POPL: "Refinement Reflection: Complete ..." Refinement Reflection: Complete Verification with SMT Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, and Ranjit Jhala (University of Maryland, USA; University of California at San Diego, USA; Indiana University, USA; University of Edinburgh, UK; Input Output HK, UK) Artifacts Functional
	Walker, David	Proc. ACM Program. Lang., vol. 2, issue POPL: "Synthesizing Bijective Lenses ..." Synthesizing Bijective Lenses Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve Zdancewic (Princeton University, USA; Tufts University, USA; University of Pennsylvania, USA) Artifacts Functional
	Walkingshaw, Eric	Proc. ACM Program. Lang., vol. 2, issue POPL: "Migrating Gradual Types ..." Migrating Gradual Types John Peter Campora, Sheng Chen, Martin Erwig, and Eric Walkingshaw (University of Louisiana at Lafayette, USA; Oregon State University, USA) Artifacts Functional
	Wang, Xinyu	Proc. ACM Program. Lang., vol. 2, issue POPL: "Program Synthesis using Abstraction ..." Program Synthesis using Abstraction Refinement Xinyu Wang, Isil Dillig, and Rishabh Singh (University of Texas at Austin, USA; Microsoft Research, USA)
	Wang, Yuepeng	Proc. ACM Program. Lang., vol. 2, issue POPL: "Verifying Equivalence of Database-Driven ..." Verifying Equivalence of Database-Driven Applications Yuepeng Wang, Isil Dillig, Shuvendu K. Lahiri, and William R. Cook (University of Texas at Austin, USA; Microsoft Research, USA)
	Wies, Thomas	Proc. ACM Program. Lang., vol. 2, issue POPL: "Go with the Flow: Compositional ..." Go with the Flow: Compositional Abstractions for Concurrent Data Structures Siddharth Krishna, Dennis Shasha, and Thomas Wies (New York University, USA)
	Wilcox, James R.	Proc. ACM Program. Lang., vol. 2, issue POPL: "Programming and Proving with ..." Programming and Proving with Distributed Protocols Ilya Sergey, James R. Wilcox, and Zachary Tatlock (University College London, UK; University of Washington, USA) Artifacts Functional
	Williams, Thomas	Proc. ACM Program. Lang., vol. 2, issue POPL: "A Principled Approach to Ornamentation ..." A Principled Approach to Ornamentation in ML Thomas Williams and Didier Rémy (Inria, France) Artifacts Functional
	Wood, Thomas	Proc. ACM Program. Lang., vol. 2, issue POPL: "JaVerT: JavaScript Verification ..." JaVerT: JavaScript Verification Toolchain José Fragoso Santos, Petar Maksimović, Daiva Naudžiūnienė, Thomas Wood, and Philippa Gardner (Imperial College London, UK; Mathematical Institute SASA, Serbia) Artifacts Functional
	Wu, Zhilin	Proc. ACM Program. Lang., vol. 2, issue POPL: "What Is Decidable about String ..." What Is Decidable about String Constraints with the ReplaceAll Function Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu (University of London, UK; Institute of Software at Chinese Academy of Sciences, China; University at Chinese Academy of Sciences, China; Royal Holloway University of London, UK; University of Oxford, UK)
	Yang, Hongseok	Proc. ACM Program. Lang., vol. 2, issue POPL: "Denotational Validation of ..." Denotational Validation of Higher-Order Bayesian Inference Adam Ścibior, Ohad Kammar, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Sean K. Moss, Chris Heunen, and Zoubin Ghahramani (University of Cambridge, UK; MPI Tübingen, Germany; University of Oxford, UK; KAIST, South Korea; University of Tübingen, Germany; University of Edinburgh, UK; Uber AI Labs, USA)
	Yee, Ming-Ho	Proc. ACM Program. Lang., vol. 2, issue POPL: "Correctness of Speculative ..." Correctness of Speculative Optimizations with Dynamic Deoptimization Olivier Flückiger, Gabriel Scherer, Ming-Ho Yee, Aviral Goel, Amal Ahmed, and Jan Vitek (Northeastern University, USA; Inria, France; Czech Technical University, Czechia)
	Ying, Mingsheng	Proc. ACM Program. Lang., vol. 2, issue POPL: "Algorithmic Analysis of Termination ..." Algorithmic Analysis of Termination Problems for Quantum Programs Yangjia Li and Mingsheng Ying (Institute of Software at Chinese Academy of Sciences, China; University of Technology Sydney, Australia; Tsinghua University, China)
	Zdancewic, Steve	Proc. ACM Program. Lang., vol. 2, issue POPL: "Synthesizing Bijective Lenses ..." Synthesizing Bijective Lenses Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve Zdancewic (Princeton University, USA; Tufts University, USA; University of Pennsylvania, USA) Artifacts Functional
	Zohar, Yoni	Proc. ACM Program. Lang., vol. 2, issue POPL: "Online Detection of Effectively ..." Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, and Yoni Zohar (Tel Aviv University, Israel; VMware, USA; Stanford University, USA) Artifacts Functional
	Zuleger, Florian	Proc. ACM Program. Lang., vol. 2, issue POPL: "Monadic Refinements for Relational ..." Monadic Refinements for Relational Cost Analysis Ivan Radiček, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Florian Zuleger (Vienna University of Technology, Austria; IMDEA Software Institute, Spain; SUNY Buffalo, USA; MPI-SWS, Germany)

243 authors

proc time: 0.27