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