| |
Aceto, Luca
|
Proc. ACM Program. Lang., vol. 3, issue POPL: "Adventures in Monitorability: ..."
Adventures in Monitorability: From Branching to Linear Time and Back Again
Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen
(Gran Sasso Science Institute, Iceland; Reykjavik University, Iceland; University of Malta, Malta; University of Kiel, Germany; University of Liverpool, UK)
 Publisher's Version
|
| |
Achilleos, Antonis |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Adventures in Monitorability: ..."
Adventures in Monitorability: From Branching to Linear Time and Back Again
Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen
(Gran Sasso Science Institute, Iceland; Reykjavik University, Iceland; University of Malta, Malta; University of Kiel, Germany; University of Liverpool, UK)
Publisher's Version
|
| |
Aguirre, Alejandro |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Formal Verification of Higher-Order ..."
Formal Verification of Higher-Order Probabilistic Programs: Reasoning about Approximation, Convergence, Bayesian Inference, and Optimization
Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Justin Hsu
(SUNY Buffalo, USA; IMDEA Software Institute, Spain; MPI-SWS, Germany; University of Wisconsin-Madison, USA)
Publisher's Version
|
| |
Ahmed, Amal |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Gradual Type Theory ..."
Gradual Type Theory
Max S. New, Daniel R. Licata, and Amal Ahmed
(Northeastern University, USA; Wesleyan University, USA; Inria, France)
Publisher's Version
|
| |
Albarghouthi, Aws |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Trace Abstraction Modulo Probability ..."
Trace Abstraction Modulo Probability
Calvin Smith, Justin Hsu, and Aws Albarghouthi
(University of Wisconsin-Madison, USA)
Publisher's Version
|
| |
Ali, Karim |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Context-, Flow-, and Field-Sensitive ..."
Context-, Flow-, and Field-Sensitive Data-Flow Analysis using Synchronized Pushdown Systems
Johannes Späth, Karim Ali, and Eric Bodden
(Fraunhofer IEM, Germany; University of Alberta, Canada; University of Paderborn, Germany)
Publisher's Version
 Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Alon, Uri |
