| |
Aanjaneya, Mridul
|
Proc. ACM Program. Lang., vol. 5, issue POPL: "An Approach to Generate Correctly ..."
An Approach to Generate Correctly Rounded Math Libraries for New Floating Point Variants
Jay P. Lim, Mridul Aanjaneya, John Gustafson, and Santosh Nagarakatte
(Rutgers University, USA; National University of Singapore, Singapore)
 Publisher's Version
 Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Abdulla, Parosh Aziz |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Deciding Reachability under ..."
Deciding Reachability under Persistent x86-TSO
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan
(Uppsala University, Sweden; University of Paris, France; Chennai Mathematical Institute, India; CNRS UMI ReLaX, India; Institute of Mathematical Sciences, India)
Publisher's Version
|
| |
Acar, Umut A. |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Provably Space-Efficient Parallel ..."
Provably Space-Efficient Parallel Functional Programming
Jatin Arora, Sam Westrick, and Umut A. Acar
(Carnegie Mellon University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Accattoli, Beniamino |
Proc. ACM Program. Lang., vol. 5, issue POPL: "The (In)Efficiency of Interaction ..."
The (In)Efficiency of Interaction
Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni
(Inria, France; École Polytechnique, France; University of Bologna, Italy)
Publisher's Version
|
| |
Aguirre, Alejandro |
Proc. ACM Program. Lang., vol. 5, issue POPL: "A Pre-expectation Calculus ..."
A Pre-expectation Calculus for Probabilistic Sensitivity
Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja
(IMDEA Software Institute, Spain; Universidad Politécnica de Madrid, Spain; MPI-SP, Germany; University of Wisconsin-Madison, USA; University College London, UK; RWTH Aachen University, Germany; ETH Zurich, Switzerland)
Publisher's Version
|
| |
Ahman, Danel |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Asynchronous Effects ..."
Asynchronous Effects
Danel Ahman and Matija Pretnar
(University of Ljubljana, Slovenia)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Almagor, Shaull |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Deciding ω-Regular Properties ..."
Deciding ω-Regular Properties on Linear Recurrence Sequences
Shaull Almagor, Toghrul Karimov, Edon Kelmendi, Joël Ouaknine, and James Worrell
(Technion, Israel; MPI-SWS, Germany; University of Oxford, UK)
Publisher's Version
|
| |
Angiuli, Carlo |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Internalizing Representation ..."
Internalizing Representation Independence with Univalence
Carlo Angiuli, Evan Cavallo, Anders Mörtberg, and Max Zeuner
(Carnegie Mellon University, USA; Stockholm University, Sweden)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Arashloo, Mina Tahmasbi |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Petr4: Formal Foundations ..."
Petr4: Formal Foundations for P4 Data Planes
Ryan Doenges, Mina Tahmasbi Arashloo, Santiago Bautista, Alexander Chang, Newton Ni, Samwise Parkinson, Rudy Peterson, Alaia Solko-Breslin, Amanda Xu, and Nate Foster
(Cornell University, USA; ENS Rennes, France)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Arora, Jatin |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Provably Space-Efficient Parallel ..."
Provably Space-Efficient Parallel Functional Programming
Jatin Arora, Sam Westrick, and Umut A. Acar
(Carnegie Mellon University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Atig, Mohamed Faouzi |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Deciding Reachability under ..."
Deciding Reachability under Persistent x86-TSO
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan
(Uppsala University, Sweden; University of Paris, France; Chennai Mathematical Institute, India; CNRS UMI ReLaX, India; Institute of Mathematical Sciences, India)
Publisher's Version
|
| |
Atkinson, Eric |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Simplifying Dependent Reductions ..."
Simplifying Dependent Reductions in the Polyhedral Model
Cambridge Yang, Eric Atkinson, and Michael Carbin
(Massachusetts Institute of Technology, USA)
Publisher's Version
|
| |
Bahr, Patrick
|
Proc. ACM Program. Lang., vol. 5, issue POPL: "Diamonds Are Not Forever: ..."
Diamonds Are Not Forever: Liveness in Reactive Programming with Guarded Recursion
Patrick Bahr, Christian Uldal Graulund, and Rasmus Ejlers Møgelberg
(IT University of Copenhagen, Denmark)
Publisher's Version
|
| |
Bañados Schwerter, Felipe |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Abstracting Gradual Typing ..."
Abstracting Gradual Typing Moving Forward: Precise and Space-Efficient
Felipe Bañados Schwerter, Alison M. Clark, Khurram A. Jafery, and Ronald Garcia
(University of British Columbia, Canada; Amazon, Canada)
Publisher's Version
|
| |
Banerjee, Anindya |
Proc. ACM Program. Lang., vol. 5, issue POPL: "On Algebraic Abstractions ..."
On Algebraic Abstractions for Concurrent Separation Logics
František Farka, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, and Ignacio Fábregas
(IMDEA Software Institute, Spain; Nomadic Labs, France; Complutense University of Madrid, Spain)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Barrière, Aurèle |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Formally Verified Speculation ..."
Formally Verified Speculation and Deoptimization in a JIT Compiler
Aurèle Barrière, Sandrine Blazy, Olivier Flückiger, David Pichardie, and Jan Vitek
(University of Rennes, France; Inria, France; CNRS, France; IRISA, France; Northeastern University, USA; Czech Technical University, Czechia)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Barthe, Gilles |
Proc. ACM Program. Lang., vol. 5, issue POPL: "A Pre-expectation Calculus ..."
A Pre-expectation Calculus for Probabilistic Sensitivity
Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja
(IMDEA Software Institute, Spain; Universidad Politécnica de Madrid, Spain; MPI-SP, Germany; University of Wisconsin-Madison, USA; University College London, UK; RWTH Aachen University, Germany; ETH Zurich, Switzerland)
Publisher's Version
Proc. ACM Program. Lang., vol. 5, issue POPL: "Deciding Accuracy of Differential ..."
Deciding Accuracy of Differential Privacy Schemes
Gilles Barthe, Rohit Chadha, Paul Krogmeier, A. Prasad Sistla, and Mahesh Viswanathan
(MPI-SP, Germany; University of Missouri, USA; University of Illinois at Urbana-Champaign, USA; University of Illinois at Chicago, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Batz, Kevin |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Relatively Complete Verification ..."
Relatively Complete Verification of Probabilistic Programs: An Expressive Language for Expectation-Based Reasoning
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja
(RWTH Aachen University, Germany; University College London, UK; ETH Zurich, Switzerland)
Publisher's Version
|
| |
Baumann, Pascal |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Context-Bounded Verification ..."
Context-Bounded Verification of Liveness Properties for Multithreaded Shared-Memory Programs
Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche
(MPI-SWS, Germany)
Publisher's Version
|
| |
Bautista, Santiago |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Petr4: Formal Foundations ..."
Petr4: Formal Foundations for P4 Data Planes
Ryan Doenges, Mina Tahmasbi Arashloo, Santiago Bautista, Alexander Chang, Newton Ni, Samwise Parkinson, Rudy Peterson, Alaia Solko-Breslin, Amanda Xu, and Nate Foster
(Cornell University, USA; ENS Rennes, France)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Bay, Johan |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Mechanized Logical Relations ..."
Mechanized Logical Relations for Termination-Insensitive Noninterference
Simon Oddershede Gregersen, Johan Bay, Amin Timany, and Lars Birkedal
(Aarhus University, Denmark)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Benedikt, Michael |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Generating Collection Transformations ..."
Generating Collection Transformations from Proofs
Michael Benedikt and Pierre Pradic
(University of Oxford, UK)
Publisher's Version
|
| |
Birkedal, Lars |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Mechanized Logical Relations ..."
Mechanized Logical Relations for Termination-Insensitive Noninterference
Simon Oddershede Gregersen, Johan Bay, Amin Timany, and Lars Birkedal
(Aarhus University, Denmark)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
Proc. ACM Program. Lang., vol. 5, issue POPL: "Distributed Causal Memory: ..."
Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic
Léon Gondelman, Simon Oddershede Gregersen, Abel Nieto, Amin Timany, and Lars Birkedal
(Aarhus University, Denmark)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
Proc. ACM Program. Lang., vol. 5, issue POPL: "Efficient and Provable Local ..."
Efficient and Provable Local Capability Revocation using Uninitialized Capabilities
Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Sander Huyghebaert, Dominique Devriese, and Lars Birkedal
(Aarhus University, Denmark; KU Leuven, Belgium; Vrije Universiteit Brussel, Belgium)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Blazy, Sandrine |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Formally Verified Speculation ..."
Formally Verified Speculation and Deoptimization in a JIT Compiler
Aurèle Barrière, Sandrine Blazy, Olivier Flückiger, David Pichardie, and Jan Vitek
(University of Rennes, France; Inria, France; CNRS, France; IRISA, France; Northeastern University, USA; Czech Technical University, Czechia)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Bouajjani, Ahmed |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Deciding Reachability under ..."
Deciding Reachability under Persistent x86-TSO
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan
(Uppsala University, Sweden; University of Paris, France; Chennai Mathematical Institute, India; CNRS UMI ReLaX, India; Institute of Mathematical Sciences, India)
Publisher's Version
|
| |
Carbin, Michael
|
Proc. ACM Program. Lang., vol. 5, issue POPL: "Simplifying Dependent Reductions ..."
Simplifying Dependent Reductions in the Polyhedral Model
Cambridge Yang, Eric Atkinson, and Michael Carbin
(Massachusetts Institute of Technology, USA)
Publisher's Version
Proc. ACM Program. Lang., vol. 5, issue POPL: "𝜆ₛ: Computable Semantics ..."
𝜆ₛ: Computable Semantics for Differentiable Programming with Higher-Order Functions and Datatypes
Benjamin Sherman, Jesse Michel, and Michael Carbin
(Massachusetts Institute of Technology, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Cauligi, Sunjay |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Automatically Eliminating ..."
Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade
Marco Vassena, Craig Disselkoen, Klaus von Gleissenthall, Sunjay Cauligi, Rami Gökhan Kıcı, Ranjit Jhala, Dean Tullsen, and Deian Stefan
(CISPA, Germany; University of California at San Diego, USA; Vrije Universiteit Amsterdam, Netherlands)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Cavallo, Evan |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Internalizing Representation ..."
Internalizing Representation Independence with Univalence
Carlo Angiuli, Evan Cavallo, Anders Mörtberg, and Max Zeuner
(Carnegie Mellon University, USA; Stockholm University, Sweden)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Cecchetti, Ethan |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Giving Semantics to Program-Counter ..."
Giving Semantics to Program-Counter Labels via Secure Effects
Andrew K. Hirsch and Ethan Cecchetti
(MPI-SWS, Germany; Cornell University, USA)
Publisher's Version
|
| |
Chadha, Rohit |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Deciding Accuracy of Differential ..."
Deciding Accuracy of Differential Privacy Schemes
Gilles Barthe, Rohit Chadha, Paul Krogmeier, A. Prasad Sistla, and Mahesh Viswanathan
(MPI-SP, Germany; University of Missouri, USA; University of Illinois at Urbana-Champaign, USA; University of Illinois at Chicago, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Chang, Alexander |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Petr4: Formal Foundations ..."
Petr4: Formal Foundations for P4 Data Planes
Ryan Doenges, Mina Tahmasbi Arashloo, Santiago Bautista, Alexander Chang, Newton Ni, Samwise Parkinson, Rudy Peterson, Alaia Solko-Breslin, Amanda Xu, and Nate Foster
(Cornell University, USA; ENS Rennes, France)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Chen, Chao-Hong |
Proc. ACM Program. Lang., vol. 5, issue POPL: "A Computational Interpretation ..."
A Computational Interpretation of Compact Closed Categories: Reversible Programming with Negative and Fractional Types
Chao-Hong Chen and Amr Sabry
(Indiana University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Choudhury, Pritam |
Proc. ACM Program. Lang., vol. 5, issue POPL: "A Graded Dependent Type System ..."
A Graded Dependent Type System with a Usage-Aware Semantics
Pritam Choudhury, Harley Eades III, Richard A. Eisenberg, and Stephanie Weirich
(University of Pennsylvania, USA; Augusta University, USA; Tweag I/O, France; Bryn Mawr College, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Clark, Alison M. |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Abstracting Gradual Typing ..."
Abstracting Gradual Typing Moving Forward: Precise and Space-Efficient
Felipe Bañados Schwerter, Alison M. Clark, Khurram A. Jafery, and Ronald Garcia
(University of British Columbia, Canada; Amazon, Canada)
Publisher's Version
|
| |
Cockx, Jesper |
Proc. ACM Program. Lang., vol. 5, issue POPL: "The Taming of the Rew: A Type ..."
The Taming of the Rew: A Type Theory with Computational Assumptions
Jesper Cockx, Nicolas Tabareau, and Théo Winterhalter
(Delft University of Technology, Netherlands; Inria, France; LS2N, France)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Courant, Nathanaël |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Verified Code Generation for ..."
Verified Code Generation for the Polyhedral Model
Nathanaël Courant and Xavier Leroy
(Inria, France; Collège de France, France; PSL University, France)
Publisher's Version
|
| |
Dal Lago, Ugo
|
Proc. ACM Program. Lang., vol. 5, issue POPL: "Intersection Types and (Positive) ..."
Intersection Types and (Positive) Almost-Sure Termination
Ugo Dal Lago, Claudia Faggian, and Simona Ronchi Della Rocca
(University of Bologna, Italy; University of Paris, France; IRIF, France; CNRS, France; University of Turin, Italy)
Publisher's Version
Proc. ACM Program. Lang., vol. 5, issue POPL: "The (In)Efficiency of Interaction ..."
The (In)Efficiency of Interaction
Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni
(Inria, France; École Polytechnique, France; University of Bologna, Italy)
Publisher's Version
|
| |
D'Antoni, Loris |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Semantics-Guided Synthesis ..."
Semantics-Guided Synthesis
Jinwoo Kim, Qinheping Hu, Loris D'Antoni, and Thomas Reps
(University of Wisconsin-Madison, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Delbianco, Germán Andrés |
Proc. ACM Program. Lang., vol. 5, issue POPL: "On Algebraic Abstractions ..."
On Algebraic Abstractions for Concurrent Separation Logics
František Farka, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, and Ignacio Fábregas
(IMDEA Software Institute, Spain; Nomadic Labs, France; Complutense University of Madrid, Spain)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
De Vilhena, Paulo Emílio |
Proc. ACM Program. Lang., vol. 5, issue POPL: "A Separation Logic for Effect ..."
A Separation Logic for Effect Handlers
Paulo Emílio de Vilhena and François Pottier
(Inria, France)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Devriese, Dominique |
Proc. ACM Program. Lang., vol. 5, issue POPL: "On the Semantic Expressiveness ..."
On the Semantic Expressiveness of Recursive Types
Marco Patrignani, Eric Mark Martin, and Dominique Devriese
(Stanford University, USA; CISPA, Germany; Vrije Universiteit Brussel, Belgium)
Publisher's Version
Proc. ACM Program. Lang., vol. 5, issue POPL: "Efficient and Provable Local ..."
Efficient and Provable Local Capability Revocation using Uninitialized Capabilities
Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Sander Huyghebaert, Dominique Devriese, and Lars Birkedal
(Aarhus University, Denmark; KU Leuven, Belgium; Vrije Universiteit Brussel, Belgium)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 5, issue POPL: "Fully Abstract from Static ..."
Fully Abstract from Static to Gradual
Koen Jacobs, Amin Timany, and Dominique Devriese
(KU Leuven, Belgium; Aarhus University, Denmark; Vrije Universiteit Brussel, Belgium)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Di Liberti, Ivan |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Functorial Semantics for Partial ..."
Functorial Semantics for Partial Theories
Ivan Di Liberti, Fosco Loregian, Chad Nester, and Paweł Sobociński
(Czech Academy of Sciences, Czechia; Tallinn University of Technology, Estonia)
Publisher's Version
|
| |
Dillig, Isil |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Verifying Correct Usage of ..."
Verifying Correct Usage of Context-Free API Protocols
Kostas Ferles, Jon Stephens, and Isil Dillig
(University of Texas at Austin, USA)
Publisher's Version
|
| |
Disselkoen, Craig |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Automatically Eliminating ..."
Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade
Marco Vassena, Craig Disselkoen, Klaus von Gleissenthall, Sunjay Cauligi, Rami Gökhan Kıcı, Ranjit Jhala, Dean Tullsen, and Deian Stefan
(CISPA, Germany; University of California at San Diego, USA; Vrije Universiteit Amsterdam, Netherlands)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Doenges, Ryan |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Petr4: Formal Foundations ..."
Petr4: Formal Foundations for P4 Data Planes
Ryan Doenges, Mina Tahmasbi Arashloo, Santiago Bautista, Alexander Chang, Newton Ni, Samwise Parkinson, Rudy Peterson, Alaia Solko-Breslin, Amanda Xu, and Nate Foster
(Cornell University, USA; ENS Rennes, France)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Dreyer, Derek |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Transfinite Step-Indexing ..."
Transfinite Step-Indexing for Termination
Simon Spies, Neel Krishnaswami, and Derek Dreyer
(MPI-SWS, Germany; University of Cambridge, UK)
Publisher's Version
|
| |
Eades III, Harley
|
Proc. ACM Program. Lang., vol. 5, issue POPL: "A Graded Dependent Type System ..."
A Graded Dependent Type System with a Usage-Aware Semantics
Pritam Choudhury, Harley Eades III, Richard A. Eisenberg, and Stephanie Weirich
(University of Pennsylvania, USA; Augusta University, USA; Tweag I/O, France; Bryn Mawr College, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Eisenberg, Richard A. |
Proc. ACM Program. Lang., vol. 5, issue POPL: "A Graded Dependent Type System ..."
A Graded Dependent Type System with a Usage-Aware Semantics
Pritam Choudhury, Harley Eades III, Richard A. Eisenberg, and Stephanie Weirich
(University of Pennsylvania, USA; Augusta University, USA; Tweag I/O, France; Bryn Mawr College, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Fábregas, Ignacio
|
Proc. ACM Program. Lang., vol. 5, issue POPL: "On Algebraic Abstractions ..."
On Algebraic Abstractions for Concurrent Separation Logics
František Farka, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, and Ignacio Fábregas
(IMDEA Software Institute, Spain; Nomadic Labs, France; Complutense University of Madrid, Spain)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Faggian, Claudia |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Intersection Types and (Positive) ..."
Intersection Types and (Positive) Almost-Sure Termination
Ugo Dal Lago, Claudia Faggian, and Simona Ronchi Della Rocca
(University of Bologna, Italy; University of Paris, France; IRIF, France; CNRS, France; University of Turin, Italy)
Publisher's Version
|
| |
Farka, František |
Proc. ACM Program. Lang., vol. 5, issue POPL: "On Algebraic Abstractions ..."
On Algebraic Abstractions for Concurrent Separation Logics
František Farka, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, and Ignacio Fábregas
(IMDEA Software Institute, Spain; Nomadic Labs, France; Complutense University of Madrid, Spain)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Feldman, Yotam M. Y. |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Learning the Boundary of Inductive ..."
Learning the Boundary of Inductive Invariants
Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, and James R. Wilcox
(Tel Aviv University, Israel; Certora, USA)
Publisher's Version
|
| |
Ferles, Kostas |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Verifying Correct Usage of ..."
Verifying Correct Usage of Context-Free API Protocols
Kostas Ferles, Jon Stephens, and Isil Dillig
(University of Texas at Austin, USA)
Publisher's Version
|
| |
Flatt, Oliver |
Proc. ACM Program. Lang., vol. 5, issue POPL: "egg: Fast and Extensible Equality ..."
egg: Fast and Extensible Equality Saturation
Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha
(University of Washington, USA; University of Utah, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Flückiger, Olivier |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Formally Verified Speculation ..."
Formally Verified Speculation and Deoptimization in a JIT Compiler
Aurèle Barrière, Sandrine Blazy, Olivier Flückiger, David Pichardie, and Jan Vitek
(University of Rennes, France; Inria, France; CNRS, France; IRISA, France; Northeastern University, USA; Czech Technical University, Czechia)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Foster, Nate |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Petr4: Formal Foundations ..."
Petr4: Formal Foundations for P4 Data Planes
Ryan Doenges, Mina Tahmasbi Arashloo, Santiago Bautista, Alexander Chang, Newton Ni, Samwise Parkinson, Rudy Peterson, Alaia Solko-Breslin, Amanda Xu, and Nate Foster
(Cornell University, USA; ENS Rennes, France)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Gaboardi, Marco
|
Proc. ACM Program. Lang., vol. 5, issue POPL: "A Unifying Type-Theory for ..."
A Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis
Vineet Rajani, Marco Gaboardi, Deepak Garg, and Jan Hoffmann
(MPI-SP, Germany; Boston University, USA; MPI-SWS, Germany; Carnegie Mellon University, USA)
Publisher's Version
|
| |
Garcia, Ronald |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Abstracting Gradual Typing ..."
Abstracting Gradual Typing Moving Forward: Precise and Space-Efficient
Felipe Bañados Schwerter, Alison M. Clark, Khurram A. Jafery, and Ronald Garcia
(University of British Columbia, Canada; Amazon, Canada)
Publisher's Version
|
| |
Garg, Deepak |
Proc. ACM Program. Lang., vol. 5, issue POPL: "A Unifying Type-Theory for ..."
A Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis
Vineet Rajani, Marco Gaboardi, Deepak Garg, and Jan Hoffmann
(MPI-SP, Germany; Boston University, USA; MPI-SWS, Germany; Carnegie Mellon University, USA)
Publisher's Version
|
| |
Georges, Aïna Linn |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Efficient and Provable Local ..."
Efficient and Provable Local Capability Revocation using Uninitialized Capabilities
Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Sander Huyghebaert, Dominique Devriese, and Lars Birkedal
(Aarhus University, Denmark; KU Leuven, Belgium; Vrije Universiteit Brussel, Belgium)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Ghilezan, Silvia |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Precise Subtyping for Asynchronous ..."
Precise Subtyping for Asynchronous Multiparty Sessions
Silvia Ghilezan, Jovanka Pantović, Ivan Prokić, Alceste Scalas, and Nobuko Yoshida
(University of Novi Sad, Serbia; DTU, Denmark; Aston University, UK; Imperial College London, UK)
Publisher's Version
|
| |
Gleissenthall, Klaus von |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Automatically Eliminating ..."
Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade
Marco Vassena, Craig Disselkoen, Klaus von Gleissenthall, Sunjay Cauligi, Rami Gökhan Kıcı, Ranjit Jhala, Dean Tullsen, and Deian Stefan
(CISPA, Germany; University of California at San Diego, USA; Vrije Universiteit Amsterdam, Netherlands)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Gondelman, Léon |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Distributed Causal Memory: ..."
Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic
Léon Gondelman, Simon Oddershede Gregersen, Abel Nieto, Amin Timany, and Lars Birkedal
(Aarhus University, Denmark)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Graulund, Christian Uldal |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Diamonds Are Not Forever: ..."
Diamonds Are Not Forever: Liveness in Reactive Programming with Guarded Recursion
Patrick Bahr, Christian Uldal Graulund, and Rasmus Ejlers Møgelberg
(IT University of Copenhagen, Denmark)
Publisher's Version
|
| |
Gregersen, Simon Oddershede |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Mechanized Logical Relations ..."
Mechanized Logical Relations for Termination-Insensitive Noninterference
Simon Oddershede Gregersen, Johan Bay, Amin Timany, and Lars Birkedal
(Aarhus University, Denmark)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
Proc. ACM Program. Lang., vol. 5, issue POPL: "Distributed Causal Memory: ..."
Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic
Léon Gondelman, Simon Oddershede Gregersen, Abel Nieto, Amin Timany, and Lars Birkedal
(Aarhus University, Denmark)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Guéneau, Armaël |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Efficient and Provable Local ..."
Efficient and Provable Local Capability Revocation using Uninitialized Capabilities
Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Sander Huyghebaert, Dominique Devriese, and Lars Birkedal
(Aarhus University, Denmark; KU Leuven, Belgium; Vrije Universiteit Brussel, Belgium)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Gustafson, John |
Proc. ACM Program. Lang., vol. 5, issue POPL: "An Approach to Generate Correctly ..."
An Approach to Generate Correctly Rounded Math Libraries for New Floating Point Variants
Jay P. Lim, Mridul Aanjaneya, John Gustafson, and Santosh Nagarakatte
(Rutgers University, USA; National University of Singapore, Singapore)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Gutsfeld, Jens Oliver |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Automata and Fixpoints for ..."
Automata and Fixpoints for Asynchronous Hyperproperties
Jens Oliver Gutsfeld, Markus Müller-Olm, and Christoph Ohrem
(University of Münster, Germany)
Publisher's Version
|
| |
Hack, Sebastian
|
Proc. ACM Program. Lang., vol. 5, issue POPL: "An Abstract Interpretation ..."
An Abstract Interpretation for SPMD Divergence on Reducible Control Flow Graphs
Julian Rosemann, Simon Moll, and Sebastian Hack
(Saarland University, Germany; NEC, Germany)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Hicks, Michael |
Proc. ACM Program. Lang., vol. 5, issue POPL: "A Verified Optimizer for Quantum ..."
A Verified Optimizer for Quantum Circuits
Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, and Michael Hicks
(University of Maryland, USA; University of Chicago, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Hietala, Kesha |
Proc. ACM Program. Lang., vol. 5, issue POPL: "A Verified Optimizer for Quantum ..."
A Verified Optimizer for Quantum Circuits
Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, and Michael Hicks
(University of Maryland, USA; University of Chicago, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Hirsch, Andrew K. |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Giving Semantics to Program-Counter ..."
Giving Semantics to Program-Counter Labels via Secure Effects
Andrew K. Hirsch and Ethan Cecchetti
(MPI-SWS, Germany; Cornell University, USA)
Publisher's Version
|
| |
Hoffmann, Jan |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Modeling and Analyzing Evaluation ..."
Modeling and Analyzing Evaluation Cost of CUDA Kernels
Stefan K. Muller and Jan Hoffmann
(Illinois Institute of Technology, USA; Carnegie Mellon University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
Proc. ACM Program. Lang., vol. 5, issue POPL: "A Unifying Type-Theory for ..."
A Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis
Vineet Rajani, Marco Gaboardi, Deepak Garg, and Jan Hoffmann
(MPI-SP, Germany; Boston University, USA; MPI-SWS, Germany; Carnegie Mellon University, USA)
Publisher's Version
|
| |
Hsu, Justin |
Proc. ACM Program. Lang., vol. 5, issue POPL: "A Pre-expectation Calculus ..."
A Pre-expectation Calculus for Probabilistic Sensitivity
Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja
(IMDEA Software Institute, Spain; Universidad Politécnica de Madrid, Spain; MPI-SP, Germany; University of Wisconsin-Madison, USA; University College London, UK; RWTH Aachen University, Germany; ETH Zurich, Switzerland)
Publisher's Version
|
| |
Hu, Qinheping |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Semantics-Guided Synthesis ..."
Semantics-Guided Synthesis
Jinwoo Kim, Qinheping Hu, Loris D'Antoni, and Thomas Reps
(University of Wisconsin-Madison, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Hung, Shih-Han |
Proc. ACM Program. Lang., vol. 5, issue POPL: "A Verified Optimizer for Quantum ..."
A Verified Optimizer for Quantum Circuits
Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, and Michael Hicks
(University of Maryland, USA; University of Chicago, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Huyghebaert, Sander |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Efficient and Provable Local ..."
Efficient and Provable Local Capability Revocation using Uninitialized Capabilities
Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Sander Huyghebaert, Dominique Devriese, and Lars Birkedal
(Aarhus University, Denmark; KU Leuven, Belgium; Vrije Universiteit Brussel, Belgium)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Jacobs, Jules
|
Proc. ACM Program. Lang., vol. 5, issue POPL: "Paradoxes of Probabilistic ..."
Paradoxes of Probabilistic Programming: And How to Condition on Events of Measure Zero with Infinitesimal Probabilities
Jules Jacobs
(Radboud University Nijmegen, Netherlands; Delft University of Technology, Netherlands)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Jacobs, Koen |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Fully Abstract from Static ..."
Fully Abstract from Static to Gradual
Koen Jacobs, Amin Timany, and Dominique Devriese
(KU Leuven, Belgium; Aarhus University, Denmark; Vrije Universiteit Brussel, Belgium)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Jafery, Khurram A. |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Abstracting Gradual Typing ..."
Abstracting Gradual Typing Moving Forward: Precise and Space-Efficient
Felipe Bañados Schwerter, Alison M. Clark, Khurram A. Jafery, and Ronald Garcia
(University of British Columbia, Canada; Amazon, Canada)
Publisher's Version
|
| |
Jhala, Ranjit |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Automatically Eliminating ..."
Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade
Marco Vassena, Craig Disselkoen, Klaus von Gleissenthall, Sunjay Cauligi, Rami Gökhan Kıcı, Ranjit Jhala, Dean Tullsen, and Deian Stefan
(CISPA, Germany; University of California at San Diego, USA; Vrije Universiteit Amsterdam, Netherlands)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Jones, Eddie |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Intensional Datatype Refinement: ..."
Intensional Datatype Refinement: With Application to Scalable Verification of Pattern-Match Safety
Eddie Jones and Steven Ramsay
(University of Bristol, UK)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Kaminski, Benjamin Lucien
|
Proc. ACM Program. Lang., vol. 5, issue POPL: "Relatively Complete Verification ..."
Relatively Complete Verification of Probabilistic Programs: An Expressive Language for Expectation-Based Reasoning
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja
(RWTH Aachen University, Germany; University College London, UK; ETH Zurich, Switzerland)
Publisher's Version
Proc. ACM Program. Lang., vol. 5, issue POPL: "A Pre-expectation Calculus ..."
A Pre-expectation Calculus for Probabilistic Sensitivity
Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja
(IMDEA Software Institute, Spain; Universidad Politécnica de Madrid, Spain; MPI-SP, Germany; University of Wisconsin-Madison, USA; University College London, UK; RWTH Aachen University, Germany; ETH Zurich, Switzerland)
Publisher's Version
|
| |
Karimov, Toghrul |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Deciding ω-Regular Properties ..."
Deciding ω-Regular Properties on Linear Recurrence Sequences
Shaull Almagor, Toghrul Karimov, Edon Kelmendi, Joël Ouaknine, and James Worrell
(Technion, Israel; MPI-SWS, Germany; University of Oxford, UK)
Publisher's Version
|
| |
Katoen, Joost-Pieter |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Relatively Complete Verification ..."
Relatively Complete Verification of Probabilistic Programs: An Expressive Language for Expectation-Based Reasoning
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja
(RWTH Aachen University, Germany; University College London, UK; ETH Zurich, Switzerland)
Publisher's Version
Proc. ACM Program. Lang., vol. 5, issue POPL: "A Pre-expectation Calculus ..."
A Pre-expectation Calculus for Probabilistic Sensitivity
Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja
(IMDEA Software Institute, Spain; Universidad Politécnica de Madrid, Spain; MPI-SP, Germany; University of Wisconsin-Madison, USA; University College London, UK; RWTH Aachen University, Germany; ETH Zurich, Switzerland)
Publisher's Version
|
| |
Kaysin, Ilya |
Proc. ACM Program. Lang., vol. 5, issue POPL: "PerSeVerE: Persistency Semantics ..."
PerSeVerE: Persistency Semantics for Verification under Ext4
Michalis Kokologiannakis, Ilya Kaysin, Azalea Raad, and Viktor Vafeiadis
(MPI-SWS, Germany; National Research University Higher School of Economics, Russia; JetBrains Research, Russia; Imperial College London, UK)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Kelmendi, Edon |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Deciding ω-Regular Properties ..."
Deciding ω-Regular Properties on Linear Recurrence Sequences
Shaull Almagor, Toghrul Karimov, Edon Kelmendi, Joël Ouaknine, and James Worrell
(Technion, Israel; MPI-SWS, Germany; University of Oxford, UK)
Publisher's Version
|
| |
Khyzha, Artem |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Taming x86-TSO Persistency ..."
Taming x86-TSO Persistency
Artem Khyzha and Ori Lahav
(Tel Aviv University, Israel)
Publisher's Version
|
| |
Kıcı, Rami Gökhan |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Automatically Eliminating ..."
Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade
Marco Vassena, Craig Disselkoen, Klaus von Gleissenthall, Sunjay Cauligi, Rami Gökhan Kıcı, Ranjit Jhala, Dean Tullsen, and Deian Stefan
(CISPA, Germany; University of California at San Diego, USA; Vrije Universiteit Amsterdam, Netherlands)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Kim, Jinwoo |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Semantics-Guided Synthesis ..."
Semantics-Guided Synthesis
Jinwoo Kim, Qinheping Hu, Loris D'Antoni, and Thomas Reps
(University of Wisconsin-Madison, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Kokologiannakis, Michalis |
Proc. ACM Program. Lang., vol. 5, issue POPL: "PerSeVerE: Persistency Semantics ..."
PerSeVerE: Persistency Semantics for Verification under Ext4
Michalis Kokologiannakis, Ilya Kaysin, Azalea Raad, and Viktor Vafeiadis
(MPI-SWS, Germany; National Research University Higher School of Economics, Russia; JetBrains Research, Russia; Imperial College London, UK)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Krebbers, Robbert |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Intrinsically Typed Compilation ..."
Intrinsically Typed Compilation with Nameless Labels
Arjen Rouvoet, Robbert Krebbers, and Eelco Visser
(Delft University of Technology, Netherlands; Radboud University Nijmegen, Netherlands)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Krishnaswami, Neel |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Transfinite Step-Indexing ..."
Transfinite Step-Indexing for Termination
Simon Spies, Neel Krishnaswami, and Derek Dreyer
(MPI-SWS, Germany; University of Cambridge, UK)
Publisher's Version
|
| |
Krogmeier, Paul |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Deciding Accuracy of Differential ..."
Deciding Accuracy of Differential Privacy Schemes
Gilles Barthe, Rohit Chadha, Paul Krogmeier, A. Prasad Sistla, and Mahesh Viswanathan
(MPI-SP, Germany; University of Missouri, USA; University of Illinois at Urbana-Champaign, USA; University of Illinois at Chicago, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Kumar, K. Narayan |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Deciding Reachability under ..."
Deciding Reachability under Persistent x86-TSO
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan
(Uppsala University, Sweden; University of Paris, France; Chennai Mathematical Institute, India; CNRS UMI ReLaX, India; Institute of Mathematical Sciences, India)
Publisher's Version
|
| |
Kuperberg, Denis |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Cyclic Proofs, System T, and ..."
Cyclic Proofs, System T, and the Power of Contraction
Denis Kuperberg, Laureline Pinault, and Damien Pous
(University of Lyon, France; CNRS, France; ENS Lyon, France; Claude Bernard University Lyon 1, France; LIP, France)
Publisher's Version
|
| |
Lahav, Ori
|
Proc. ACM Program. Lang., vol. 5, issue POPL: "Taming x86-TSO Persistency ..."
Taming x86-TSO Persistency
Artem Khyzha and Ori Lahav
(Tel Aviv University, Israel)
Publisher's Version
Proc. ACM Program. Lang., vol. 5, issue POPL: "Verifying Observational Robustness ..."
Verifying Observational Robustness against a C11-Style Memory Model
Roy Margalit and Ori Lahav
(Tel Aviv University, Israel)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Lee, Woosuk |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Combining the Top-Down Propagation ..."
Combining the Top-Down Propagation and Bottom-Up Enumeration for Inductive Program Synthesis
Woosuk Lee
(Hanyang University, South Korea)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Leroy, Xavier |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Verified Code Generation for ..."
Verified Code Generation for the Polyhedral Model
Nathanaël Courant and Xavier Leroy
(Inria, France; Collège de France, France; PSL University, France)
Publisher's Version
|
| |
Li, Yuanbo |
Proc. ACM Program. Lang., vol. 5, issue POPL: "On the Complexity of Bidirected ..."
On the Complexity of Bidirected Interleaved Dyck-Reachability
Yuanbo Li, Qirun Zhang, and Thomas Reps
(Georgia Institute of Technology, USA; University of Wisconsin-Madison, USA)
Publisher's Version
|
| |
Lim, Jay P. |
Proc. ACM Program. Lang., vol. 5, issue POPL: "An Approach to Generate Correctly ..."
An Approach to Generate Correctly Rounded Math Libraries for New Floating Point Variants
Jay P. Lim, Mridul Aanjaneya, John Gustafson, and Santosh Nagarakatte
(Rutgers University, USA; National University of Singapore, Singapore)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Loregian, Fosco |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Functorial Semantics for Partial ..."
Functorial Semantics for Partial Theories
Ivan Di Liberti, Fosco Loregian, Chad Nester, and Paweł Sobociński
(Czech Academy of Sciences, Czechia; Tallinn University of Technology, Estonia)
Publisher's Version
|
| |
Majumdar, Rupak
|
Proc. ACM Program. Lang., vol. 5, issue POPL: "Context-Bounded Verification ..."
Context-Bounded Verification of Liveness Properties for Multithreaded Shared-Memory Programs
Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche
(MPI-SWS, Germany)
Publisher's Version
|
| |
Margalit, Roy |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Verifying Observational Robustness ..."
Verifying Observational Robustness against a C11-Style Memory Model
Roy Margalit and Ori Lahav
(Tel Aviv University, Israel)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Martin, Eric Mark |
Proc. ACM Program. Lang., vol. 5, issue POPL: "On the Semantic Expressiveness ..."
On the Semantic Expressiveness of Recursive Types
Marco Patrignani, Eric Mark Martin, and Dominique Devriese
(Stanford University, USA; CISPA, Germany; Vrije Universiteit Brussel, Belgium)
Publisher's Version
|
| |
Matheja, Christoph |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Relatively Complete Verification ..."
Relatively Complete Verification of Probabilistic Programs: An Expressive Language for Expectation-Based Reasoning
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja
(RWTH Aachen University, Germany; University College London, UK; ETH Zurich, Switzerland)
Publisher's Version
Proc. ACM Program. Lang., vol. 5, issue POPL: "A Pre-expectation Calculus ..."
A Pre-expectation Calculus for Probabilistic Sensitivity
Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja
(IMDEA Software Institute, Spain; Universidad Politécnica de Madrid, Spain; MPI-SP, Germany; University of Wisconsin-Madison, USA; University College London, UK; RWTH Aachen University, Germany; ETH Zurich, Switzerland)
Publisher's Version
|
| |
Mathiasen, Anders Alnor |
Proc. ACM Program. Lang., vol. 5, issue POPL: "The Fine-Grained and Parallel ..."
The Fine-Grained and Parallel Complexity of Andersen’s Pointer Analysis
Anders Alnor Mathiasen and Andreas Pavlogiannis
(Aarhus University, Denmark)
Publisher's Version
|
| |
Mathur, Umang |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Optimal Prediction of Synchronization-Preserving ..."
Optimal Prediction of Synchronization-Preserving Races
Umang Mathur, Andreas Pavlogiannis, and Mahesh Viswanathan
(University of Illinois at Urbana-Champaign, USA; Aarhus University, Denmark)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Mazza, Damiano |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Automatic Differentiation ..."
Automatic Differentiation in PCF
Damiano Mazza and Michele Pagani
(CNRS, France; University of Paris, France)
Publisher's Version
|
| |
Michel, Jesse |
Proc. ACM Program. Lang., vol. 5, issue POPL: "𝜆ₛ: Computable Semantics ..."
𝜆ₛ: Computable Semantics for Differentiable Programming with Higher-Order Functions and Datatypes
Benjamin Sherman, Jesse Michel, and Michael Carbin
(Massachusetts Institute of Technology, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Møgelberg, Rasmus Ejlers |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Diamonds Are Not Forever: ..."
Diamonds Are Not Forever: Liveness in Reactive Programming with Guarded Recursion
Patrick Bahr, Christian Uldal Graulund, and Rasmus Ejlers Møgelberg
(IT University of Copenhagen, Denmark)
Publisher's Version
|
| |
Moll, Simon |
Proc. ACM Program. Lang., vol. 5, issue POPL: "An Abstract Interpretation ..."
An Abstract Interpretation for SPMD Divergence on Reducible Control Flow Graphs
Julian Rosemann, Simon Moll, and Sebastian Hack
(Saarland University, Germany; NEC, Germany)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Mörtberg, Anders |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Internalizing Representation ..."
Internalizing Representation Independence with Univalence
Carlo Angiuli, Evan Cavallo, Anders Mörtberg, and Max Zeuner
(Carnegie Mellon University, USA; Stockholm University, Sweden)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Moy, Cameron |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Corpse Reviver: Sound and ..."
Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification
Cameron Moy, Phúc C. Nguyễn, Sam Tobin-Hochstadt, and David Van Horn
(Northeastern University, USA; University of Maryland, USA; Indiana University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Muller, Stefan K. |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Modeling and Analyzing Evaluation ..."
Modeling and Analyzing Evaluation Cost of CUDA Kernels
Stefan K. Muller and Jan Hoffmann
(Illinois Institute of Technology, USA; Carnegie Mellon University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Müller-Olm, Markus |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Automata and Fixpoints for ..."
Automata and Fixpoints for Asynchronous Hyperproperties
Jens Oliver Gutsfeld, Markus Müller-Olm, and Christoph Ohrem
(University of Münster, Germany)
Publisher's Version
|
| |
Nagarakatte, Santosh
|
Proc. ACM Program. Lang., vol. 5, issue POPL: "An Approach to Generate Correctly ..."
An Approach to Generate Correctly Rounded Math Libraries for New Floating Point Variants
Jay P. Lim, Mridul Aanjaneya, John Gustafson, and Santosh Nagarakatte
(Rutgers University, USA; National University of Singapore, Singapore)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Nandi, Chandrakana |
Proc. ACM Program. Lang., vol. 5, issue POPL: "egg: Fast and Extensible Equality ..."
egg: Fast and Extensible Equality Saturation
Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha
(University of Washington, USA; University of Utah, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Nanevski, Aleksandar |
Proc. ACM Program. Lang., vol. 5, issue POPL: "On Algebraic Abstractions ..."
On Algebraic Abstractions for Concurrent Separation Logics
František Farka, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, and Ignacio Fábregas
(IMDEA Software Institute, Spain; Nomadic Labs, France; Complutense University of Madrid, Spain)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Nester, Chad |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Functorial Semantics for Partial ..."
Functorial Semantics for Partial Theories
Ivan Di Liberti, Fosco Loregian, Chad Nester, and Paweł Sobociński
(Czech Academy of Sciences, Czechia; Tallinn University of Technology, Estonia)
Publisher's Version
|
| |
Nguyễn, Phúc C. |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Corpse Reviver: Sound and ..."
Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification
Cameron Moy, Phúc C. Nguyễn, Sam Tobin-Hochstadt, and David Van Horn
(Northeastern University, USA; University of Maryland, USA; Indiana University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Ni, Newton |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Petr4: Formal Foundations ..."
Petr4: Formal Foundations for P4 Data Planes
Ryan Doenges, Mina Tahmasbi Arashloo, Santiago Bautista, Alexander Chang, Newton Ni, Samwise Parkinson, Rudy Peterson, Alaia Solko-Breslin, Amanda Xu, and Nate Foster
(Cornell University, USA; ENS Rennes, France)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Nieto, Abel |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Distributed Causal Memory: ..."
Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic
Léon Gondelman, Simon Oddershede Gregersen, Abel Nieto, Amin Timany, and Lars Birkedal
(Aarhus University, Denmark)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Ohrem, Christoph
|
Proc. ACM Program. Lang., vol. 5, issue POPL: "Automata and Fixpoints for ..."
Automata and Fixpoints for Asynchronous Hyperproperties
Jens Oliver Gutsfeld, Markus Müller-Olm, and Christoph Ohrem
(University of Münster, Germany)
Publisher's Version
|
| |
Ouaknine, Joël |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Deciding ω-Regular Properties ..."
Deciding ω-Regular Properties on Linear Recurrence Sequences
Shaull Almagor, Toghrul Karimov, Edon Kelmendi, Joël Ouaknine, and James Worrell
(Technion, Israel; MPI-SWS, Germany; University of Oxford, UK)
Publisher's Version
|
| |
Pagani, Michele
|
Proc. ACM Program. Lang., vol. 5, issue POPL: "Automatic Differentiation ..."
Automatic Differentiation in PCF
Damiano Mazza and Michele Pagani
(CNRS, France; University of Paris, France)
Publisher's Version
|
| |
Panchekha, Pavel |
Proc. ACM Program. Lang., vol. 5, issue POPL: "egg: Fast and Extensible Equality ..."
egg: Fast and Extensible Equality Saturation
Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha
(University of Washington, USA; University of Utah, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Pantović, Jovanka |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Precise Subtyping for Asynchronous ..."
Precise Subtyping for Asynchronous Multiparty Sessions
Silvia Ghilezan, Jovanka Pantović, Ivan Prokić, Alceste Scalas, and Nobuko Yoshida
(University of Novi Sad, Serbia; DTU, Denmark; Aston University, UK; Imperial College London, UK)
Publisher's Version
|
| |
Parkinson, Samwise |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Petr4: Formal Foundations ..."
Petr4: Formal Foundations for P4 Data Planes
Ryan Doenges, Mina Tahmasbi Arashloo, Santiago Bautista, Alexander Chang, Newton Ni, Samwise Parkinson, Rudy Peterson, Alaia Solko-Breslin, Amanda Xu, and Nate Foster
(Cornell University, USA; ENS Rennes, France)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Patrignani, Marco |
Proc. ACM Program. Lang., vol. 5, issue POPL: "On the Semantic Expressiveness ..."
On the Semantic Expressiveness of Recursive Types
Marco Patrignani, Eric Mark Martin, and Dominique Devriese
(Stanford University, USA; CISPA, Germany; Vrije Universiteit Brussel, Belgium)
Publisher's Version
|
| |
Pavlinovic, Zvonimir |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Data Flow Refinement Type ..."
Data Flow Refinement Type Inference
Zvonimir Pavlinovic, Yusen Su, and Thomas Wies
(New York University, USA; Google, USA; University of Waterloo, Canada)
Publisher's Version
|
| |
Pavlogiannis, Andreas |
Proc. ACM Program. Lang., vol. 5, issue POPL: "The Fine-Grained and Parallel ..."
The Fine-Grained and Parallel Complexity of Andersen’s Pointer Analysis
Anders Alnor Mathiasen and Andreas Pavlogiannis
(Aarhus University, Denmark)
Publisher's Version
Proc. ACM Program. Lang., vol. 5, issue POPL: "Optimal Prediction of Synchronization-Preserving ..."
Optimal Prediction of Synchronization-Preserving Races
Umang Mathur, Andreas Pavlogiannis, and Mahesh Viswanathan
(University of Illinois at Urbana-Champaign, USA; Aarhus University, Denmark)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Peterson, Rudy |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Petr4: Formal Foundations ..."
Petr4: Formal Foundations for P4 Data Planes
Ryan Doenges, Mina Tahmasbi Arashloo, Santiago Bautista, Alexander Chang, Newton Ni, Samwise Parkinson, Rudy Peterson, Alaia Solko-Breslin, Amanda Xu, and Nate Foster
(Cornell University, USA; ENS Rennes, France)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Pichardie, David |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Formally Verified Speculation ..."
Formally Verified Speculation and Deoptimization in a JIT Compiler
Aurèle Barrière, Sandrine Blazy, Olivier Flückiger, David Pichardie, and Jan Vitek
(University of Rennes, France; Inria, France; CNRS, France; IRISA, France; Northeastern University, USA; Czech Technical University, Czechia)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Pinault, Laureline |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Cyclic Proofs, System T, and ..."
Cyclic Proofs, System T, and the Power of Contraction
Denis Kuperberg, Laureline Pinault, and Damien Pous
(University of Lyon, France; CNRS, France; ENS Lyon, France; Claude Bernard University Lyon 1, France; LIP, France)
Publisher's Version
|
| |
Pottier, François |
Proc. ACM Program. Lang., vol. 5, issue POPL: "A Separation Logic for Effect ..."
A Separation Logic for Effect Handlers
Paulo Emílio de Vilhena and François Pottier
(Inria, France)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Pous, Damien |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Cyclic Proofs, System T, and ..."
Cyclic Proofs, System T, and the Power of Contraction
Denis Kuperberg, Laureline Pinault, and Damien Pous
(University of Lyon, France; CNRS, France; ENS Lyon, France; Claude Bernard University Lyon 1, France; LIP, France)
Publisher's Version
|
| |
Pradic, Pierre |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Generating Collection Transformations ..."
Generating Collection Transformations from Proofs
Michael Benedikt and Pierre Pradic
(University of Oxford, UK)
Publisher's Version
|
| |
Pretnar, Matija |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Asynchronous Effects ..."
Asynchronous Effects
Danel Ahman and Matija Pretnar
(University of Ljubljana, Slovenia)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Prokić, Ivan |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Precise Subtyping for Asynchronous ..."
Precise Subtyping for Asynchronous Multiparty Sessions
Silvia Ghilezan, Jovanka Pantović, Ivan Prokić, Alceste Scalas, and Nobuko Yoshida
(University of Novi Sad, Serbia; DTU, Denmark; Aston University, UK; Imperial College London, UK)
Publisher's Version
|
| |
Raad, Azalea
|
Proc. ACM Program. Lang., vol. 5, issue POPL: "PerSeVerE: Persistency Semantics ..."
PerSeVerE: Persistency Semantics for Verification under Ext4
Michalis Kokologiannakis, Ilya Kaysin, Azalea Raad, and Viktor Vafeiadis
(MPI-SWS, Germany; National Research University Higher School of Economics, Russia; JetBrains Research, Russia; Imperial College London, UK)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Rajani, Vineet |
Proc. ACM Program. Lang., vol. 5, issue POPL: "A Unifying Type-Theory for ..."
A Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis
Vineet Rajani, Marco Gaboardi, Deepak Garg, and Jan Hoffmann
(MPI-SP, Germany; Boston University, USA; MPI-SWS, Germany; Carnegie Mellon University, USA)
Publisher's Version
|
| |
Ramsay, Steven |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Intensional Datatype Refinement: ..."
Intensional Datatype Refinement: With Application to Scalable Verification of Pattern-Match Safety
Eddie Jones and Steven Ramsay
(University of Bristol, UK)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Rand, Robert |
Proc. ACM Program. Lang., vol. 5, issue POPL: "A Verified Optimizer for Quantum ..."
A Verified Optimizer for Quantum Circuits
Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, and Michael Hicks
(University of Maryland, USA; University of Chicago, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Reps, Thomas |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Semantics-Guided Synthesis ..."
Semantics-Guided Synthesis
Jinwoo Kim, Qinheping Hu, Loris D'Antoni, and Thomas Reps
(University of Wisconsin-Madison, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 5, issue POPL: "On the Complexity of Bidirected ..."
On the Complexity of Bidirected Interleaved Dyck-Reachability
Yuanbo Li, Qirun Zhang, and Thomas Reps
(Georgia Institute of Technology, USA; University of Wisconsin-Madison, USA)
Publisher's Version
|
| |
Reynaud, Alban |
Proc. ACM Program. Lang., vol. 5, issue POPL: "A Practical Mode System for ..."
A Practical Mode System for Recursive Definitions
Alban Reynaud, Gabriel Scherer, and Jeremy Yallop
(ENS Lyon, France; Inria, France; University of Cambridge, UK)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Rocca, Simona Ronchi Della |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Intersection Types and (Positive) ..."
Intersection Types and (Positive) Almost-Sure Termination
Ugo Dal Lago, Claudia Faggian, and Simona Ronchi Della Rocca
(University of Bologna, Italy; University of Paris, France; IRIF, France; CNRS, France; University of Turin, Italy)
Publisher's Version
|
| |
Rosemann, Julian |
Proc. ACM Program. Lang., vol. 5, issue POPL: "An Abstract Interpretation ..."
An Abstract Interpretation for SPMD Divergence on Reducible Control Flow Graphs
Julian Rosemann, Simon Moll, and Sebastian Hack
(Saarland University, Germany; NEC, Germany)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Rouvoet, Arjen |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Intrinsically Typed Compilation ..."
Intrinsically Typed Compilation with Nameless Labels
Arjen Rouvoet, Robbert Krebbers, and Eelco Visser
(Delft University of Technology, Netherlands; Radboud University Nijmegen, Netherlands)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Sabok, Marcin
|
Proc. ACM Program. Lang., vol. 5, issue POPL: "Probabilistic Programming ..."
Probabilistic Programming Semantics for Name Generation
Marcin Sabok, Sam Staton, Dario Stein, and Michael Wolman
(McGill University, Canada; University of Oxford, UK)
Publisher's Version
|
| |
Sabry, Amr |
Proc. ACM Program. Lang., vol. 5, issue POPL: "A Computational Interpretation ..."
A Computational Interpretation of Compact Closed Categories: Reversible Programming with Negative and Fractional Types
Chao-Hong Chen and Amr Sabry
(Indiana University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Sagiv, Mooly |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Learning the Boundary of Inductive ..."
Learning the Boundary of Inductive Invariants
Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, and James R. Wilcox
(Tel Aviv University, Israel; Certora, USA)
Publisher's Version
|
| |
Saivasan, Prakash |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Deciding Reachability under ..."
Deciding Reachability under Persistent x86-TSO
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan
(Uppsala University, Sweden; University of Paris, France; Chennai Mathematical Institute, India; CNRS UMI ReLaX, India; Institute of Mathematical Sciences, India)
Publisher's Version
|
| |
Scalas, Alceste |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Precise Subtyping for Asynchronous ..."
Precise Subtyping for Asynchronous Multiparty Sessions
Silvia Ghilezan, Jovanka Pantović, Ivan Prokić, Alceste Scalas, and Nobuko Yoshida
(University of Novi Sad, Serbia; DTU, Denmark; Aston University, UK; Imperial College London, UK)
Publisher's Version
|
| |
Scherer, Gabriel |
Proc. ACM Program. Lang., vol. 5, issue POPL: "A Practical Mode System for ..."
A Practical Mode System for Recursive Definitions
Alban Reynaud, Gabriel Scherer, and Jeremy Yallop
(ENS Lyon, France; Inria, France; University of Cambridge, UK)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Sherman, Benjamin |
Proc. ACM Program. Lang., vol. 5, issue POPL: "𝜆ₛ: Computable Semantics ..."
𝜆ₛ: Computable Semantics for Differentiable Programming with Higher-Order Functions and Datatypes
Benjamin Sherman, Jesse Michel, and Michael Carbin
(Massachusetts Institute of Technology, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Shoham, Sharon |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Learning the Boundary of Inductive ..."
Learning the Boundary of Inductive Invariants
Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, and James R. Wilcox
(Tel Aviv University, Israel; Certora, USA)
Publisher's Version
|
| |
Silver, Lucas |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Dijkstra Monads Forever: Termination-Sensitive ..."
Dijkstra Monads Forever: Termination-Sensitive Specifications for Interaction Trees
Lucas Silver and Steve Zdancewic
(University of Pennsylvania, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Sistla, A. Prasad |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Deciding Accuracy of Differential ..."
Deciding Accuracy of Differential Privacy Schemes
Gilles Barthe, Rohit Chadha, Paul Krogmeier, A. Prasad Sistla, and Mahesh Viswanathan
(MPI-SP, Germany; University of Missouri, USA; University of Illinois at Urbana-Champaign, USA; University of Illinois at Chicago, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Sobociński, Paweł |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Functorial Semantics for Partial ..."
Functorial Semantics for Partial Theories
Ivan Di Liberti, Fosco Loregian, Chad Nester, and Paweł Sobociński
(Czech Academy of Sciences, Czechia; Tallinn University of Technology, Estonia)
Publisher's Version
|
| |
Solko-Breslin, Alaia |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Petr4: Formal Foundations ..."
Petr4: Formal Foundations for P4 Data Planes
Ryan Doenges, Mina Tahmasbi Arashloo, Santiago Bautista, Alexander Chang, Newton Ni, Samwise Parkinson, Rudy Peterson, Alaia Solko-Breslin, Amanda Xu, and Nate Foster
(Cornell University, USA; ENS Rennes, France)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Spies, Simon |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Transfinite Step-Indexing ..."
Transfinite Step-Indexing for Termination
Simon Spies, Neel Krishnaswami, and Derek Dreyer
(MPI-SWS, Germany; University of Cambridge, UK)
Publisher's Version
|
| |
Staton, Sam |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Probabilistic Programming ..."
Probabilistic Programming Semantics for Name Generation
Marcin Sabok, Sam Staton, Dario Stein, and Michael Wolman
(McGill University, Canada; University of Oxford, UK)
Publisher's Version
|
| |
Stefan, Deian |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Automatically Eliminating ..."
Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade
Marco Vassena, Craig Disselkoen, Klaus von Gleissenthall, Sunjay Cauligi, Rami Gökhan Kıcı, Ranjit Jhala, Dean Tullsen, and Deian Stefan
(CISPA, Germany; University of California at San Diego, USA; Vrije Universiteit Amsterdam, Netherlands)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Stein, Dario |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Probabilistic Programming ..."
Probabilistic Programming Semantics for Name Generation
Marcin Sabok, Sam Staton, Dario Stein, and Michael Wolman
(McGill University, Canada; University of Oxford, UK)
Publisher's Version
|
| |
Stephens, Jon |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Verifying Correct Usage of ..."
Verifying Correct Usage of Context-Free API Protocols
Kostas Ferles, Jon Stephens, and Isil Dillig
(University of Texas at Austin, USA)
Publisher's Version
|
| |
Su, Yusen |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Data Flow Refinement Type ..."
Data Flow Refinement Type Inference
Zvonimir Pavlinovic, Yusen Su, and Thomas Wies
(New York University, USA; Google, USA; University of Waterloo, Canada)
Publisher's Version
|
| |
Tabareau, Nicolas
|
Proc. ACM Program. Lang., vol. 5, issue POPL: "The Taming of the Rew: A Type ..."
The Taming of the Rew: A Type Theory with Computational Assumptions
Jesper Cockx, Nicolas Tabareau, and Théo Winterhalter
(Delft University of Technology, Netherlands; Inria, France; LS2N, France)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Tatlock, Zachary |
Proc. ACM Program. Lang., vol. 5, issue POPL: "egg: Fast and Extensible Equality ..."
egg: Fast and Extensible Equality Saturation
Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha
(University of Washington, USA; University of Utah, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Thinniyam, Ramanathan S. |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Context-Bounded Verification ..."
Context-Bounded Verification of Liveness Properties for Multithreaded Shared-Memory Programs
Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche
(MPI-SWS, Germany)
Publisher's Version
|
| |
Timany, Amin |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Mechanized Logical Relations ..."
Mechanized Logical Relations for Termination-Insensitive Noninterference
Simon Oddershede Gregersen, Johan Bay, Amin Timany, and Lars Birkedal
(Aarhus University, Denmark)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
Proc. ACM Program. Lang., vol. 5, issue POPL: "Distributed Causal Memory: ..."
Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic
Léon Gondelman, Simon Oddershede Gregersen, Abel Nieto, Amin Timany, and Lars Birkedal
(Aarhus University, Denmark)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
Proc. ACM Program. Lang., vol. 5, issue POPL: "Efficient and Provable Local ..."
Efficient and Provable Local Capability Revocation using Uninitialized Capabilities
Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Sander Huyghebaert, Dominique Devriese, and Lars Birkedal
(Aarhus University, Denmark; KU Leuven, Belgium; Vrije Universiteit Brussel, Belgium)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 5, issue POPL: "Fully Abstract from Static ..."
Fully Abstract from Static to Gradual
Koen Jacobs, Amin Timany, and Dominique Devriese
(KU Leuven, Belgium; Aarhus University, Denmark; Vrije Universiteit Brussel, Belgium)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Tobin-Hochstadt, Sam |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Corpse Reviver: Sound and ..."
Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification
Cameron Moy, Phúc C. Nguyễn, Sam Tobin-Hochstadt, and David Van Horn
(Northeastern University, USA; University of Maryland, USA; Indiana University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Trieu, Alix |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Efficient and Provable Local ..."
Efficient and Provable Local Capability Revocation using Uninitialized Capabilities
Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Sander Huyghebaert, Dominique Devriese, and Lars Birkedal
(Aarhus University, Denmark; KU Leuven, Belgium; Vrije Universiteit Brussel, Belgium)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Tullsen, Dean |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Automatically Eliminating ..."
Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade
Marco Vassena, Craig Disselkoen, Klaus von Gleissenthall, Sunjay Cauligi, Rami Gökhan Kıcı, Ranjit Jhala, Dean Tullsen, and Deian Stefan
(CISPA, Germany; University of California at San Diego, USA; Vrije Universiteit Amsterdam, Netherlands)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Vafeiadis, Viktor
|
Proc. ACM Program. Lang., vol. 5, issue POPL: "PerSeVerE: Persistency Semantics ..."
PerSeVerE: Persistency Semantics for Verification under Ext4
Michalis Kokologiannakis, Ilya Kaysin, Azalea Raad, and Viktor Vafeiadis
(MPI-SWS, Germany; National Research University Higher School of Economics, Russia; JetBrains Research, Russia; Imperial College London, UK)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Van Horn, David |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Corpse Reviver: Sound and ..."
Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification
Cameron Moy, Phúc C. Nguyễn, Sam Tobin-Hochstadt, and David Van Horn
(Northeastern University, USA; University of Maryland, USA; Indiana University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Vanoni, Gabriele |
Proc. ACM Program. Lang., vol. 5, issue POPL: "The (In)Efficiency of Interaction ..."
The (In)Efficiency of Interaction
Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni
(Inria, France; École Polytechnique, France; University of Bologna, Italy)
Publisher's Version
|
| |
Van Strydonck, Thomas |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Efficient and Provable Local ..."
Efficient and Provable Local Capability Revocation using Uninitialized Capabilities
Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Sander Huyghebaert, Dominique Devriese, and Lars Birkedal
(Aarhus University, Denmark; KU Leuven, Belgium; Vrije Universiteit Brussel, Belgium)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Vassena, Marco |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Automatically Eliminating ..."
Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade
Marco Vassena, Craig Disselkoen, Klaus von Gleissenthall, Sunjay Cauligi, Rami Gökhan Kıcı, Ranjit Jhala, Dean Tullsen, and Deian Stefan
(CISPA, Germany; University of California at San Diego, USA; Vrije Universiteit Amsterdam, Netherlands)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Visser, Eelco |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Intrinsically Typed Compilation ..."
Intrinsically Typed Compilation with Nameless Labels
Arjen Rouvoet, Robbert Krebbers, and Eelco Visser
(Delft University of Technology, Netherlands; Radboud University Nijmegen, Netherlands)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Viswanathan, Mahesh |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Optimal Prediction of Synchronization-Preserving ..."
Optimal Prediction of Synchronization-Preserving Races
Umang Mathur, Andreas Pavlogiannis, and Mahesh Viswanathan
(University of Illinois at Urbana-Champaign, USA; Aarhus University, Denmark)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 5, issue POPL: "Deciding Accuracy of Differential ..."
Deciding Accuracy of Differential Privacy Schemes
Gilles Barthe, Rohit Chadha, Paul Krogmeier, A. Prasad Sistla, and Mahesh Viswanathan
(MPI-SP, Germany; University of Missouri, USA; University of Illinois at Urbana-Champaign, USA; University of Illinois at Chicago, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Vitek, Jan |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Formally Verified Speculation ..."
Formally Verified Speculation and Deoptimization in a JIT Compiler
Aurèle Barrière, Sandrine Blazy, Olivier Flückiger, David Pichardie, and Jan Vitek
(University of Rennes, France; Inria, France; CNRS, France; IRISA, France; Northeastern University, USA; Czech Technical University, Czechia)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Wang, Yisu Remy
|
Proc. ACM Program. Lang., vol. 5, issue POPL: "egg: Fast and Extensible Equality ..."
egg: Fast and Extensible Equality Saturation
Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha
(University of Washington, USA; University of Utah, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Weirich, Stephanie |
Proc. ACM Program. Lang., vol. 5, issue POPL: "A Graded Dependent Type System ..."
A Graded Dependent Type System with a Usage-Aware Semantics
Pritam Choudhury, Harley Eades III, Richard A. Eisenberg, and Stephanie Weirich
(University of Pennsylvania, USA; Augusta University, USA; Tweag I/O, France; Bryn Mawr College, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Westrick, Sam |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Provably Space-Efficient Parallel ..."
Provably Space-Efficient Parallel Functional Programming
Jatin Arora, Sam Westrick, and Umut A. Acar
(Carnegie Mellon University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Wies, Thomas |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Data Flow Refinement Type ..."
Data Flow Refinement Type Inference
Zvonimir Pavlinovic, Yusen Su, and Thomas Wies
(New York University, USA; Google, USA; University of Waterloo, Canada)
Publisher's Version
|
| |
Wilcox, James R. |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Learning the Boundary of Inductive ..."
Learning the Boundary of Inductive Invariants
Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, and James R. Wilcox
(Tel Aviv University, Israel; Certora, USA)
Publisher's Version
|
| |
Willsey, Max |
Proc. ACM Program. Lang., vol. 5, issue POPL: "egg: Fast and Extensible Equality ..."
egg: Fast and Extensible Equality Saturation
Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha
(University of Washington, USA; University of Utah, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Winterhalter, Théo |
Proc. ACM Program. Lang., vol. 5, issue POPL: "The Taming of the Rew: A Type ..."
The Taming of the Rew: A Type Theory with Computational Assumptions
Jesper Cockx, Nicolas Tabareau, and Théo Winterhalter
(Delft University of Technology, Netherlands; Inria, France; LS2N, France)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Wolman, Michael |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Probabilistic Programming ..."
Probabilistic Programming Semantics for Name Generation
Marcin Sabok, Sam Staton, Dario Stein, and Michael Wolman
(McGill University, Canada; University of Oxford, UK)
Publisher's Version
|
| |
Worrell, James |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Deciding ω-Regular Properties ..."
Deciding ω-Regular Properties on Linear Recurrence Sequences
Shaull Almagor, Toghrul Karimov, Edon Kelmendi, Joël Ouaknine, and James Worrell
(Technion, Israel; MPI-SWS, Germany; University of Oxford, UK)
Publisher's Version
|
| |
Wu, Xiaodi |
Proc. ACM Program. Lang., vol. 5, issue POPL: "A Verified Optimizer for Quantum ..."
A Verified Optimizer for Quantum Circuits
Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, and Michael Hicks
(University of Maryland, USA; University of Chicago, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Xu, Amanda
|
Proc. ACM Program. Lang., vol. 5, issue POPL: "Petr4: Formal Foundations ..."
Petr4: Formal Foundations for P4 Data Planes
Ryan Doenges, Mina Tahmasbi Arashloo, Santiago Bautista, Alexander Chang, Newton Ni, Samwise Parkinson, Rudy Peterson, Alaia Solko-Breslin, Amanda Xu, and Nate Foster
(Cornell University, USA; ENS Rennes, France)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Yallop, Jeremy
|
Proc. ACM Program. Lang., vol. 5, issue POPL: "A Practical Mode System for ..."
A Practical Mode System for Recursive Definitions
Alban Reynaud, Gabriel Scherer, and Jeremy Yallop
(ENS Lyon, France; Inria, France; University of Cambridge, UK)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Yang, Cambridge |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Simplifying Dependent Reductions ..."
Simplifying Dependent Reductions in the Polyhedral Model
Cambridge Yang, Eric Atkinson, and Michael Carbin
(Massachusetts Institute of Technology, USA)
Publisher's Version
|
| |
Yoshida, Nobuko |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Precise Subtyping for Asynchronous ..."
Precise Subtyping for Asynchronous Multiparty Sessions
Silvia Ghilezan, Jovanka Pantović, Ivan Prokić, Alceste Scalas, and Nobuko Yoshida
(University of Novi Sad, Serbia; DTU, Denmark; Aston University, UK; Imperial College London, UK)
Publisher's Version
|
| |
Zdancewic, Steve
|
Proc. ACM Program. Lang., vol. 5, issue POPL: "Dijkstra Monads Forever: Termination-Sensitive ..."
Dijkstra Monads Forever: Termination-Sensitive Specifications for Interaction Trees
Lucas Silver and Steve Zdancewic
(University of Pennsylvania, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Artifacts Functional
|
| |
Zetzsche, Georg |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Context-Bounded Verification ..."
Context-Bounded Verification of Liveness Properties for Multithreaded Shared-Memory Programs
Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche
(MPI-SWS, Germany)
Publisher's Version
|
| |
Zeuner, Max |
Proc. ACM Program. Lang., vol. 5, issue POPL: "Internalizing Representation ..."
Internalizing Representation Independence with Univalence
Carlo Angiuli, Evan Cavallo, Anders Mörtberg, and Max Zeuner
(Carnegie Mellon University, USA; Stockholm University, Sweden)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Zhang, Qirun |
Proc. ACM Program. Lang., vol. 5, issue POPL: "On the Complexity of Bidirected ..."
On the Complexity of Bidirected Interleaved Dyck-Reachability
Yuanbo Li, Qirun Zhang, and Thomas Reps
(Georgia Institute of Technology, USA; University of Wisconsin-Madison, USA)
Publisher's Version
|