POPL 2020
Proceedings of the ACM on Programming Languages, Volume 4, Number POPL
Powered by
Conference Publishing Consulting

Proceedings of the ACM on Programming Languages, Volume 4, Number POPL, January 19–25, 2020, New Orleans, LA, USA

POPL – Journal Issue

Contents - Abstracts - Authors

Frontmatter

Title Page
Editorial Message
Sponsors

Papers

Taylor Subsumes Scott, Berry, Kahn and Plotkin
Davide Barbarossa and Giulio Manzonetto
(University of Paris 13, France)
Article Search
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)
Article Search
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)
Article Search Artifacts Available Artifacts Reusable
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)
Article Search Artifacts Available Artifacts Reusable
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)
Article Search
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)
Preprint Artifacts Available Artifacts Reusable
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)
Preprint Artifacts Available Artifacts Reusable
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)
Article Search Artifacts Available Artifacts Reusable
Undecidability of D<: and Its Decidable Fragments
Jason Z. S. Hu and Ondřej Lhoták
(McGill University, Canada; University of Waterloo, Canada)
Article Search Info Artifacts Available Artifacts Reusable
Incorrectness Logic
Peter W. O'Hearn
(Facebook, UK; University College London, UK)
Article Search
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)
Article Search Info
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)
Article Search Info Artifacts Available Artifacts Reusable
Reductions for Safety Proofs
Azadeh Farzan and Anthony Vandikas
(University of Toronto, Canada)
Article Search Artifacts Available Artifacts Reusable
Deterministic Parallel Fixpoint Computation
Sung Kook Kim, Arnaud J. Venet, and Aditya V. Thakur
(University of California at Davis, USA; Facebook, USA)
Preprint Artifacts Available Artifacts Reusable
Recurrence Extraction for Functional Programs through Call-by-Push-Value
G. A. Kavvos, Edward Morehouse, Daniel R. Licata, and Norman Danner
(Wesleyan University, USA)
Article Search
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)
Article Search Artifacts Available Artifacts Reusable
Fast, Sound, and Effectively Complete Dynamic Race Prediction
Andreas Pavlogiannis
(Aarhus University, Denmark)
Article Search
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)
Article Search
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)
Preprint
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)
Article Search Artifacts Functional
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)
Article Search
Seminaïve Evaluation for a Higher-Order Functional Language
Michael Arntzenius and Neel Krishnaswami
(University of Birmingham, UK; University of Cambridge, UK)
Article Search Artifacts Functional
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)
Article Search Info Artifacts Available Artifacts Reusable
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)
Article Search Artifacts Available Artifacts Reusable
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)
Article Search Artifacts Available Artifacts Functional
Parameterized Verification under TSO is PSPACE-Complete
Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Rojin Rezvan
(Uppsala University, Sweden; Sharif University of Technology, Iran)
Article Search
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)
Article Search Artifacts Available Artifacts Reusable
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)
Article Search
What Is Decidable about Gradual Types?
Zeina Migeed and Jens Palsberg
(University of California at Los Angeles, USA)
Article Search Artifacts Available Artifacts Reusable
Decomposition Diversity with Symmetric Data and Codata
David Binder, Julian Jabs, Ingo Skupin, and Klaus Ostermann
(University of Tübingen, Germany)
Article Search Artifacts Reusable
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)
Article Search
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)
Article Search Artifacts Available Artifacts Reusable
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)
Preprint Info
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)
Article Search Info Artifacts Available Artifacts Reusable
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)
Article Search Artifacts Available Artifacts Reusable
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)
Article Search Artifacts Available Artifacts Functional
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)
Article Search
A Simple Differentiable Programming Language
Martín Abadi and Gordon D. Plotkin
(Google Research, USA)
Article Search
PλωNK: Functional Probabilistic NetKAT
Alexander Vandenbroucke and Tom Schrijvers
(KU Leuven, Belgium)
Preprint Info
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)
Article Search
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)
Article Search Info Artifacts Available Artifacts Reusable
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)
Article Search
Executable Formal Semantics for the POSIX Shell
Michael Greenberg and Austin J. Blatt
(Pomona College, USA; Puppet Labs, USA)
Preprint Info Artifacts Available Artifacts Reusable
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)
Article Search Info Artifacts Available Artifacts Reusable
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)
Article Search Info Artifacts Available Artifacts Reusable
Graduality and Parametricity: Together Again for the First Time
Max S. New, Dustin Jamner, and Amal Ahmed
(Northeastern University, USA)
Article Search
Disentanglement in Nested-Parallel Programs
Sam Westrick, Rohan Yadav, Matthew Fluet, and Umut A. Acar
(Carnegie Mellon University, USA; Rochester Institute of Technology, USA)
Article Search
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)
Article Search Artifacts Functional
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)
Article Search Artifacts Available Artifacts Functional
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)
Article Search Artifacts Functional
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)
Article Search Artifacts Available Artifacts Reusable
Synthesizing Replacement Classes
Malavika Samak, Deokhwan Kim, and Martin C. Rinard
(Massachusetts Institute of Technology, USA)
Article Search
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)
Article Search
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)
Article Search Artifacts Functional
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)
Preprint
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)
Article Search
Semantics of Higher-Order Probabilistic Programs with Conditioning
Fredrik Dahlqvist and Dexter Kozen
(University College London, UK; Imperial College London, UK; Cornell University, USA)
Article Search
The Fire Triangle: How to Mix Substitution, Dependent Elimination, and Effects
Pierre-Marie Pédrot and Nicolas Tabareau
(Inria, France)
Article Search
SyTeCi: Automating Contextual Equivalence for Higher-Order Programs with References
Guilhem Jaber
(University of Nantes, France; LS2N CNRS, France; Inria, France)
Article Search Artifacts Available Artifacts Functional
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)
Article Search
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)
Preprint
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)
Article Search Artifacts Available Artifacts Reusable
Full Abstraction for the Quantum Lambda-Calculus
Pierre Clairambault and Marc de Visme
(University of Lyon, France; ENS Lyon, France; CNRS, France; LIP, France)
Article Search
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)
Article Search
Does Blame Shifting Work?
Lukas Lazarek, Alexis King, Samanvitha Sundar, Robert Bruce Findler, and Christos Dimoulas
(Northwestern University, USA)
Article Search Artifacts Available Artifacts Functional
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)
Article Search Artifacts Reusable
Label-Dependent Session Types
Peter Thiemann and Vasco T. Vasconcelos
(University of Freiburg, Germany; University of Lisbon, Portugal)
Preprint
Pointer Life Cycle Types for Lock-Free Data Structures with Memory Reclamation
Roland Meyer and Sebastian Wolff
(TU Braunschweig, Germany)
Article Search Info Artifacts Available Artifacts Reusable

proc time: 28.75