Proc. ACM Program. Lang., vol. 3, issue POPL: "code2vec: Learning Distributed ..."
code2vec: Learning Distributed Representations of Code
Uri Alon, Meital Zilberstein, Omer Levy, and Eran Yahav
(Technion, Israel; Facebook AI Research, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Altenkirch, Thorsten |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Constructing Quotient Inductive-Inductive ..."
Constructing Quotient Inductive-Inductive Types
Ambrus Kaposi, András Kovács, and Thorsten Altenkirch
(Eötvös Loránd University, Hungary; University of Nottingham, UK)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Alur, Rajeev |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Modular Quantitative Monitoring ..."
Modular Quantitative Monitoring
Rajeev Alur, Konstantinos Mamouras, and Caleb Stanford
(University of Pennsylvania, USA; Rice University, USA)
Publisher's Version
|
| |
Andreescu, Oana F. |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Inferring Frame Conditions ..."
Inferring Frame Conditions with Static Correlation Analysis
Oana F. Andreescu, Thomas Jensen, Stéphane Lescuyer, and Benoît Montagu
(Internet of Trust, France; Inria, France; Prove & Run, France)
Publisher's Version
Artifacts Functional
|
| |
Armstrong, Alasdair |
Proc. ACM Program. Lang., vol. 3, issue POPL: "ISA Semantics for ARMv8-A, ..."
ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter Sewell
(University of Cambridge, UK; University of Edinburgh, UK; ARM, UK; SRI International, USA)
Publisher's Version
Artifacts Functional
|
| |
Bae, Kyungmin
|
Proc. ACM Program. Lang., vol. 3, issue POPL: "Bounded Model Checking of ..."
Bounded Model Checking of Signal Temporal Logic Properties using Syntactic Separation
Kyungmin Bae and Jia Lee
(POSTECH, South Korea)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Bakst, Alexander |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Pretend Synchrony: Synchronous ..."
Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs
Klaus v. Gleissenthall, Rami Gökhan Kıcı, Alexander Bakst, Deian Stefan, and Ranjit Jhala
(University of California at San Diego, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Baldan, Paolo |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Fixpoint Games on Continuous ..."
Fixpoint Games on Continuous Lattices
Paolo Baldan, Barbara König, Christina Mika-Michalski, and Tommaso Padoan
(University of Padua, Italy; University of Duisburg-Essen, Germany)
Publisher's Version
|
| |
Barthe, Gilles |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Formal Verification of Higher-Order ..."
Formal Verification of Higher-Order Probabilistic Programs: Reasoning about Approximation, Convergence, Bayesian Inference, and Optimization
Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Justin Hsu
(SUNY Buffalo, USA; IMDEA Software Institute, Spain; MPI-SWS, Germany; University of Wisconsin-Madison, USA)
Publisher's Version
|
| |
Batz, Kevin |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Quantitative Separation Logic: ..."
Quantitative Separation Logic: A Logic for Reasoning about Probabilistic Pointer Programs
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll
(RWTH Aachen University, Germany)
Publisher's Version
|
| |
Bauereiss, Thomas |
Proc. ACM Program. Lang., vol. 3, issue POPL: "ISA Semantics for ARMv8-A, ..."
ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter Sewell
(University of Cambridge, UK; University of Edinburgh, UK; ARM, UK; SRI International, USA)
Publisher's Version
Artifacts Functional
|
| |
Biernacki, Dariusz |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Abstracting Algebraic Effects ..."
Abstracting Algebraic Effects
Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski
(University of Wrocław, Poland)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Birkedal, Lars |
Proc. ACM Program. Lang., vol. 3, issue POPL: "StkTokens: Enforcing Well-Bracketed ..."
StkTokens: Enforcing Well-Bracketed Control Flow and Stack Encapsulation Using Linear Capabilities
Lau Skorstengaard, Dominique Devriese, and Lars Birkedal
(Aarhus University, Denmark; Vrije Universiteit Brussel, Belgium)
Publisher's Version
Proc. ACM Program. Lang., vol. 3, issue POPL: "Iron: Managing Obligations ..."
Iron: Managing Obligations in Higher-Order Concurrent Separation Logic
Aleš Bizjak, Daniel Gratzer, Robbert Krebbers, and Lars Birkedal
(Aarhus University, Denmark; Delft University of Technology, Netherlands)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Bizjak, Aleš |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Iron: Managing Obligations ..."
Iron: Managing Obligations in Higher-Order Concurrent Separation Logic
Aleš Bizjak, Daniel Gratzer, Robbert Krebbers, and Lars Birkedal
(Aarhus University, Denmark; Delft University of Technology, Netherlands)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Blanchette, Jasmin Christian |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Bindings as Bounded Natural ..."
Bindings as Bounded Natural Functors
Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, and Dmitriy Traytel
(Vrije Universiteit Amsterdam, Netherlands; Max Planck Institute for Informatics, Germany; Middlesex University, UK; Institute of Mathematics at Romanian Academy, Romania; ETH Zurich, Switzerland)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Bodden, Eric |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Context-, Flow-, and Field-Sensitive ..."
Context-, Flow-, and Field-Sensitive Data-Flow Analysis using Synchronized Pushdown Systems
Johannes Späth, Karim Ali, and Eric Bodden
(Fraunhofer IEM, Germany; University of Alberta, Canada; University of Paderborn, Germany)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Bodin, Martin |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Skeletal Semantics and Their ..."
Skeletal Semantics and Their Interpretations
Martin Bodin, Philippa Gardner, Thomas Jensen, and Alan Schmitt
(Imperial College London, UK; Inria, France)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Bonchi, Filippo |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Diagrammatic Algebra: From ..."
Diagrammatic Algebra: From Linear to Concurrent Systems
Filippo Bonchi, Joshua Holland, Robin Piedeleu, Paweł Sobociński, and Fabio Zanasi
(University of Pisa, Italy; University of Southampton, UK; University of Oxford, UK; University College London, UK)
Publisher's Version
|
| |
Breck, Jason |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Refinement of Path Expressions ..."
Refinement of Path Expressions for Static Analysis
John Cyphert, Jason Breck, Zachary Kincaid, and Thomas Reps
(University of Wisconsin, USA; Princeton University, USA; GrammaTech, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Proc. ACM Program. Lang., vol. 3, issue POPL: "Closed Forms for Numerical ..."
Closed Forms for Numerical Loops
Zachary Kincaid, Jason Breck, John Cyphert, and Thomas Reps
(Princeton University, USA; University of Wisconsin, USA; GrammaTech, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Campbell, Brian
|
Proc. ACM Program. Lang., vol. 3, issue POPL: "ISA Semantics for ARMv8-A, ..."
ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter Sewell
(University of Cambridge, UK; University of Edinburgh, UK; ARM, UK; SRI International, USA)
Publisher's Version
Artifacts Functional
|
| |
Castagna, Giuseppe |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Gradual Typing: A New Perspective ..."
Gradual Typing: A New Perspective
Giuseppe Castagna, Victor Lanvin, Tommaso Petrucciani, and Jeremy G. Siek
(CNRS, France; University of Paris Diderot, France; University of Genoa, Italy; Indiana University, USA)
Publisher's Version
|
| |
Castellan, Simon |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Two Sides of the Same Coin: ..."
Two Sides of the Same Coin: Session Types and Game Semantics: A Synchronous Side and an Asynchronous Side
Simon Castellan and Nobuko Yoshida
(Imperial College London, UK)
Publisher's Version
|
| |
Castro, David |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Distributed Programming using ..."
Distributed Programming using Role-Parametric Session Types in Go: Statically-Typed Endpoint APIs for Dynamically-Instantiated Communication Structures
David Castro, Raymond Hu, Sung-Shik Jongmans, Nicholas Ng, and Nobuko Yoshida
(Imperial College London, UK; Open University of the Netherlands, Netherlands)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Cauligi, Sunjay |
Proc. ACM Program. Lang., vol. 3, issue POPL: "CT-Wasm: Type-Driven Secure ..."
CT-Wasm: Type-Driven Secure Cryptography for the Web Ecosystem
Conrad Watt, John Renner, Natalie Popescu, Sunjay Cauligi, and Deian Stefan
(University of Cambridge, UK; University of California at San Diego, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Cavallo, Evan |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Higher Inductive Types in ..."
Higher Inductive Types in Cubical Computational Type Theory
Evan Cavallo and Robert Harper
(Carnegie Mellon University, USA)
Publisher's Version
|
| |
Chakraborty, Soham |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Grounding Thin-Air Reads with ..."
Grounding Thin-Air Reads with Event Structures
Soham Chakraborty and Viktor Vafeiadis
(MPI-SWS, Germany)
Publisher's Version
|
| |
Chatterjee, Krishnendu |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Efficient Parameterized Algorithms ..."
Efficient Parameterized Algorithms for Data Packing
Krishnendu Chatterjee, Amir Kafshdar Goharshady, Nastaran Okati, and Andreas Pavlogiannis
(IST Austria, Austria; Ferdowsi University of Mashhad, Iran; EPFL, Switzerland)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Chen, Liqian |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Efficient Automated Repair ..."
Efficient Automated Repair of High Floating-Point Errors in Numerical Libraries
Xin Yi, Liqian Chen, Xiaoguang Mao, and Tao Ji
(National University of Defense Technology, China)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Chen, Taolue |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Decision Procedures for Path ..."
Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations
Taolue Chen, Matthew Hague, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu
(Birkbeck University of London, UK; Royal Holloway University of London, UK; University of Oxford, UK; Uppsala University, Sweden; Institute of Software at Chinese Academy of Sciences, China)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Chugh, Ravi |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Live Functional Programming ..."
Live Functional Programming with Typed Holes
Cyrus Omar, Ian Voysey, Ravi Chugh, and Matthew A. Hammer
(University of Chicago, USA; Carnegie Mellon University, USA; University of Colorado Boulder, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Clairambault, Pierre |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Game Semantics for Quantum ..."
Game Semantics for Quantum Programming
Pierre Clairambault, Marc De Visme, and Glynn Winskel
(University of Lyon, France; CNRS, France; ENS Lyon, France; University of Cambridge, UK)
Publisher's Version
|
| |
Cockx, Jesper |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Definitional Proof-Irrelevance ..."
Definitional Proof-Irrelevance without K
Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau
(Inria, France; Chalmers University of Technology, Sweden; University of Gothenburg, Sweden; IRIF, France)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Cousot, Patrick |
Proc. ACM Program. Lang., vol. 3, issue POPL: "A²I: Abstract² Interpretation ..."
A²I: Abstract² Interpretation
Patrick Cousot, Roberto Giacobazzi, and Francesco Ranzato
(New York University, USA; University of Verona, Italy; IMDEA Software Institute, Spain; University of Padua, Italy)
Publisher's Version
|
| |
Crary, Karl |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Fully Abstract Module Compilation ..."
Fully Abstract Module Compilation
Karl Crary
(Carnegie Mellon University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Cusumano-Towner, Marco F. |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Bayesian Synthesis of Probabilistic ..."
Bayesian Synthesis of Probabilistic Programs for Automatic Data Modeling
Feras A. Saad, Marco F. Cusumano-Towner, Ulrich Schaechtle, Martin C. Rinard, and Vikash K. Mansinghka
(Massachusetts Institute of Technology, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Cyphert, John |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Refinement of Path Expressions ..."
Refinement of Path Expressions for Static Analysis
John Cyphert, Jason Breck, Zachary Kincaid, and Thomas Reps
(University of Wisconsin, USA; Princeton University, USA; GrammaTech, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Proc. ACM Program. Lang., vol. 3, issue POPL: "Closed Forms for Numerical ..."
Closed Forms for Numerical Loops
Zachary Kincaid, Jason Breck, John Cyphert, and Thomas Reps
(Princeton University, USA; University of Wisconsin, USA; GrammaTech, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Dal Lago, Ugo
|
Proc. ACM Program. Lang., vol. 3, issue POPL: "Intersection Types and Runtime ..."
Intersection Types and Runtime Errors in the Pi-Calculus
Ugo Dal Lago, Marc de Visme, Damiano Mazza, and Akira Yoshimizu
(University of Bologna, Italy; Inria, France; University of Lyon, France; ENS Lyon, France; CNRS, France; University of Paris 13, France)
Publisher's Version
|
| |
Davis, Brooks |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Exploring C Semantics and ..."
Exploring C Semantics and Pointer Provenance
Kayvan Memarian, Victor B. F. Gomes, Brooks Davis, Stephen Kell, Alexander Richardson, Robert N. M. Watson, and Peter Sewell
(University of Cambridge, UK; SRI International, USA)
Publisher's Version
|
| |
Decova, Sára |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Exceptional Asynchronous Session ..."
Exceptional Asynchronous Session Types: Session Types without Tiers
Simon Fowler, Sam Lindley, J. Garrett Morris, and Sára Decova
(University of Edinburgh, UK; University of Kansas, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
De Visme, Marc |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Game Semantics for Quantum ..."
Game Semantics for Quantum Programming
Pierre Clairambault, Marc De Visme, and Glynn Winskel
(University of Lyon, France; CNRS, France; ENS Lyon, France; University of Cambridge, UK)
Publisher's Version
Proc. ACM Program. Lang., vol. 3, issue POPL: "Intersection Types and Runtime ..."
Intersection Types and Runtime Errors in the Pi-Calculus
Ugo Dal Lago, Marc de Visme, Damiano Mazza, and Akira Yoshimizu
(University of Bologna, Italy; Inria, France; University of Lyon, France; ENS Lyon, France; CNRS, France; University of Paris 13, France)
Publisher's Version
|
| |
Devriese, Dominique |
Proc. ACM Program. Lang., vol. 3, issue POPL: "StkTokens: Enforcing Well-Bracketed ..."
StkTokens: Enforcing Well-Bracketed Control Flow and Stack Encapsulation Using Linear Capabilities
Lau Skorstengaard, Dominique Devriese, and Lars Birkedal
(Aarhus University, Denmark; Vrije Universiteit Brussel, Belgium)
Publisher's Version
|
| |
Doko, Marko |
Proc. ACM Program. Lang., vol. 3, issue POPL: "On Library Correctness under ..."
On Library Correctness under Weak Memory Consistency: Specifying and Verifying Concurrent Libraries under Declarative Consistency Models
Azalea Raad, Marko Doko, Lovro Rožić, Ori Lahav, and Viktor Vafeiadis
(MPI-SWS, Germany; Tel Aviv University, Israel)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Dudenhefner, Andrej |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Principality and Approximation ..."
Principality and Approximation under Dimensional Bound
Andrej Dudenhefner and Jakob Rehof
(TU Dortmund, Germany)
Publisher's Version
|
| |
Dunfield, Joshua |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Sound and Complete Bidirectional ..."
Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism with Existentials and Indexed Types
Joshua Dunfield and Neelakantan R. Krishnaswami
(Queen's University, Canada; University of Cambridge, UK)
Publisher's Version
|
| |
Emmi, Michael
|
Proc. ACM Program. Lang., vol. 3, issue POPL: "Weak-Consistency Specification ..."
Weak-Consistency Specification via Visibility Relaxation
Michael Emmi and Constantin Enea
(SRI International, USA; IRIF, France; University of Paris Diderot, France; CNRS, France)
Publisher's Version
|
| |
Enea, Constantin |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Weak-Consistency Specification ..."
Weak-Consistency Specification via Visibility Relaxation
Michael Emmi and Constantin Enea
(SRI International, USA; IRIF, France; University of Paris Diderot, France; CNRS, France)
Publisher's Version
|
| |
Findler, Robert Bruce
|
Proc. ACM Program. Lang., vol. 3, issue POPL: "A Calculus for Esterel: If ..."
A Calculus for Esterel: If can, can. If no can, no can.
Spencer P. Florence, Shu-Hung You, Jesse A. Tov, and Robert Bruce Findler
(Northwestern University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Florence, Spencer P. |
Proc. ACM Program. Lang., vol. 3, issue POPL: "A Calculus for Esterel: If ..."
A Calculus for Esterel: If can, can. If no can, no can.
Spencer P. Florence, Shu-Hung You, Jesse A. Tov, and Robert Bruce Findler
(Northwestern University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Flur, Shaked |
Proc. ACM Program. Lang., vol. 3, issue POPL: "ISA Semantics for ARMv8-A, ..."
ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter Sewell
(University of Cambridge, UK; University of Edinburgh, UK; ARM, UK; SRI International, USA)
Publisher's Version
Artifacts Functional
|
| |
Fowler, Simon |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Exceptional Asynchronous Session ..."
Exceptional Asynchronous Session Types: Session Types without Tiers
Simon Fowler, Sam Lindley, J. Garrett Morris, and Sára Decova
(University of Edinburgh, UK; University of Kansas, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Fragoso Santos, José |
Proc. ACM Program. Lang., vol. 3, issue POPL: "JaVerT 2.0: Compositional ..."
JaVerT 2.0: Compositional Symbolic Execution for JavaScript
José Fragoso Santos, Petar Maksimović, Gabriela Sampaio, and Philippa Gardner
(Imperial College London, UK; Mathematical Institute SASA, Serbia)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Francalanza, Adrian |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Adventures in Monitorability: ..."
Adventures in Monitorability: From Branching to Linear Time and Back Again
Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen
(Gran Sasso Science Institute, Iceland; Reykjavik University, Iceland; University of Malta, Malta; University of Kiel, Germany; University of Liverpool, UK)
Publisher's Version
|
| |
French, Jon |
Proc. ACM Program. Lang., vol. 3, issue POPL: "ISA Semantics for ARMv8-A, ..."
ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter Sewell
(University of Cambridge, UK; University of Edinburgh, UK; ARM, UK; SRI International, USA)
Publisher's Version
Artifacts Functional
|
| |
Fromherz, Aymeric |
Proc. ACM Program. Lang., vol. 3, issue POPL: "A Verified, Efficient Embedding ..."
A Verified, Efficient Embedding of a Verifiable Assembly Language
Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, and Nikhil Swamy
(Carnegie Mellon University, USA; Princeton University, USA; Microsoft Research, USA; Microsoft Research, India)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Gaboardi, Marco
|
Proc. ACM Program. Lang., vol. 3, issue POPL: "Formal Verification of Higher-Order ..."
Formal Verification of Higher-Order Probabilistic Programs: Reasoning about Approximation, Convergence, Bayesian Inference, and Optimization
Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Justin Hsu
(SUNY Buffalo, USA; IMDEA Software Institute, Spain; MPI-SWS, Germany; University of Wisconsin-Madison, USA)
Publisher's Version
|
| |
Gardner, Philippa |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Skeletal Semantics and Their ..."
Skeletal Semantics and Their Interpretations
Martin Bodin, Philippa Gardner, Thomas Jensen, and Alan Schmitt
(Imperial College London, UK; Inria, France)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Proc. ACM Program. Lang., vol. 3, issue POPL: "JaVerT 2.0: Compositional ..."
JaVerT 2.0: Compositional Symbolic Execution for JavaScript
José Fragoso Santos, Petar Maksimović, Gabriela Sampaio, and Philippa Gardner
(Imperial College London, UK; Mathematical Institute SASA, Serbia)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Garg, Deepak |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Formal Verification of Higher-Order ..."
Formal Verification of Higher-Order Probabilistic Programs: Reasoning about Approximation, Convergence, Bayesian Inference, and Optimization
Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Justin Hsu
(SUNY Buffalo, USA; IMDEA Software Institute, Spain; MPI-SWS, Germany; University of Wisconsin-Madison, USA)
Publisher's Version
Proc. ACM Program. Lang., vol. 3, issue POPL: "From Fine- to Coarse-Grained ..."
From Fine- to Coarse-Grained Dynamic Information Flow Control and Back
Marco Vassena, Alejandro Russo, Deepak Garg, Vineet Rajani, and Deian Stefan
(Chalmers University of Technology, Sweden; MPI-SWS, Germany; University of California at San Diego, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Gehr, Timon |
Proc. ACM Program. Lang., vol. 3, issue POPL: "An Abstract Domain for Certifying ..."
An Abstract Domain for Certifying Neural Networks
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev
(ETH Zurich, Switzerland)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Gheri, Lorenzo |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Bindings as Bounded Natural ..."
Bindings as Bounded Natural Functors
Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, and Dmitriy Traytel
(Vrije Universiteit Amsterdam, Netherlands; Max Planck Institute for Informatics, Germany; Middlesex University, UK; Institute of Mathematics at Romanian Academy, Romania; ETH Zurich, Switzerland)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Giacobazzi, Roberto |
Proc. ACM Program. Lang., vol. 3, issue POPL: "A²I: Abstract² Interpretation ..."
A²I: Abstract² Interpretation
Patrick Cousot, Roberto Giacobazzi, and Francesco Ranzato
(New York University, USA; University of Verona, Italy; IMDEA Software Institute, Spain; University of Padua, Italy)
Publisher's Version
|
| |
Giannarakis, Nick |
Proc. ACM Program. Lang., vol. 3, issue POPL: "A Verified, Efficient Embedding ..."
A Verified, Efficient Embedding of a Verifiable Assembly Language
Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, and Nikhil Swamy
(Carnegie Mellon University, USA; Princeton University, USA; Microsoft Research, USA; Microsoft Research, India)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Gilbert, Gaëtan |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Definitional Proof-Irrelevance ..."
Definitional Proof-Irrelevance without K
Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau
(Inria, France; Chalmers University of Technology, Sweden; University of Gothenburg, Sweden; IRIF, France)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Goharshady, Amir Kafshdar |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Efficient Parameterized Algorithms ..."
Efficient Parameterized Algorithms for Data Packing
Krishnendu Chatterjee, Amir Kafshdar Goharshady, Nastaran Okati, and Andreas Pavlogiannis
(IST Austria, Austria; Ferdowsi University of Mashhad, Iran; EPFL, Switzerland)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Gomes, Victor B. F. |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Exploring C Semantics and ..."
Exploring C Semantics and Pointer Provenance
Kayvan Memarian, Victor B. F. Gomes, Brooks Davis, Stephen Kell, Alexander Richardson, Robert N. M. Watson, and Peter Sewell
(University of Cambridge, UK; SRI International, USA)
Publisher's Version
|
| |
Gordon, Andrew D. |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Probabilistic Programming ..."
Probabilistic Programming with Densities in SlicStan: Efficient, Flexible, and Deterministic
Maria I. Gorinova, Andrew D. Gordon, and Charles Sutton
(University of Edinburgh, UK; Microsoft Research, UK; Google Brain, USA)
Publisher's Version
|
| |
Gorinova, Maria I. |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Probabilistic Programming ..."
Probabilistic Programming with Densities in SlicStan: Efficient, Flexible, and Deterministic
Maria I. Gorinova, Andrew D. Gordon, and Charles Sutton
(University of Edinburgh, UK; Microsoft Research, UK; Google Brain, USA)
Publisher's Version
|
| |
Gorogiannis, Nikos |
Proc. ACM Program. Lang., vol. 3, issue POPL: "A True Positives Theorem for ..."
A True Positives Theorem for a Static Race Detector
Nikos Gorogiannis, Peter W. O'Hearn, and Ilya Sergey
(Facebook, UK; Middlesex University, UK; University College London, UK; Yale-NUS College, Singapore; National University of Singapore, Singapore)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Gratzer, Daniel |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Iron: Managing Obligations ..."
Iron: Managing Obligations in Higher-Order Concurrent Separation Logic
Aleš Bizjak, Daniel Gratzer, Robbert Krebbers, and Lars Birkedal
(Aarhus University, Denmark; Delft University of Technology, Netherlands)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Gray, Kathryn E. |
Proc. ACM Program. Lang., vol. 3, issue POPL: "ISA Semantics for ARMv8-A, ..."
ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter Sewell
(University of Cambridge, UK; University of Edinburgh, UK; ARM, UK; SRI International, USA)
Publisher's Version
Artifacts Functional
|
| |
Grossman, Dan |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Concerto: A Framework for ..."
Concerto: A Framework for Combined Concrete and Abstract Interpretation
John Toman and Dan Grossman
(University of Washington, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Hague, Matthew
|
Proc. ACM Program. Lang., vol. 3, issue POPL: "Decision Procedures for Path ..."
Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations
Taolue Chen, Matthew Hague, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu
(Birkbeck University of London, UK; Royal Holloway University of London, UK; University of Oxford, UK; Uppsala University, Sweden; Institute of Software at Chinese Academy of Sciences, China)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Hammer, Matthew A. |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Live Functional Programming ..."
Live Functional Programming with Typed Holes
Cyrus Omar, Ian Voysey, Ravi Chugh, and Matthew A. Hammer
(University of Chicago, USA; Carnegie Mellon University, USA; University of Colorado Boulder, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Harper, Robert |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Higher Inductive Types in ..."
Higher Inductive Types in Cubical Computational Type Theory
Evan Cavallo and Robert Harper
(Carnegie Mellon University, USA)
Publisher's Version
Proc. ACM Program. Lang., vol. 3, issue POPL: "A Separation Logic for Concurrent ..."
A Separation Logic for Concurrent Randomized Programs
Joseph Tassarotti and Robert Harper
(Carnegie Mellon University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Hawblitzel, Chris |
Proc. ACM Program. Lang., vol. 3, issue POPL: "A Verified, Efficient Embedding ..."
A Verified, Efficient Embedding of a Verifiable Assembly Language
Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, and Nikhil Swamy
(Carnegie Mellon University, USA; Princeton University, USA; Microsoft Research, USA; Microsoft Research, India)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Hicks, Michael |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Quantitative Robustness Analysis ..."
Quantitative Robustness Analysis of Quantum Programs
Shih-Han Hung, Kesha Hietala, Shaopeng Zhu, Mingsheng Ying, Michael Hicks, and Xiaodi Wu
(University of Maryland, USA; University of Technology Sydney, Australia; Institute of Software at Chinese Academy of Sciences, China; Tsinghua University, China)
Publisher's Version
Proc. ACM Program. Lang., vol. 3, issue POPL: "LWeb: Information Flow Security ..."
LWeb: Information Flow Security for Multi-tier Web Applications
James Parker, Niki Vazou, and Michael Hicks
(University of Maryland, USA; IMDEA Software Institute, Spain)
Publisher's Version
|
| |
Hietala, Kesha |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Quantitative Robustness Analysis ..."
Quantitative Robustness Analysis of Quantum Programs
Shih-Han Hung, Kesha Hietala, Shaopeng Zhu, Mingsheng Ying, Michael Hicks, and Xiaodi Wu
(University of Maryland, USA; University of Technology Sydney, Australia; Institute of Software at Chinese Academy of Sciences, China; Tsinghua University, China)
Publisher's Version
|
| |
Hirschowitz, Tom |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Familial Monads and Structural ..."
Familial Monads and Structural Operational Semantics
Tom Hirschowitz
(Grenoble Alps University, France; Savoie Mont Blanc University, France; CNRS, France; LAMA, France)
Publisher's Version
|
| |
Hoffmann, Jan |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Type-Guided Worst-Case Input ..."
Type-Guided Worst-Case Input Generation
Di Wang and Jan Hoffmann
(Carnegie Mellon University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Holland, Joshua |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Diagrammatic Algebra: From ..."
Diagrammatic Algebra: From Linear to Concurrent Systems
Filippo Bonchi, Joshua Holland, Robin Piedeleu, Paweł Sobociński, and Fabio Zanasi
(University of Pisa, Italy; University of Southampton, UK; University of Oxford, UK; University College London, UK)
Publisher's Version
|
| |
Hong, Jaemin |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Polymorphic Symmetric Multiple ..."
Polymorphic Symmetric Multiple Dispatch with Variance
Gyunghee Park, Jaemin Hong, Guy L. Steele Jr., and Sukyoung Ryu
(KAIST, South Korea; Oracle Labs, USA)
Publisher's Version
|
| |
Houshmand, Farzin |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Hamsaz: Replication Coordination ..."
Hamsaz: Replication Coordination Analysis and Synthesis
Farzin Houshmand and Mohsen Lesani
(University of California at Riverside, USA)
Publisher's Version
|
| |
Hsu, Justin |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Formal Verification of Higher-Order ..."
Formal Verification of Higher-Order Probabilistic Programs: Reasoning about Approximation, Convergence, Bayesian Inference, and Optimization
Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Justin Hsu
(SUNY Buffalo, USA; IMDEA Software Institute, Spain; MPI-SWS, Germany; University of Wisconsin-Madison, USA)
Publisher's Version
Proc. ACM Program. Lang., vol. 3, issue POPL: "Trace Abstraction Modulo Probability ..."
Trace Abstraction Modulo Probability
Calvin Smith, Justin Hsu, and Aws Albarghouthi
(University of Wisconsin-Madison, USA)
Publisher's Version
|
| |
Hu, Raymond |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Distributed Programming using ..."
Distributed Programming using Role-Parametric Session Types in Go: Statically-Typed Endpoint APIs for Dynamically-Instantiated Communication Structures
David Castro, Raymond Hu, Sung-Shik Jongmans, Nicholas Ng, and Nobuko Yoshida
(Imperial College London, UK; Open University of the Netherlands, Netherlands)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Hung, Shih-Han |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Quantitative Robustness Analysis ..."
Quantitative Robustness Analysis of Quantum Programs
Shih-Han Hung, Kesha Hietala, Shaopeng Zhu, Mingsheng Ying, Michael Hicks, and Xiaodi Wu
(University of Maryland, USA; University of Technology Sydney, Australia; Institute of Software at Chinese Academy of Sciences, China; Tsinghua University, China)
Publisher's Version
|
| |
Igarashi, Atsushi
|
Proc. ACM Program. Lang., vol. 3, issue POPL: "Dynamic Type Inference for ..."
Dynamic Type Inference for Gradual Hindley–Milner Typing
Yusuke Miyazaki, Taro Sekiyama, and Atsushi Igarashi
(Kyoto University, Japan; National Institute of Informatics, Japan)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Ingólfsdóttir, Anna |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Adventures in Monitorability: ..."
Adventures in Monitorability: From Branching to Linear Time and Back Again
Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen
(Gran Sasso Science Institute, Iceland; Reykjavik University, Iceland; University of Malta, Malta; University of Kiel, Germany; University of Liverpool, UK)
Publisher's Version
|
| |
Jensen, Thomas
|
Proc. ACM Program. Lang., vol. 3, issue POPL: "Skeletal Semantics and Their ..."
Skeletal Semantics and Their Interpretations
Martin Bodin, Philippa Gardner, Thomas Jensen, and Alan Schmitt
(Imperial College London, UK; Inria, France)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Proc. ACM Program. Lang., vol. 3, issue POPL: "Inferring Frame Conditions ..."
Inferring Frame Conditions with Static Correlation Analysis
Oana F. Andreescu, Thomas Jensen, Stéphane Lescuyer, and Benoît Montagu
(Internet of Trust, France; Inria, France; Prove & Run, France)
Publisher's Version
Artifacts Functional
|
| |
Jhala, Ranjit |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Pretend Synchrony: Synchronous ..."
Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs
Klaus v. Gleissenthall, Rami Gökhan Kıcı, Alexander Bakst, Deian Stefan, and Ranjit Jhala
(University of California at San Diego, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Ji, Tao |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Efficient Automated Repair ..."
Efficient Automated Repair of High Floating-Point Errors in Numerical Libraries
Xin Yi, Liqian Chen, Xiaoguang Mao, and Tao Ji
(National University of Defense Technology, China)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Jongmans, Sung-Shik |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Distributed Programming using ..."
Distributed Programming using Role-Parametric Session Types in Go: Statically-Typed Endpoint APIs for Dynamically-Instantiated Communication Structures
David Castro, Raymond Hu, Sung-Shik Jongmans, Nicholas Ng, and Nobuko Yoshida
(Imperial College London, UK; Open University of the Netherlands, Netherlands)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Kaminski, Benjamin Lucien
|
Proc. ACM Program. Lang., vol. 3, issue POPL: "Quantitative Separation Logic: ..."
Quantitative Separation Logic: A Logic for Reasoning about Probabilistic Pointer Programs
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll
(RWTH Aachen University, Germany)
Publisher's Version
|
| |
Kammar, Ohad |
Proc. ACM Program. Lang., vol. 3, issue POPL: "A Domain Theory for Statistical ..."
A Domain Theory for Statistical Probabilistic Programming
Matthijs Vákár, Ohad Kammar, and Sam Staton
(Columbia University, USA; University of Oxford, UK)
Publisher's Version
|
| |
Kaposi, Ambrus |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Constructing Quotient Inductive-Inductive ..."
Constructing Quotient Inductive-Inductive Types
Ambrus Kaposi, András Kovács, and Thorsten Altenkirch
(Eötvös Loránd University, Hungary; University of Nottingham, UK)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Katoen, Joost-Pieter |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Quantitative Separation Logic: ..."
Quantitative Separation Logic: A Logic for Reasoning about Probabilistic Pointer Programs
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll
(RWTH Aachen University, Germany)
Publisher's Version
|
| |
Kavvos, G. A. |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Modalities, Cohesion, and ..."
Modalities, Cohesion, and Information Flow
G. A. Kavvos
(Wesleyan University, USA)
Publisher's Version
|
| |
Kell, Stephen |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Exploring C Semantics and ..."
Exploring C Semantics and Pointer Provenance
Kayvan Memarian, Victor B. F. Gomes, Brooks Davis, Stephen Kell, Alexander Richardson, Robert N. M. Watson, and Peter Sewell
(University of Cambridge, UK; SRI International, USA)
Publisher's Version
|
| |
Kıcı, Rami Gökhan |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Pretend Synchrony: Synchronous ..."
Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs
Klaus v. Gleissenthall, Rami Gökhan Kıcı, Alexander Bakst, Deian Stefan, and Ranjit Jhala
(University of California at San Diego, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Kincaid, Zachary |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Refinement of Path Expressions ..."
Refinement of Path Expressions for Static Analysis
John Cyphert, Jason Breck, Zachary Kincaid, and Thomas Reps
(University of Wisconsin, USA; Princeton University, USA; GrammaTech, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Proc. ACM Program. Lang., vol. 3, issue POPL: "Closed Forms for Numerical ..."
Closed Forms for Numerical Loops
Zachary Kincaid, Jason Breck, John Cyphert, and Thomas Reps
(Princeton University, USA; University of Wisconsin, USA; GrammaTech, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Kokke, Wen |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Better Late Than Never: A ..."
Better Late Than Never: A Fully-Abstract Semantics for Classical Processes
Wen Kokke, Fabrizio Montesi, and Marco Peressotti
(University of Edinburgh, UK; University of Southern Denmark, Denmark)
Publisher's Version
|
| |
König, Barbara |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Fixpoint Games on Continuous ..."
Fixpoint Games on Continuous Lattices
Paolo Baldan, Barbara König, Christina Mika-Michalski, and Tommaso Padoan
(University of Padua, Italy; University of Duisburg-Essen, Germany)
Publisher's Version
|
| |
Kovács, András |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Constructing Quotient Inductive-Inductive ..."
Constructing Quotient Inductive-Inductive Types
Ambrus Kaposi, András Kovács, and Thorsten Altenkirch
(Eötvös Loránd University, Hungary; University of Nottingham, UK)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Krebbers, Robbert |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Iron: Managing Obligations ..."
Iron: Managing Obligations in Higher-Order Concurrent Separation Logic
Aleš Bizjak, Daniel Gratzer, Robbert Krebbers, and Lars Birkedal
(Aarhus University, Denmark; Delft University of Technology, Netherlands)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Krishnaswami, Neel |
Proc. ACM Program. Lang., vol. 3, issue POPL: "ISA Semantics for ARMv8-A, ..."
ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter Sewell
(University of Cambridge, UK; University of Edinburgh, UK; ARM, UK; SRI International, USA)
Publisher's Version
Artifacts Functional
|
| |
Krishnaswami, Neelakantan R. |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Sound and Complete Bidirectional ..."
Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism with Existentials and Indexed Types
Joshua Dunfield and Neelakantan R. Krishnaswami
(Queen's University, Canada; University of Cambridge, UK)
Publisher's Version
|
| |
Labrada, Elizabeth
|
Proc. ACM Program. Lang., vol. 3, issue POPL: "Gradual Parametricity, Revisited ..."
Gradual Parametricity, Revisited
Matías Toro, Elizabeth Labrada, and Éric Tanter
(University of Chile, Chile; Inria, France)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Lahav, Ori |
Proc. ACM Program. Lang., vol. 3, issue POPL: "On Library Correctness under ..."
On Library Correctness under Weak Memory Consistency: Specifying and Verifying Concurrent Libraries under Declarative Consistency Models
Azalea Raad, Marko Doko, Lovro Rožić, Ori Lahav, and Viktor Vafeiadis
(MPI-SWS, Germany; Tel Aviv University, Israel)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Proc. ACM Program. Lang., vol. 3, issue POPL: "Bridging the Gap between Programming ..."
Bridging the Gap between Programming Languages and Hardware Weak Memory Models
Anton Podkopaev, Ori Lahav, and Viktor Vafeiadis
(St. Petersburg University, Russia; JetBrains Research, Russia; MPI-SWS, Germany; Tel Aviv University, Israel)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Lanvin, Victor |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Gradual Typing: A New Perspective ..."
Gradual Typing: A New Perspective
Giuseppe Castagna, Victor Lanvin, Tommaso Petrucciani, and Jeremy G. Siek
(CNRS, France; University of Paris Diderot, France; University of Genoa, Italy; Indiana University, USA)
Publisher's Version
|
| |
Lee, Jia |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Bounded Model Checking of ..."
Bounded Model Checking of Signal Temporal Logic Properties using Syntactic Separation
Kyungmin Bae and Jia Lee
(POSTECH, South Korea)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Lehtinen, Karoliina |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Adventures in Monitorability: ..."
Adventures in Monitorability: From Branching to Linear Time and Back Again
Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen
(Gran Sasso Science Institute, Iceland; Reykjavik University, Iceland; University of Malta, Malta; University of Kiel, Germany; University of Liverpool, UK)
Publisher's Version
|
| |
Lesani, Mohsen |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Hamsaz: Replication Coordination ..."
Hamsaz: Replication Coordination Analysis and Synthesis
Farzin Houshmand and Mohsen Lesani
(University of California at Riverside, USA)
Publisher's Version
|
| |
Lescuyer, Stéphane |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Inferring Frame Conditions ..."
Inferring Frame Conditions with Static Correlation Analysis
Oana F. Andreescu, Thomas Jensen, Stéphane Lescuyer, and Benoît Montagu
(Internet of Trust, France; Inria, France; Prove & Run, France)
Publisher's Version
Artifacts Functional
|
| |
Levy, Omer |
Proc. ACM Program. Lang., vol. 3, issue POPL: "code2vec: Learning Distributed ..."
code2vec: Learning Distributed Representations of Code
Uri Alon, Meital Zilberstein, Omer Levy, and Eran Yahav
(Technion, Israel; Facebook AI Research, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Liang, Percy |
Proc. ACM Program. Lang., vol. 3, issue POPL: "FrAngel: Component-Based Synthesis ..."
FrAngel: Component-Based Synthesis with Control Structures
Kensen Shi, Jacob Steinhardt, and Percy Liang
(Stanford University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Licata, Daniel R. |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Gradual Type Theory ..."
Gradual Type Theory
Max S. New, Daniel R. Licata, and Amal Ahmed
(Northeastern University, USA; Wesleyan University, USA; Inria, France)
Publisher's Version
|
| |
Lin, Anthony W. |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Decision Procedures for Path ..."
Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations
Taolue Chen, Matthew Hague, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu
(Birkbeck University of London, UK; Royal Holloway University of London, UK; University of Oxford, UK; Uppsala University, Sweden; Institute of Software at Chinese Academy of Sciences, China)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Lindley, Sam |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Exceptional Asynchronous Session ..."
Exceptional Asynchronous Session Types: Session Types without Tiers
Simon Fowler, Sam Lindley, J. Garrett Morris, and Sára Decova
(University of Edinburgh, UK; University of Kansas, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Madhusudan, P.
|
Proc. ACM Program. Lang., vol. 3, issue POPL: "Decidable Verification of ..."
Decidable Verification of Uninterpreted Programs
Umang Mathur, P. Madhusudan, and Mahesh Viswanathan
(University of Illinois at Urbana-Champaign, USA)
Publisher's Version
|
| |
Maïza, Claire |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Fast and Exact Analysis for ..."
Fast and Exact Analysis for LRU Caches
Valentin Touzeau, Claire Maïza, David Monniaux, and Jan Reineke
(Grenoble Alps University, France; Grenoble INP, France; CNRS, France; Saarland University, Germany)
Publisher's Version
|
| |
Maksimović, Petar |
Proc. ACM Program. Lang., vol. 3, issue POPL: "JaVerT 2.0: Compositional ..."
JaVerT 2.0: Compositional Symbolic Execution for JavaScript
José Fragoso Santos, Petar Maksimović, Gabriela Sampaio, and Philippa Gardner
(Imperial College London, UK; Mathematical Institute SASA, Serbia)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Mamouras, Konstantinos |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Modular Quantitative Monitoring ..."
Modular Quantitative Monitoring
Rajeev Alur, Konstantinos Mamouras, and Caleb Stanford
(University of Pennsylvania, USA; Rice University, USA)
Publisher's Version
|
| |
Mansinghka, Vikash K. |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Bayesian Synthesis of Probabilistic ..."
Bayesian Synthesis of Probabilistic Programs for Automatic Data Modeling
Feras A. Saad, Marco F. Cusumano-Towner, Ulrich Schaechtle, Martin C. Rinard, and Vikash K. Mansinghka
(Massachusetts Institute of Technology, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Mao, Xiaoguang |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Efficient Automated Repair ..."
Efficient Automated Repair of High Floating-Point Errors in Numerical Libraries
Xin Yi, Liqian Chen, Xiaoguang Mao, and Tao Ji
(National University of Defense Technology, China)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Matheja, Christoph |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Quantitative Separation Logic: ..."
Quantitative Separation Logic: A Logic for Reasoning about Probabilistic Pointer Programs
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll
(RWTH Aachen University, Germany)
Publisher's Version
|
| |
Mathur, Umang |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Decidable Verification of ..."
Decidable Verification of Uninterpreted Programs
Umang Mathur, P. Madhusudan, and Mahesh Viswanathan
(University of Illinois at Urbana-Champaign, USA)
Publisher's Version
|
| |
Mazza, Damiano |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Intersection Types and Runtime ..."
Intersection Types and Runtime Errors in the Pi-Calculus
Ugo Dal Lago, Marc de Visme, Damiano Mazza, and Akira Yoshimizu
(University of Bologna, Italy; Inria, France; University of Lyon, France; ENS Lyon, France; CNRS, France; University of Paris 13, France)
Publisher's Version
|
| |
McKinna, James |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Abstracting Extensible Data ..."
Abstracting Extensible Data Types: Or, Rows by Any Other Name
J. Garrett Morris and James McKinna
(University of Kansas, USA; University of Edinburgh, UK)
Publisher's Version
|
| |
Mellies, Paul-André |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Categorical Combinatorics ..."
Categorical Combinatorics of Scheduling and Synchronization in Game Semantics
Paul-André Mellies
(CNRS, France; University of Paris Diderot, France)
Publisher's Version
|
| |
Memarian, Kayvan |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Exploring C Semantics and ..."
Exploring C Semantics and Pointer Provenance
Kayvan Memarian, Victor B. F. Gomes, Brooks Davis, Stephen Kell, Alexander Richardson, Robert N. M. Watson, and Peter Sewell
(University of Cambridge, UK; SRI International, USA)
Publisher's Version
|
| |
Meyer, Roland |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Decoupling Lock-Free Data ..."
Decoupling Lock-Free Data Structures from Memory Reclamation for Static Analysis
Roland Meyer and Sebastian Wolff
(TU Braunschweig, Germany)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Mika-Michalski, Christina |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Fixpoint Games on Continuous ..."
Fixpoint Games on Continuous Lattices
Paolo Baldan, Barbara König, Christina Mika-Michalski, and Tommaso Padoan
(University of Padua, Italy; University of Duisburg-Essen, Germany)
Publisher's Version
|
| |
Miyazaki, Yusuke |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Dynamic Type Inference for ..."
Dynamic Type Inference for Gradual Hindley–Milner Typing
Yusuke Miyazaki, Taro Sekiyama, and Atsushi Igarashi
(Kyoto University, Japan; National Institute of Informatics, Japan)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Møgelberg, Rasmus Ejlers |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Bisimulation as Path Type ..."
Bisimulation as Path Type for Guarded Recursive Types
Rasmus Ejlers Møgelberg and Niccolò Veltri
(IT University of Copenhagen, Denmark)
Publisher's Version
|
| |
Monniaux, David |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Fast and Exact Analysis for ..."
Fast and Exact Analysis for LRU Caches
Valentin Touzeau, Claire Maïza, David Monniaux, and Jan Reineke
(Grenoble Alps University, France; Grenoble INP, France; CNRS, France; Saarland University, Germany)
Publisher's Version
|
| |
Montagu, Benoît |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Inferring Frame Conditions ..."
Inferring Frame Conditions with Static Correlation Analysis
Oana F. Andreescu, Thomas Jensen, Stéphane Lescuyer, and Benoît Montagu
(Internet of Trust, France; Inria, France; Prove & Run, France)
Publisher's Version
Artifacts Functional
|
| |
Montesi, Fabrizio |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Better Late Than Never: A ..."
Better Late Than Never: A Fully-Abstract Semantics for Classical Processes
Wen Kokke, Fabrizio Montesi, and Marco Peressotti
(University of Edinburgh, UK; University of Southern Denmark, Denmark)
Publisher's Version
|
| |
Morris, J. Garrett |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Abstracting Extensible Data ..."
Abstracting Extensible Data Types: Or, Rows by Any Other Name
J. Garrett Morris and James McKinna
(University of Kansas, USA; University of Edinburgh, UK)
Publisher's Version
Proc. ACM Program. Lang., vol. 3, issue POPL: "Exceptional Asynchronous Session ..."
Exceptional Asynchronous Session Types: Session Types without Tiers
Simon Fowler, Sam Lindley, J. Garrett Morris, and Sára Decova
(University of Edinburgh, UK; University of Kansas, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Mundkur, Prashanth |
Proc. ACM Program. Lang., vol. 3, issue POPL: "ISA Semantics for ARMv8-A, ..."
ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter Sewell
(University of Cambridge, UK; University of Edinburgh, UK; ARM, UK; SRI International, USA)
Publisher's Version
Artifacts Functional
|
| |
Myers, Andrew C. |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Abstraction-Safe Effect Handlers ..."
Abstraction-Safe Effect Handlers via Tunneling
Yizhou Zhang and Andrew C. Myers
(Cornell University, USA)
Publisher's Version
|
| |
New, Max S.
|
Proc. ACM Program. Lang., vol. 3, issue POPL: "Gradual Type Theory ..."
Gradual Type Theory
Max S. New, Daniel R. Licata, and Amal Ahmed
(Northeastern University, USA; Wesleyan University, USA; Inria, France)
Publisher's Version
|
| |
Ng, Nicholas |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Distributed Programming using ..."
Distributed Programming using Role-Parametric Session Types in Go: Statically-Typed Endpoint APIs for Dynamically-Instantiated Communication Structures
David Castro, Raymond Hu, Sung-Shik Jongmans, Nicholas Ng, and Nobuko Yoshida
(Imperial College London, UK; Open University of the Netherlands, Netherlands)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Noll, Thomas |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Quantitative Separation Logic: ..."
Quantitative Separation Logic: A Logic for Reasoning about Probabilistic Pointer Programs
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll
(RWTH Aachen University, Germany)
Publisher's Version
|
| |
Norton, Robert M. |
Proc. ACM Program. Lang., vol. 3, issue POPL: "ISA Semantics for ARMv8-A, ..."
ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter Sewell
(University of Cambridge, UK; University of Edinburgh, UK; ARM, UK; SRI International, USA)
Publisher's Version
Artifacts Functional
|
| |
O'Hearn, Peter W.
|
Proc. ACM Program. Lang., vol. 3, issue POPL: "A True Positives Theorem for ..."
A True Positives Theorem for a Static Race Detector
Nikos Gorogiannis, Peter W. O'Hearn, and Ilya Sergey
(Facebook, UK; Middlesex University, UK; University College London, UK; Yale-NUS College, Singapore; National University of Singapore, Singapore)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Okati, Nastaran |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Efficient Parameterized Algorithms ..."
Efficient Parameterized Algorithms for Data Packing
Krishnendu Chatterjee, Amir Kafshdar Goharshady, Nastaran Okati, and Andreas Pavlogiannis
(IST Austria, Austria; Ferdowsi University of Mashhad, Iran; EPFL, Switzerland)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Omar, Cyrus |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Live Functional Programming ..."
Live Functional Programming with Typed Holes
Cyrus Omar, Ian Voysey, Ravi Chugh, and Matthew A. Hammer
(University of Chicago, USA; Carnegie Mellon University, USA; University of Colorado Boulder, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Padoan, Tommaso
|
Proc. ACM Program. Lang., vol. 3, issue POPL: "Fixpoint Games on Continuous ..."
Fixpoint Games on Continuous Lattices
Paolo Baldan, Barbara König, Christina Mika-Michalski, and Tommaso Padoan
(University of Padua, Italy; University of Duisburg-Essen, Germany)
Publisher's Version
|
| |
Park, Gyunghee |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Polymorphic Symmetric Multiple ..."
Polymorphic Symmetric Multiple Dispatch with Variance
Gyunghee Park, Jaemin Hong, Guy L. Steele Jr., and Sukyoung Ryu
(KAIST, South Korea; Oracle Labs, USA)
Publisher's Version
|
| |
Parker, James |
Proc. ACM Program. Lang., vol. 3, issue POPL: "LWeb: Information Flow Security ..."
LWeb: Information Flow Security for Multi-tier Web Applications
James Parker, Niki Vazou, and Michael Hicks
(University of Maryland, USA; IMDEA Software Institute, Spain)
Publisher's Version
|
| |
Parno, Bryan |
Proc. ACM Program. Lang., vol. 3, issue POPL: "A Verified, Efficient Embedding ..."
A Verified, Efficient Embedding of a Verifiable Assembly Language
Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, and Nikhil Swamy
(Carnegie Mellon University, USA; Princeton University, USA; Microsoft Research, USA; Microsoft Research, India)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Pavlogiannis, Andreas |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Efficient Parameterized Algorithms ..."
Efficient Parameterized Algorithms for Data Packing
Krishnendu Chatterjee, Amir Kafshdar Goharshady, Nastaran Okati, and Andreas Pavlogiannis
(IST Austria, Austria; Ferdowsi University of Mashhad, Iran; EPFL, Switzerland)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Peressotti, Marco |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Better Late Than Never: A ..."
Better Late Than Never: A Fully-Abstract Semantics for Classical Processes
Wen Kokke, Fabrizio Montesi, and Marco Peressotti
(University of Edinburgh, UK; University of Southern Denmark, Denmark)
Publisher's Version
|
| |
Petrucciani, Tommaso |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Gradual Typing: A New Perspective ..."
Gradual Typing: A New Perspective
Giuseppe Castagna, Victor Lanvin, Tommaso Petrucciani, and Jeremy G. Siek
(CNRS, France; University of Paris Diderot, France; University of Genoa, Italy; Indiana University, USA)
Publisher's Version
|
| |
Piedeleu, Robin |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Diagrammatic Algebra: From ..."
Diagrammatic Algebra: From Linear to Concurrent Systems
Filippo Bonchi, Joshua Holland, Robin Piedeleu, Paweł Sobociński, and Fabio Zanasi
(University of Pisa, Italy; University of Southampton, UK; University of Oxford, UK; University College London, UK)
Publisher's Version
|
| |
Piróg, Maciej |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Abstracting Algebraic Effects ..."
Abstracting Algebraic Effects
Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski
(University of Wrocław, Poland)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Podkopaev, Anton |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Bridging the Gap between Programming ..."
Bridging the Gap between Programming Languages and Hardware Weak Memory Models
Anton Podkopaev, Ori Lahav, and Viktor Vafeiadis
(St. Petersburg University, Russia; JetBrains Research, Russia; MPI-SWS, Germany; Tel Aviv University, Israel)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Polesiuk, Piotr |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Abstracting Algebraic Effects ..."
Abstracting Algebraic Effects
Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski
(University of Wrocław, Poland)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Polikarpova, Nadia |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Structuring the Synthesis ..."
Structuring the Synthesis of Heap-Manipulating Programs
Nadia Polikarpova and Ilya Sergey
(University of California at San Diego, USA; Yale-NUS College, Singapore; National University of Singapore, Singapore)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Popescu, Andrei |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Bindings as Bounded Natural ..."
Bindings as Bounded Natural Functors
Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, and Dmitriy Traytel
(Vrije Universiteit Amsterdam, Netherlands; Max Planck Institute for Informatics, Germany; Middlesex University, UK; Institute of Mathematics at Romanian Academy, Romania; ETH Zurich, Switzerland)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Popescu, Natalie |
Proc. ACM Program. Lang., vol. 3, issue POPL: "CT-Wasm: Type-Driven Secure ..."
CT-Wasm: Type-Driven Secure Cryptography for the Web Ecosystem
Conrad Watt, John Renner, Natalie Popescu, Sunjay Cauligi, and Deian Stefan
(University of Cambridge, UK; University of California at San Diego, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Pulte, Christopher |
Proc. ACM Program. Lang., vol. 3, issue POPL: "ISA Semantics for ARMv8-A, ..."
ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter Sewell
(University of Cambridge, UK; University of Edinburgh, UK; ARM, UK; SRI International, USA)
Publisher's Version
Artifacts Functional
|
| |
Püschel, Markus |
Proc. ACM Program. Lang., vol. 3, issue POPL: "An Abstract Domain for Certifying ..."
An Abstract Domain for Certifying Neural Networks
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev
(ETH Zurich, Switzerland)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Raad, Azalea
|
Proc. ACM Program. Lang., vol. 3, issue POPL: "On Library Correctness under ..."
On Library Correctness under Weak Memory Consistency: Specifying and Verifying Concurrent Libraries under Declarative Consistency Models
Azalea Raad, Marko Doko, Lovro Rožić, Ori Lahav, and Viktor Vafeiadis
(MPI-SWS, Germany; Tel Aviv University, Israel)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Rajani, Vineet |
Proc. ACM Program. Lang., vol. 3, issue POPL: "From Fine- to Coarse-Grained ..."
From Fine- to Coarse-Grained Dynamic Information Flow Control and Back
Marco Vassena, Alejandro Russo, Deepak Garg, Vineet Rajani, and Deian Stefan
(Chalmers University of Technology, Sweden; MPI-SWS, Germany; University of California at San Diego, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Ranzato, Francesco |
Proc. ACM Program. Lang., vol. 3, issue POPL: "A²I: Abstract² Interpretation ..."
A²I: Abstract² Interpretation
Patrick Cousot, Roberto Giacobazzi, and Francesco Ranzato
(New York University, USA; University of Verona, Italy; IMDEA Software Institute, Spain; University of Padua, Italy)
Publisher's Version
|
| |
Rastogi, Aseem |
Proc. ACM Program. Lang., vol. 3, issue POPL: "A Verified, Efficient Embedding ..."
A Verified, Efficient Embedding of a Verifiable Assembly Language
Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, and Nikhil Swamy
(Carnegie Mellon University, USA; Princeton University, USA; Microsoft Research, USA; Microsoft Research, India)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Rehof, Jakob |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Principality and Approximation ..."
Principality and Approximation under Dimensional Bound
Andrej Dudenhefner and Jakob Rehof
(TU Dortmund, Germany)
Publisher's Version
|
| |
Reid, Alastair |
Proc. ACM Program. Lang., vol. 3, issue POPL: "ISA Semantics for ARMv8-A, ..."
ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter Sewell
(University of Cambridge, UK; University of Edinburgh, UK; ARM, UK; SRI International, USA)
Publisher's Version
Artifacts Functional
|
| |
Reineke, Jan |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Fast and Exact Analysis for ..."
Fast and Exact Analysis for LRU Caches
Valentin Touzeau, Claire Maïza, David Monniaux, and Jan Reineke
(Grenoble Alps University, France; Grenoble INP, France; CNRS, France; Saarland University, Germany)
Publisher's Version
|
| |
Renner, John |
Proc. ACM Program. Lang., vol. 3, issue POPL: "CT-Wasm: Type-Driven Secure ..."
CT-Wasm: Type-Driven Secure Cryptography for the Web Ecosystem
Conrad Watt, John Renner, Natalie Popescu, Sunjay Cauligi, and Deian Stefan
(University of Cambridge, UK; University of California at San Diego, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Reps, Thomas |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Refinement of Path Expressions ..."
Refinement of Path Expressions for Static Analysis
John Cyphert, Jason Breck, Zachary Kincaid, and Thomas Reps
(University of Wisconsin, USA; Princeton University, USA; GrammaTech, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Proc. ACM Program. Lang., vol. 3, issue POPL: "Closed Forms for Numerical ..."
Closed Forms for Numerical Loops
Zachary Kincaid, Jason Breck, John Cyphert, and Thomas Reps
(Princeton University, USA; University of Wisconsin, USA; GrammaTech, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Richardson, Alexander |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Exploring C Semantics and ..."
Exploring C Semantics and Pointer Provenance
Kayvan Memarian, Victor B. F. Gomes, Brooks Davis, Stephen Kell, Alexander Richardson, Robert N. M. Watson, and Peter Sewell
(University of Cambridge, UK; SRI International, USA)
Publisher's Version
|
| |
Rinard, Martin C. |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Bayesian Synthesis of Probabilistic ..."
Bayesian Synthesis of Probabilistic Programs for Automatic Data Modeling
Feras A. Saad, Marco F. Cusumano-Towner, Ulrich Schaechtle, Martin C. Rinard, and Vikash K. Mansinghka
(Massachusetts Institute of Technology, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Rožić, Lovro |
Proc. ACM Program. Lang., vol. 3, issue POPL: "On Library Correctness under ..."
On Library Correctness under Weak Memory Consistency: Specifying and Verifying Concurrent Libraries under Declarative Consistency Models
Azalea Raad, Marko Doko, Lovro Rožić, Ori Lahav, and Viktor Vafeiadis
(MPI-SWS, Germany; Tel Aviv University, Israel)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Rümmer, Philipp |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Decision Procedures for Path ..."
Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations
Taolue Chen, Matthew Hague, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu
(Birkbeck University of London, UK; Royal Holloway University of London, UK; University of Oxford, UK; Uppsala University, Sweden; Institute of Software at Chinese Academy of Sciences, China)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Russo, Alejandro |
Proc. ACM Program. Lang., vol. 3, issue POPL: "From Fine- to Coarse-Grained ..."
From Fine- to Coarse-Grained Dynamic Information Flow Control and Back
Marco Vassena, Alejandro Russo, Deepak Garg, Vineet Rajani, and Deian Stefan
(Chalmers University of Technology, Sweden; MPI-SWS, Germany; University of California at San Diego, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Ryu, Sukyoung |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Polymorphic Symmetric Multiple ..."
Polymorphic Symmetric Multiple Dispatch with Variance
Gyunghee Park, Jaemin Hong, Guy L. Steele Jr., and Sukyoung Ryu
(KAIST, South Korea; Oracle Labs, USA)
Publisher's Version
|
| |
Saad, Feras A.
|
Proc. ACM Program. Lang., vol. 3, issue POPL: "Bayesian Synthesis of Probabilistic ..."
Bayesian Synthesis of Probabilistic Programs for Automatic Data Modeling
Feras A. Saad, Marco F. Cusumano-Towner, Ulrich Schaechtle, Martin C. Rinard, and Vikash K. Mansinghka
(Massachusetts Institute of Technology, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Sampaio, Gabriela |
Proc. ACM Program. Lang., vol. 3, issue POPL: "JaVerT 2.0: Compositional ..."
JaVerT 2.0: Compositional Symbolic Execution for JavaScript
José Fragoso Santos, Petar Maksimović, Gabriela Sampaio, and Philippa Gardner
(Imperial College London, UK; Mathematical Institute SASA, Serbia)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Sato, Tetsuya |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Formal Verification of Higher-Order ..."
Formal Verification of Higher-Order Probabilistic Programs: Reasoning about Approximation, Convergence, Bayesian Inference, and Optimization
Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Justin Hsu
(SUNY Buffalo, USA; IMDEA Software Institute, Spain; MPI-SWS, Germany; University of Wisconsin-Madison, USA)
Publisher's Version
|
| |
Scalas, Alceste |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Less Is More: Multiparty Session ..."
Less Is More: Multiparty Session Types Revisited
Alceste Scalas and Nobuko Yoshida
(Imperial College London, UK)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Schaechtle, Ulrich |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Bayesian Synthesis of Probabilistic ..."
Bayesian Synthesis of Probabilistic Programs for Automatic Data Modeling
Feras A. Saad, Marco F. Cusumano-Towner, Ulrich Schaechtle, Martin C. Rinard, and Vikash K. Mansinghka
(Massachusetts Institute of Technology, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Schmitt, Alan |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Skeletal Semantics and Their ..."
Skeletal Semantics and Their Interpretations
Martin Bodin, Philippa Gardner, Thomas Jensen, and Alan Schmitt
(Imperial College London, UK; Inria, France)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Sekiyama, Taro |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Dynamic Type Inference for ..."
Dynamic Type Inference for Gradual Hindley–Milner Typing
Yusuke Miyazaki, Taro Sekiyama, and Atsushi Igarashi
(Kyoto University, Japan; National Institute of Informatics, Japan)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Sergey, Ilya |
Proc. ACM Program. Lang., vol. 3, issue POPL: "A True Positives Theorem for ..."
A True Positives Theorem for a Static Race Detector
Nikos Gorogiannis, Peter W. O'Hearn, and Ilya Sergey
(Facebook, UK; Middlesex University, UK; University College London, UK; Yale-NUS College, Singapore; National University of Singapore, Singapore)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 3, issue POPL: "Structuring the Synthesis ..."
Structuring the Synthesis of Heap-Manipulating Programs
Nadia Polikarpova and Ilya Sergey
(University of California at San Diego, USA; Yale-NUS College, Singapore; National University of Singapore, Singapore)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Sewell, Peter |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Exploring C Semantics and ..."
Exploring C Semantics and Pointer Provenance
Kayvan Memarian, Victor B. F. Gomes, Brooks Davis, Stephen Kell, Alexander Richardson, Robert N. M. Watson, and Peter Sewell
(University of Cambridge, UK; SRI International, USA)
Publisher's Version
Proc. ACM Program. Lang., vol. 3, issue POPL: "ISA Semantics for ARMv8-A, ..."
ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter Sewell
(University of Cambridge, UK; University of Edinburgh, UK; ARM, UK; SRI International, USA)
Publisher's Version
Artifacts Functional
|
| |
Shao, Zhong |
Proc. ACM Program. Lang., vol. 3, issue POPL: "An Abstract Stack Based Approach ..."
An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code
Yuting Wang, Pierre Wilke, and Zhong Shao
(Yale University, USA; CentraleSupélec, France)
Publisher's Version
Artifacts Functional
|
| |
Shi, Kensen |
Proc. ACM Program. Lang., vol. 3, issue POPL: "FrAngel: Component-Based Synthesis ..."
FrAngel: Component-Based Synthesis with Control Structures
Kensen Shi, Jacob Steinhardt, and Percy Liang
(Stanford University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Sieczkowski, Filip |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Abstracting Algebraic Effects ..."
Abstracting Algebraic Effects
Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski
(University of Wrocław, Poland)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Siek, Jeremy G. |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Gradual Typing: A New Perspective ..."
Gradual Typing: A New Perspective
Giuseppe Castagna, Victor Lanvin, Tommaso Petrucciani, and Jeremy G. Siek
(CNRS, France; University of Paris Diderot, France; University of Genoa, Italy; Indiana University, USA)
Publisher's Version
|
| |
Singh, Gagandeep |
Proc. ACM Program. Lang., vol. 3, issue POPL: "An Abstract Domain for Certifying ..."
An Abstract Domain for Certifying Neural Networks
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev
(ETH Zurich, Switzerland)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Skorstengaard, Lau |
Proc. ACM Program. Lang., vol. 3, issue POPL: "StkTokens: Enforcing Well-Bracketed ..."
StkTokens: Enforcing Well-Bracketed Control Flow and Stack Encapsulation Using Linear Capabilities
Lau Skorstengaard, Dominique Devriese, and Lars Birkedal
(Aarhus University, Denmark; Vrije Universiteit Brussel, Belgium)
Publisher's Version
|
| |
Smith, Calvin |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Trace Abstraction Modulo Probability ..."
Trace Abstraction Modulo Probability
Calvin Smith, Justin Hsu, and Aws Albarghouthi
(University of Wisconsin-Madison, USA)
Publisher's Version
|
| |
Sobociński, Paweł |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Diagrammatic Algebra: From ..."
Diagrammatic Algebra: From Linear to Concurrent Systems
Filippo Bonchi, Joshua Holland, Robin Piedeleu, Paweł Sobociński, and Fabio Zanasi
(University of Pisa, Italy; University of Southampton, UK; University of Oxford, UK; University College London, UK)
Publisher's Version
|
| |
Sozeau, Matthieu |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Definitional Proof-Irrelevance ..."
Definitional Proof-Irrelevance without K
Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau
(Inria, France; Chalmers University of Technology, Sweden; University of Gothenburg, Sweden; IRIF, France)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Späth, Johannes |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Context-, Flow-, and Field-Sensitive ..."
Context-, Flow-, and Field-Sensitive Data-Flow Analysis using Synchronized Pushdown Systems
Johannes Späth, Karim Ali, and Eric Bodden
(Fraunhofer IEM, Germany; University of Alberta, Canada; University of Paderborn, Germany)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Stanford, Caleb |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Modular Quantitative Monitoring ..."
Modular Quantitative Monitoring
Rajeev Alur, Konstantinos Mamouras, and Caleb Stanford
(University of Pennsylvania, USA; Rice University, USA)
Publisher's Version
|
| |
Stark, Ian |
Proc. ACM Program. Lang., vol. 3, issue POPL: "ISA Semantics for ARMv8-A, ..."
ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter Sewell
(University of Cambridge, UK; University of Edinburgh, UK; ARM, UK; SRI International, USA)
Publisher's Version
Artifacts Functional
|
| |
Staton, Sam |
Proc. ACM Program. Lang., vol. 3, issue POPL: "A Domain Theory for Statistical ..."
A Domain Theory for Statistical Probabilistic Programming
Matthijs Vákár, Ohad Kammar, and Sam Staton
(Columbia University, USA; University of Oxford, UK)
Publisher's Version
|
| |
Steele Jr., Guy L. |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Polymorphic Symmetric Multiple ..."
Polymorphic Symmetric Multiple Dispatch with Variance
Gyunghee Park, Jaemin Hong, Guy L. Steele Jr., and Sukyoung Ryu
(KAIST, South Korea; Oracle Labs, USA)
Publisher's Version
|
| |
Stefan, Deian |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Pretend Synchrony: Synchronous ..."
Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs
Klaus v. Gleissenthall, Rami Gökhan Kıcı, Alexander Bakst, Deian Stefan, and Ranjit Jhala
(University of California at San Diego, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 3, issue POPL: "From Fine- to Coarse-Grained ..."
From Fine- to Coarse-Grained Dynamic Information Flow Control and Back
Marco Vassena, Alejandro Russo, Deepak Garg, Vineet Rajani, and Deian Stefan
(Chalmers University of Technology, Sweden; MPI-SWS, Germany; University of California at San Diego, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Proc. ACM Program. Lang., vol. 3, issue POPL: "CT-Wasm: Type-Driven Secure ..."
CT-Wasm: Type-Driven Secure Cryptography for the Web Ecosystem
Conrad Watt, John Renner, Natalie Popescu, Sunjay Cauligi, and Deian Stefan
(University of Cambridge, UK; University of California at San Diego, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Steinhardt, Jacob |
Proc. ACM Program. Lang., vol. 3, issue POPL: "FrAngel: Component-Based Synthesis ..."
FrAngel: Component-Based Synthesis with Control Structures
Kensen Shi, Jacob Steinhardt, and Percy Liang
(Stanford University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Sutton, Charles |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Probabilistic Programming ..."
Probabilistic Programming with Densities in SlicStan: Efficient, Flexible, and Deterministic
Maria I. Gorinova, Andrew D. Gordon, and Charles Sutton
(University of Edinburgh, UK; Microsoft Research, UK; Google Brain, USA)
Publisher's Version
|
| |
Swamy, Nikhil |
Proc. ACM Program. Lang., vol. 3, issue POPL: "A Verified, Efficient Embedding ..."
A Verified, Efficient Embedding of a Verifiable Assembly Language
Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, and Nikhil Swamy
(Carnegie Mellon University, USA; Princeton University, USA; Microsoft Research, USA; Microsoft Research, India)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Tabareau, Nicolas
|
Proc. ACM Program. Lang., vol. 3, issue POPL: "Definitional Proof-Irrelevance ..."
Definitional Proof-Irrelevance without K
Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau
(Inria, France; Chalmers University of Technology, Sweden; University of Gothenburg, Sweden; IRIF, France)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Tanter, Éric |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Gradual Parametricity, Revisited ..."
Gradual Parametricity, Revisited
Matías Toro, Elizabeth Labrada, and Éric Tanter
(University of Chile, Chile; Inria, France)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Tassarotti, Joseph |
Proc. ACM Program. Lang., vol. 3, issue POPL: "A Separation Logic for Concurrent ..."
A Separation Logic for Concurrent Randomized Programs
Joseph Tassarotti and Robert Harper
(Carnegie Mellon University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Toman, John |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Concerto: A Framework for ..."
Concerto: A Framework for Combined Concrete and Abstract Interpretation
John Toman and Dan Grossman
(University of Washington, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Toro, Matías |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Gradual Parametricity, Revisited ..."
Gradual Parametricity, Revisited
Matías Toro, Elizabeth Labrada, and Éric Tanter
(University of Chile, Chile; Inria, France)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Touzeau, Valentin |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Fast and Exact Analysis for ..."
Fast and Exact Analysis for LRU Caches
Valentin Touzeau, Claire Maïza, David Monniaux, and Jan Reineke
(Grenoble Alps University, France; Grenoble INP, France; CNRS, France; Saarland University, Germany)
Publisher's Version
|
| |
Tov, Jesse A. |
Proc. ACM Program. Lang., vol. 3, issue POPL: "A Calculus for Esterel: If ..."
A Calculus for Esterel: If can, can. If no can, no can.
Spencer P. Florence, Shu-Hung You, Jesse A. Tov, and Robert Bruce Findler
(Northwestern University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Traytel, Dmitriy |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Bindings as Bounded Natural ..."
Bindings as Bounded Natural Functors
Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, and Dmitriy Traytel
(Vrije Universiteit Amsterdam, Netherlands; Max Planck Institute for Informatics, Germany; Middlesex University, UK; Institute of Mathematics at Romanian Academy, Romania; ETH Zurich, Switzerland)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Unruh, Dominique
|
Proc. ACM Program. Lang., vol. 3, issue POPL: "Quantum Relational Hoare Logic ..."
Quantum Relational Hoare Logic
Dominique Unruh
(University of Tartu, Estonia)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Vafeiadis, Viktor
|
Proc. ACM Program. Lang., vol. 3, issue POPL: "On Library Correctness under ..."
On Library Correctness under Weak Memory Consistency: Specifying and Verifying Concurrent Libraries under Declarative Consistency Models
Azalea Raad, Marko Doko, Lovro Rožić, Ori Lahav, and Viktor Vafeiadis
(MPI-SWS, Germany; Tel Aviv University, Israel)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Proc. ACM Program. Lang., vol. 3, issue POPL: "Bridging the Gap between Programming ..."
Bridging the Gap between Programming Languages and Hardware Weak Memory Models
Anton Podkopaev, Ori Lahav, and Viktor Vafeiadis
(St. Petersburg University, Russia; JetBrains Research, Russia; MPI-SWS, Germany; Tel Aviv University, Israel)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Proc. ACM Program. Lang., vol. 3, issue POPL: "Grounding Thin-Air Reads with ..."
Grounding Thin-Air Reads with Event Structures
Soham Chakraborty and Viktor Vafeiadis
(MPI-SWS, Germany)
Publisher's Version
|
| |
Vákár, Matthijs |
Proc. ACM Program. Lang., vol. 3, issue POPL: "A Domain Theory for Statistical ..."
A Domain Theory for Statistical Probabilistic Programming
Matthijs Vákár, Ohad Kammar, and Sam Staton
(Columbia University, USA; University of Oxford, UK)
Publisher's Version
|
| |
Vassena, Marco |
Proc. ACM Program. Lang., vol. 3, issue POPL: "From Fine- to Coarse-Grained ..."
From Fine- to Coarse-Grained Dynamic Information Flow Control and Back
Marco Vassena, Alejandro Russo, Deepak Garg, Vineet Rajani, and Deian Stefan
(Chalmers University of Technology, Sweden; MPI-SWS, Germany; University of California at San Diego, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Vazou, Niki |
Proc. ACM Program. Lang., vol. 3, issue POPL: "LWeb: Information Flow Security ..."
LWeb: Information Flow Security for Multi-tier Web Applications
James Parker, Niki Vazou, and Michael Hicks
(University of Maryland, USA; IMDEA Software Institute, Spain)
Publisher's Version
|
| |
Vechev, Martin |
Proc. ACM Program. Lang., vol. 3, issue POPL: "An Abstract Domain for Certifying ..."
An Abstract Domain for Certifying Neural Networks
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev
(ETH Zurich, Switzerland)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Veltri, Niccolò |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Bisimulation as Path Type ..."
Bisimulation as Path Type for Guarded Recursive Types
Rasmus Ejlers Møgelberg and Niccolò Veltri
(IT University of Copenhagen, Denmark)
Publisher's Version
|
| |
V. Gleissenthall, Klaus |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Pretend Synchrony: Synchronous ..."
Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs
Klaus v. Gleissenthall, Rami Gökhan Kıcı, Alexander Bakst, Deian Stefan, and Ranjit Jhala
(University of California at San Diego, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Viswanathan, Mahesh |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Decidable Verification of ..."
Decidable Verification of Uninterpreted Programs
Umang Mathur, P. Madhusudan, and Mahesh Viswanathan
(University of Illinois at Urbana-Champaign, USA)
Publisher's Version
|
| |
Voysey, Ian |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Live Functional Programming ..."
Live Functional Programming with Typed Holes
Cyrus Omar, Ian Voysey, Ravi Chugh, and Matthew A. Hammer
(University of Chicago, USA; Carnegie Mellon University, USA; University of Colorado Boulder, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Wang, Di
|
Proc. ACM Program. Lang., vol. 3, issue POPL: "Type-Guided Worst-Case Input ..."
Type-Guided Worst-Case Input Generation
Di Wang and Jan Hoffmann
(Carnegie Mellon University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Wang, Yuting |
Proc. ACM Program. Lang., vol. 3, issue POPL: "An Abstract Stack Based Approach ..."
An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code
Yuting Wang, Pierre Wilke, and Zhong Shao
(Yale University, USA; CentraleSupélec, France)
Publisher's Version
Artifacts Functional
|
| |
Wassell, Mark |
Proc. ACM Program. Lang., vol. 3, issue POPL: "ISA Semantics for ARMv8-A, ..."
ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter Sewell
(University of Cambridge, UK; University of Edinburgh, UK; ARM, UK; SRI International, USA)
Publisher's Version
Artifacts Functional
|
| |
Watson, Robert N. M. |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Exploring C Semantics and ..."
Exploring C Semantics and Pointer Provenance
Kayvan Memarian, Victor B. F. Gomes, Brooks Davis, Stephen Kell, Alexander Richardson, Robert N. M. Watson, and Peter Sewell
(University of Cambridge, UK; SRI International, USA)
Publisher's Version
|
| |
Watt, Conrad |
Proc. ACM Program. Lang., vol. 3, issue POPL: "CT-Wasm: Type-Driven Secure ..."
CT-Wasm: Type-Driven Secure Cryptography for the Web Ecosystem
Conrad Watt, John Renner, Natalie Popescu, Sunjay Cauligi, and Deian Stefan
(University of Cambridge, UK; University of California at San Diego, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Wilke, Pierre |
Proc. ACM Program. Lang., vol. 3, issue POPL: "An Abstract Stack Based Approach ..."
An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code
Yuting Wang, Pierre Wilke, and Zhong Shao
(Yale University, USA; CentraleSupélec, France)
Publisher's Version
Artifacts Functional
|
| |
Winskel, Glynn |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Game Semantics for Quantum ..."
Game Semantics for Quantum Programming
Pierre Clairambault, Marc De Visme, and Glynn Winskel
(University of Lyon, France; CNRS, France; ENS Lyon, France; University of Cambridge, UK)
Publisher's Version
|
| |
Wolff, Sebastian |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Decoupling Lock-Free Data ..."
Decoupling Lock-Free Data Structures from Memory Reclamation for Static Analysis
Roland Meyer and Sebastian Wolff
(TU Braunschweig, Germany)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Wu, Xiaodi |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Quantitative Robustness Analysis ..."
Quantitative Robustness Analysis of Quantum Programs
Shih-Han Hung, Kesha Hietala, Shaopeng Zhu, Mingsheng Ying, Michael Hicks, and Xiaodi Wu
(University of Maryland, USA; University of Technology Sydney, Australia; Institute of Software at Chinese Academy of Sciences, China; Tsinghua University, China)
Publisher's Version
|
| |
Wu, Zhilin |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Decision Procedures for Path ..."
Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations
Taolue Chen, Matthew Hague, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu
(Birkbeck University of London, UK; Royal Holloway University of London, UK; University of Oxford, UK; Uppsala University, Sweden; Institute of Software at Chinese Academy of Sciences, China)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Yahav, Eran
|
Proc. ACM Program. Lang., vol. 3, issue POPL: "code2vec: Learning Distributed ..."
code2vec: Learning Distributed Representations of Code
Uri Alon, Meital Zilberstein, Omer Levy, and Eran Yahav
(Technion, Israel; Facebook AI Research, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Yi, Xin |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Efficient Automated Repair ..."
Efficient Automated Repair of High Floating-Point Errors in Numerical Libraries
Xin Yi, Liqian Chen, Xiaoguang Mao, and Tao Ji
(National University of Defense Technology, China)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Ying, Mingsheng |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Quantitative Robustness Analysis ..."
Quantitative Robustness Analysis of Quantum Programs
Shih-Han Hung, Kesha Hietala, Shaopeng Zhu, Mingsheng Ying, Michael Hicks, and Xiaodi Wu
(University of Maryland, USA; University of Technology Sydney, Australia; Institute of Software at Chinese Academy of Sciences, China; Tsinghua University, China)
Publisher's Version
|
| |
Yoshida, Nobuko |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Two Sides of the Same Coin: ..."
Two Sides of the Same Coin: Session Types and Game Semantics: A Synchronous Side and an Asynchronous Side
Simon Castellan and Nobuko Yoshida
(Imperial College London, UK)
Publisher's Version
Proc. ACM Program. Lang., vol. 3, issue POPL: "Distributed Programming using ..."
Distributed Programming using Role-Parametric Session Types in Go: Statically-Typed Endpoint APIs for Dynamically-Instantiated Communication Structures
David Castro, Raymond Hu, Sung-Shik Jongmans, Nicholas Ng, and Nobuko Yoshida
(Imperial College London, UK; Open University of the Netherlands, Netherlands)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Proc. ACM Program. Lang., vol. 3, issue POPL: "Less Is More: Multiparty Session ..."
Less Is More: Multiparty Session Types Revisited
Alceste Scalas and Nobuko Yoshida
(Imperial College London, UK)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Yoshimizu, Akira |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Intersection Types and Runtime ..."
Intersection Types and Runtime Errors in the Pi-Calculus
Ugo Dal Lago, Marc de Visme, Damiano Mazza, and Akira Yoshimizu
(University of Bologna, Italy; Inria, France; University of Lyon, France; ENS Lyon, France; CNRS, France; University of Paris 13, France)
Publisher's Version
|
| |
You, Shu-Hung |
Proc. ACM Program. Lang., vol. 3, issue POPL: "A Calculus for Esterel: If ..."
A Calculus for Esterel: If can, can. If no can, no can.
Spencer P. Florence, Shu-Hung You, Jesse A. Tov, and Robert Bruce Findler
(Northwestern University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Zanasi, Fabio
|
Proc. ACM Program. Lang., vol. 3, issue POPL: "Diagrammatic Algebra: From ..."
Diagrammatic Algebra: From Linear to Concurrent Systems
Filippo Bonchi, Joshua Holland, Robin Piedeleu, Paweł Sobociński, and Fabio Zanasi
(University of Pisa, Italy; University of Southampton, UK; University of Oxford, UK; University College London, UK)
Publisher's Version
|
| |
Zhang, Yizhou |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Abstraction-Safe Effect Handlers ..."
Abstraction-Safe Effect Handlers via Tunneling
Yizhou Zhang and Andrew C. Myers
(Cornell University, USA)
Publisher's Version
|
| |
Zhu, Shaopeng |
Proc. ACM Program. Lang., vol. 3, issue POPL: "Quantitative Robustness Analysis ..."
Quantitative Robustness Analysis of Quantum Programs
Shih-Han Hung, Kesha Hietala, Shaopeng Zhu, Mingsheng Ying, Michael Hicks, and Xiaodi Wu
(University of Maryland, USA; University of Technology Sydney, Australia; Institute of Software at Chinese Academy of Sciences, China; Tsinghua University, China)
Publisher's Version
|
| |
Zilberstein, Meital |
Proc. ACM Program. Lang., vol. 3, issue POPL: "code2vec: Learning Distributed ..."
code2vec: Learning Distributed Representations of Code
Uri Alon, Meital Zilberstein, Omer Levy, and Eran Yahav
(Technion, Israel; Facebook AI Research, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|