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

Proceedings of the ACM on Programming Languages, Volume 5, Number POPL, January 17–22, 2021, Virtual, Denmark

POPL – Journal Issue

Contents - Abstracts - Authors

Frontmatter

Title Page
Editorial Message
Sponsors

Papers

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

proc time: 38