POPL 2021
2021-01-17..2021-01-22
-- online --
POPL ·
[POPL 2021, POPL 2022, POPL 2022 Virtual Workshop, POPL 2023, POPL 2023 SRC, POPL 2024, POPL 2025, POPL 2026]
as the organisers put it
POPL 2021 videos are publicly available on Clowdr! There are also Clowdr tutorial videos available. POPL 2021 papers published in PACMPL, vol. 5, issue POPL. Preprints are also linked from Clowdr. Having trouble getting on Clowdr? DM @poplconf on Twitter or email popl2021team@gmail.com. Online registration is still open. POPL 2021 will take place on January 17–22, 2021 as a virtual meeting. Here’s How to POPL 2021. Video pre-publication is coming! The POPL 2021 Program is up! POPL 2021 Accepted Papers
| title | author | length |
|---|---|---|
| Welcome to Copenhagen, where everything's perfect, as it always is! | 14m | |
But maybe you won't be able to eat a POPL burger this go round... | ||
| Emotional Machines | Aaron Turon | 01h 01m |
Argues that feelings are information to be noticed, named, validated and metabolized rather than obstacles, and links childhood parenting patterns to adult… | ||
| The Lean Researcher | Alastair F. Donaldson | 46m |
Argument links Lean Startup rules to research and gives concrete, checkable examples: GPUVerify starts as manual two‑thread translations into Boogie and Z3 to… | ||
| Information Flow Types, Runtime Monitors, and Gradual Typing | Limin Jia | 47m |
Describes a concrete design that connects static information‑flow types and dynamic monitors: a two‑point lattice (L/H), typing rules that check explicit flows… | ||
| Reasoning in Higher-Order Concurrent Separation Logic | Amin Timany | 50m |
Iris program logic is a higher-order concurrent separation logic that produces a tailored program logic from an operational semantics and an adequacy theorem… | ||
| Think Abstractly, Work Concretely | Ichiro Hasuo | 52m |
Uses while dt programs that replace continuous flows by infinitesimal jumps and gives a semantics via hyperreals and an ultrafilter so formulas satisfy the… | ||
| Doing Research in PL panel | Greg Morrisett, Susan Eisenbach, Sam Lindley, Jeehoon Kang, Delphine Demange | 52m |
Recent concrete work reported includes a postdoc-built prototype that replaces P4’s hand‑rolled state‑machine parsers with a compositional parser design, a… | ||
| making your way in a changing world | Sophia Drossopoulou | 46m |
Career memoir gives concrete hits: develops an algorithmic type system that consumes five years chasing proof before abandoning it, models parameterized… | ||
| Numbers, Logic, and Decidability for Cyber-Physical Systems | Rupak Majumdar | 52m |
Encoding bounded-time reachability for linear ODEs into the first-order theory of the reals reduces the verification problem to satisfiability in a logic with… | ||
| Structural Language Models of Code | Eran Yahav | 01h 01m |
Describes a production-ready method that models code as AST paths and trains a structural language model used for name prediction, caption generation and… | ||
| A Programmable Cloud: CALM Foundations and Open Challenges | Joe Hellerstein | 01h 11m |
Argues that a proven equivalence — CALM Theorem — makes a program coordination-free exactly when it is monotonic, and shows formal tools used: Bloom/Dedalus… | ||
| Dynamical Systems and Program Analysis | James Worrell | 56m |
Algorithmic verdicts: termination of deterministic linear-update loops is decidable over the reals and rationals and (recently) decidable over the integers for… | ||
| The road to a Universal Internet Machine | Rachid Guerraoui | 01h 02m |
Claim: building a widely distributed universal computer loses Turing universality unless consensus is available, but many real tasks don’t need consensus… | ||
| Verifying a compiler through equational means | Yannick Zakowski | 01h 06m |
A machine-checked methodology builds a compositional, equational semantics for an LLVM-like IR using Interaction Trees and a formal IR called VIR/Vellvm… | ||
| Session with the Coq Development Team | Matthieu Sozeau, Enrico Tassi | 46m |
Coq 8.13 ships with a new warning for hints and a staged migration: marking hints global preserves old behavior while the default will flip later, so compile… | ||
| A Limited Case for Reification by Type Inference | Jason Gross | 14m |
Claims that Coq’s notation system plus type inference can perform reification for a restricted class of problems, specifically extracting the curried argument… | ||
| Towards a Coq Specification for Generalized Algebraic Datatypes in OCaml | Xuanrui Qi, Jacques Garrigue | 15m |
A Coq mechanization of OCaml-style GADTs targets a core language with structural polymorphism, recursive types and type-level equality witnesses (OCaml 4.11)… | ||
| Automated Synthesis of Verified Firewalls | Shardul Chiplunkar, Clément Pit-Claudel, Adam Chlipala | 12m |
Claim of correct-by-construction, stateful TCP/IP packet filters implemented as a verified compiler in Coq using the Fiat refinement framework and the… | ||
| Verification of Algorithm and Code Generation for Signal Transforms | Patrick Brinich, Jeremy Johnson | 14m |
Coq-verified subset of SPIRAL formalizes SPL matrix semantics and proves rewrite rules preserve matrices (including a mechanized Cooley–Tukey factorization… | ||
| An experience report on writing usable DSLs in Coq | Clément Pit-Claudel, Thomas Bourgeat | 10m |
A report on building a hardware DSL in Coq: the codebase totals a few thousand lines of Coq and hundreds of lines of notations; Coq 8.9 custom entries let the… | ||
| Record Updates in Coq | Tej Chajed | 10m |
Implements record updates in Coq by generating setters via type class resolution and Ltac: a Ltac procedure solve_setter extracts an ada_expansion (eval hnf)… | ||
| An Abstract Interpretation for SPMD Divergence on Reducible Control Flow Graphs | Julian Rosemann, Sebastian Hack, Simon Moll | 23m |
Presents an abstract interpretation for uniformity that handles reducible CFGs, with a largely Coq mechanized proof of correctness and an LLVM prototype… | ||
| Abstracting Gradual Typing Moving Forward : Precise and Space-Efficient | Felipe Bañados Schwerter, Alison M. Clark, Ronald Garcia, Khurram A. Jafery | 19m |
AGT gets two concrete fixes: a new evidence abstraction called bounded rows and records makes consistent evidence composition forward-complete, which prevents… | ||
| A Graded Dependent Type System with a Usage-Aware Semantics | Harley D. Eades III, Pritam Choudhury, Stephanie Weirich, Richard A. Eisenberg | 31m |
Presents Grad, a dependent type calculus with natural-number grades and separate demand contexts for terms and types, plus a heap-based reduction using graded… | ||
| A Computational Interpretation of Compact Closed Categories | Chao-Hong Chen, Amr Sabry | 24m |
Extends a reversible isomorphism language with negative types (a backward-direction effect) and pointed fractional types (indexed GC tokens that can raise… | ||
| A Practical Mode System for Recursive Definitions | Jeremy Yallop, Gabriel Scherer, Alban Reynaud | 35m |
A static mode system that classifies recursive bindings as safe or vicious and is proven sound against the Nordlander–Carlsson–Gill source semantics. It gives… | ||
| Generating Correctly Rounded Math Libraries for New Floating Point Variants | Jay P. Lim, Mridul Aanjaneya, John Gustafson, Santosh Nagarakatte | 26m |
Generates polynomials that approximate the correctly rounded value (not the real value) and encodes coefficient constraints as an LP-formulated constraints… | ||
| A Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis | Vineet Rajani, Marco Gaboardi, Jan Hoffmann, Deepak Garg | 23m |
Presents λ-amor, an affine type theory that adds a modal potential type plus a graded cost monad and refinements, and proves soundness with a Kripke… | ||
| A Pre-Expectation Calculus for Probabilistic Sensitivity | Gilles Barthe, Joost-Pieter Katoen, Christoph Matheja, Benjamin Lucien Kaminski, Alejandro Aguirre, Justin Hsu | 29m |
A relational pre-expectation calculus gives computable upper bounds on the Kantorovich lifting of output distributions, proved sound and (in cases) continuous… | ||
| A Separation Logic for Effect Handlers | Paulo Emílio de Vilhena, François Pottier | 25m |
Introduces a Separation Logic that embeds protocols into Iris-style weakest preconditions to specify and verify programs using user-defined effect handlers… | ||
| Automata and Fixpoints for Asynchronous Hyperproperties | Markus Müller-Olm, Christoph Ohrem, Jens Oliver Gutsfeld | 22m |
Introduces Hμ (a linear-time μ-calculus with named path quantifiers and indexed nexts) and Alternating Asynchronous Parity Automata as concrete tools, proves a… | ||
| Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade | Marco Vassena, Dean Tullsen, Klaus von Gleissenthall, Craig Disselkoen, Ranjit Jhala, Deian Stefan, Sunjay Cauligi, Rami Gökhan Kıcı | 16m |
Blade automatically finds data-flow paths from memory reads that can speculatively carry secrets to cache-leaking sinks, models them with a transient vs stable… | ||
| A Verified Optimizer for Quantum Circuits | Michael Hicks, Robert Rand, Shih-Han Hung, Xiaodi Wu, Kesha Hietala | 29m |
VOQC is a fully verified optimizer for quantum circuits implemented in the Coq proof assistant over the SQIR intermediate language; all transformations are… | ||
| Automatic Differentiation in PCF | Damiano Mazza, Michele Pagani | 30m |
Proves that automatic differentiation on PCF with reals (higher-order, Turing-complete) is correct except on a Lebesgue-measure-zero set: forward and reverse… | ||
| Context-Bounded Verification of Liveness for Multithreaded Shared-Memory Programs | Ramanathan S. Thinniyam, Pascal Baumann, Georg Zetzsche, Rupak Majumdar | 26m |
Shows that K‑context‑bounded fair termination for recursive multithreaded shared‑memory programs is decidable by reducing to reachability in Petri nets… | ||
| Combining Top-down Propagation and Bottom-up Enumeration for Inductive Synthesis | Woosuk Lee | 28m |
Combines top-down propagation with bottom-up enumeration to generate small component expressions and compose them into full programs; implements this in Duet… | ||
| Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification | David Van Horn, Phúc C. Nguyễn, Cameron Moy, Sam Tobin-Hochstadt | 23m |
Tool extracts Type Racket’s boundary contracts, runs the SCV symbolic verifier on the untyped client code, and selectively bypasses only those runtime checks… | ||
| Cyclic Proofs, System T, and the Power of Contraction | Laureline Pinault, Damien Pous, Denis Kuperberg | 29m |
The paper studies a cyclic proof system C built over regular-expression types (inspired by linear logic and non-wellfounded proofs) and interprets C-proofs as… | ||
| Data Flow Refinement Type Inference | Thomas Wies, Zvonimir Pavlinovic, Yusen Su | 24m |
DRIFT is a parametric abstract-interpretation framework that produces refinement-type systems and an inference algorithm; it implements numerical domains via… | ||
| Debugging Large-Scale Datalog: A Scalable Provenance Evaluation Strategy | Bernhard Scholz, David Zhao, Pavle Subotic | 26m |
A bottom-up evaluation augments Soufflé relations with proof annotations (rule id + minimal proof-tree height) so the engine computes and updates heights… | ||
| Deciding Accuracy of Differential Privacy Schemes | Rohit Chadha, A. Prasad Sistla, Mahesh Viswanathan, Paul Krogmeier, Gilles Barthe | 28m |
Introduces accuracy as a parametric notion based on distance to disagreement (dd) and output closeness γ, yielding an explicit alpha–beta–gamma claim: e.g. for… | ||
| Deciding Reachability under Persistent x86-TSO | Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan | 30m |
Shows that reachability for the persistent x86-TSO (Px86) model is decidable reachability by giving a new semantics equivalent to Raad et al.’s Px86 that is a… | ||
| Formally Verified Speculation and Deoptimization in a JIT Compiler | Jan Vitek, Olivier Flückiger, Sandrine Blazy, David Pichardie, Aurèle Barrière | 23m |
A formal model defines a JIT’s middle end, an RTL-like IR and two concrete speculative ops: the anchor instruction which marks safe deoptimization points and… | ||
| Deciding ω-Regular Properties on Linear Recurrence Sequences | Joël Ouaknine, Toghrul Karimov, Shaull Almagor, Edon Kelmendi, James Worrell | 30m |
A procedure inputs a prefix‑independent ω‑regular condition and a linear recurrence sequence and decides whether the sequence’s sign word satisfies it, but… | ||
| Dijkstra Monads Forever | Lucas Silver, Steve Zdancewic | 25m |
Extends Dijkstra monads to termination‑sensitive specifications for interactive, possibly nonterminating programs by adding two base spec monads (a delay spec… | ||
| Diamonds Are Not Forever: Liveness in Reactive Programming with Guarded Recursion | Patrick Bahr, Christian Uldal Graulund, Rasmus Ejlers Møgelberg | 29m |
A new language called Lively RaTT combines guarded recursion with an inductive until type (e.g. diamond = unit until a) by treating the temporal circle… | ||
| Distributed Causal Memory for Higher-Order Distributed Separation Logic | Amin Timany, Lars Birkedal, Abel Nieto, Léon Gondelman, Simon Oddershede Gregersen | 18m |
Presents the first full specification and machine-checked verification of a causally-consistent distributed database implementation and client libraries… | ||
| Efficient, Provable Local Capability Revocation using Uninitialized Capabilities | Aina Linn Georges, Lars Birkedal, Dominique Devriese, Alix Trieu, Armaël Guéneau, Amin Timany, Thomas Van Strydonck, Sander Huyghebaert | 29m |
Proposes uninitialized capabilities that give write-only access to an uninitialized stack region and require overwriting before any read, implemented with… | ||
| egg: Fast and Extensible Equality Saturation | Max Willsey, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, Chandrakana Nandi, Pavel Panchekha | 30m |
Equality saturation is implemented as the egg Rust library, which applies rewrites into an e-graph and then runs a single rebuild once per iteration rather… | ||
| Fully Abstract from Static to Gradual | Dominique Devriese, Koen Jacobs, Amin Timany | 27m |
Proposes that the embedding from static into gradual languages must be fully abstract embedding — it preserves and reflects contextual equivalence — and shows… | ||
| Generating Collection Transformations from Proofs | Michael Benedikt, Pierre Pradic | 21m |
A procedure converts constructive proofs of functionality for bounded delta0 specifications into concrete nested relational calculus programs, running in… | ||
| Functorial Semantics for Partial Theories | Fosco Loregian, Chad Nester, Ivan Di Liberti, Pawel Sobocinski | 27m |
Provides a Lawvere-style syntax for theories with partially defined operations by replacing cartesian string diagrams with string diagrams for partial maps… | ||
| Intensional Datatype Refinement | Steven Ramsay, Eddie Jones | 29m |
A refinement type system verifies that pattern-match failures cannot occur by adding finitely many constructor-subset refinements and solving set constraints… | ||
| Giving Semantics to Program-Counter Labels via Secure Effects | Ethan Cecchetti, Andrew K. Hirsch | 22m |
Provides monadic semantics for program-counter labels by translating type-and-effect languages into pure ones using indexed monads and a more general productor… | ||
| Intersection Types and (Positive) Almost-Sure Termination | Simona Ronchi Della Rocca, Ugo Dal Lago, Claudia Faggian | 24m |
Intersection types exactly characterize two probabilistic termination notions: the probability of convergence equals the least upper bound of norms of certain… | ||
| Internalizing Representation Independence with Univalence | Evan Cavallo, Carlo Angiuli, Max Zeuner, Anders Mörtberg | 23m |
Proves a concrete method to internalize representation independence inside dependent type theory by combining univalence as a computable ua with higher… | ||
| Learning the Boundary of Inductive Invariants | James R. Wilcox, Yotam M. Y. Feldman, Sharon Shoham, Mooly Sagiv | 18m |
An interpolation-based invariant inference algorithm with model-based generalization (dropping literals) uses bounded model checking to implement membership… | ||
| Intrinsically Typed Compilation with Nameless Labels | Robbert Krebbers, Arjen Rouvoet, Eelco Visser | 25m |
Claims a compositional way to intrinsically type bytecode by replacing global names with nameless labels and a co-contextual interface algebra, implemented as… | ||
| Modeling and Analyzing Evaluation Cost of CUDA Kernels | Jan Hoffmann, Stefan K. Muller | 26m |
Paper presents a quantitative program logic and cost semantics for CUDA that are formalized in Coq formalization and implemented as the prototype tool vercuta… | ||
| On Algebraic Abstractions for Concurrent Separation Logics | Anindya Banerjee, František Farka, Germán Andrés Delbianco, Aleksandar Nanevski, Ignacio Fábregas | 26m |
Defines morphisms of PCMs and separating relations as the concrete algebraic machinery that preserves ownership across parallel composition, then uses them to… | ||
| Mechanized Logical Relations for Termination-Insensitive Noninterference | Simon Oddershede Gregersen, Johan Bay, Lars Birkedal, Amin Timany | 19m |
Paper proves that a rich information‑flow type system (recursive and existential types, System F impredicative polymorphism, label polymorphism, higher‑order… | ||
| On the Complexity of Bidirected Interleaved Dyck-Reachability | Yuanbo Li, Qirun Zhang, Thomas Reps | 26m |
Shows that bidirected InterDyck reachability is decidable for D1 ⊙ D1 and gives a concrete polynomial-time algorithm that computes all pairs reachable by… | ||
| Optimal Prediction of Synchronization-Preserving Races | Umang Mathur, Andreas Pavlogiannis, Mahesh Viswanathan | 18m |
Paper gives a sound and complete algorithm SyncP that predicts synchronization-preserving races and runs in Õ(N) time and space on a trace of length N, with a… | ||
| On the Semantic Expressiveness of Recursive Types | Marco Patrignani, Eric Mark Martin, Dominique Devriese | 23m |
Paper proves iso-recursive types, equirecursive types, and a term-level fix are semantically equivalent by constructing three fully abstract compilers… | ||
| Paradoxes of probabilistic programming | Jules Jacobs | 24m |
Probabilistic programs that multiply weights by pdfs produce unit errors and paradoxes: a simple height example gives 1.75 normally but a coin-conditional… | ||
| PerSeVerE: Persistency Semantics for Verification under Ext4 | Ilya Kaysin, Viktor Vafeiadis, Michalis Kokologiannakis, Azalea Raad | 28m |
Formal semantics for ext4 are derived from the kernel implementation and stress tests and integrated with C/C++ weak-memory models; a model-checker then… | ||
| Precise Subtyping for Asynchronous Multiparty Sessions | Silvia Ghilezan, Nobuko Yoshida, Ivan Prokić, Jovanka Pantović, Alceste Scalas | 23m |
First formalization of precise subtyping for asynchronous multiparty sessions that proves both soundness (safe replacement) and completeness (no larger… | ||
| Petr4: Formal Foundations for P4 Data Planes | Samwise Parkinson, Amanda Xu, Rudy Peterson, Ryan Doenges, Alexander Chang, Alaia Solko-Breslin, Nate Foster, Newton Ni, Mina Tahmasbi Arashloo, Santiago Bautista | 27m |
Petr4 provides a clean‑slate definitional interpreter and a compact core calculus that models a P4 fragment, validated by running over 750 tests from the P4… | ||
| Probabilistic Programming Semantics for Name Generation | Michael Wolman, Sam Staton, Marcin Sabok, Dario Stein | 20m |
Claims a concrete semantics: quasi-Borel spaces interpret the ν-calculus by mapping name generation to Gaussian sampling, and the model is fully abstract at… | ||
| Provably Space Efficient Parallel Functional Programming | Sam Westrick, Umut A. Acar, Jatin Arora | 24m |
Proves that determinacy‑race‑free parallel ML runs need at most O(R · P) space and at most O(W + R · P) work by integrating a heap scheduler with… | ||
| Relatively Complete Verification of Probabilistic Programs | Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja | 30m |
Defines a compact grammar for non‑negative real‑valued assertions (rationals, addition, multiplication, truncated subtraction, guarded expectations, scaling… | ||
| Semantics-Guided Synthesis | Jinwoo Kim, Loris D'Antoni, Qinheping Hu, Thomas Reps | 30m |
Framework that takes a grammar, a big‑step semantics expressed as Constrained Horn Clauses, and examples or formulas as specs, then reduces synthesis to CHC… | ||
| Taming x86-TSO Persistency | Ori Lahav, Artem Khyzha | 26m |
Proposes a new synchronous PTSO model that eagerly persists writes and proves it reaches the same non‑volatile states as the asynchronous POPL’20 model — a… | ||
| Simplifying Multiple-Statement Reductions with the Polyhedral Model | Cambridge Yang, Eric Atkinson, Michael Carbin | 24m |
Paper formalizes simplifying dependent reductions as an integer bilinear program over reuse vectors and polyhedral schedules and shows it is hard to solve… | ||
| The (In)Efficiency of Interaction | Beniamino Accattoli, Gabriele Vanoni, Ugo Dal Lago | 21m |
Compares four token-based abstract machines and proves precise time gaps: YAM (geometry of interaction) can be exponentially slower than Curien’s environment… | ||
| The Fine-Grained and Parallel Complexity of Andersen's Pointer Analysis | Anders Alnor Mathiasen, Andreas Pavlogiannis | 22m |
Establishes an O(n^3) optimal algorithm for Andersen-style inclusion-based pointer analysis and a matching Ω(n^3) lower bound for even on-demand queries via a… | ||
| The Taming of the Rew: A Type Theory with Computational Assumptions | Jesper Cockx, Nicolas Tabareau, Théo Winterhalter | 28m |
Rewriting Type Theory lets users add user-defined rewrite rules as computational assumptions that the type checker applies automatically, not as… | ||
| Verifying Correct Usage of Context-Free API Protocols | Kostas Ferles, Jon Stephens, Isil Dillig | 18m |
CFPChecker verifies context-free grammar API protocols by over-approximating program API sequences with a CFG, checking language inclusion, and running… | ||
| Verified Code Generation for the Polyhedral Model | Nathanaëlle Courant, Xavier Leroy | 23m |
A formally verified code generator turns a polyhedral IR into sequential counted loops and is mechanized in Coq producing about 8k lines of development; it… | ||
| Verifying Observational Robustness Against a C11-style Memory Model | Roy Margalit, Ori Lahav | 23m |
Proves robustness against the C11-style model is decidable (PSPACE-complete) by a concrete reduction to SC reachability, implements that instrumentation in the… | ||
| The Taming of the Rew: A Type Theory with Computational Assumptions | Jesper Cockx, Nicolas Tabareau, Théo Winterhalter | 28m |
Adds Rewriting Type Theory to dependently typed systems so user-supplied rewrite rules run automatically during typechecking instead of requiring explicit… | ||
| λS: Computable Semantics for Diff'ble Programming with HO Functions and Datatypes | Jesse Michel, Michael Carbin, Benjamin Sherman | 30m |
A new differentiable programming semantics, λS, gives computable meanings for higher-order derivatives and for nondifferentiable ops via the Clarke derivative… | ||
| nothing matches | ||