POPL 2023
2023-01-15..2023-01-21
Boston, United States
POPL ·
[POPL 2021, POPL 2022, POPL 2022 Virtual Workshop, POPL 2023, POPL 2023 SRC, POPL 2024, POPL 2025, POPL 2026]
who it's for
programming language researchers, formal verification engineers, proof assistant users, language designers, compiler developers, systems programmers, security researchers
topics
separation-logic refinement types; Coq mechanized proofs; memory-safe WebAssembly extensions; effectful JIT native code generation; iso-recursive subtyping algorithms; linearly typed deadlock-free locks; probabilistic resource-aware session types; quantitative inhabitation frameworks; dynamic race detection with O(1) samples; symbolic compilation as a library
| title | author | length |
|---|---|---|
| Higher-Order Leak and Deadlock Free Locks | Jules Jacobs, Stephanie Balzer | 26m |
Presents a linearly typed lambda calculus that enforces both deadlock and memory-leak freedom for first-class, nestable locks, proving that well-typed programs… | ||
| Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-a... | Taro Sekiyama, Hiroshi Unno | 25m |
Extends a temporal type-and-effect system to handle delimited continuations (shift0/reset0) by tracking how continuations change the observable trace — the key… | ||
| Recursive Subtyping for All | Litao Zhou, Yaoda Zhou | 25m |
Presents F_{≤}^{μ}, a kernel F_{≤} extension that adds iso-recursive types plus nominal unfolding rules and new structural folding/unfolding rules, and proves… | ||
| A High-Level Separation Logic for Heap Space under Garbage Collection | Alexandre Moine, Arthur Charguéraud, François Pottier | 23m |
Logic gives a concrete way to prove heap-space bounds under a GC that follows the free-variable rule: allocation consumes space credits, deallocation returns… | ||
| CN: Verifying Systems C Code with Separation-Logic Refinement Types | Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, Neel Krishnaswami | 24m |
CN is a separation-logic refinement type system for ISO C that uses a Cerberus translation to a core language, implements resource types as first-class… | ||
| Conditional Contextual Refinement | Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Sammler, Derek Dreyer | 24m |
A new refinement notion, Conditional Contextual Refinement (CCR), combines separation-logic pre/post conditions with transitive contextual refinement by… | ||
| MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code | Alexandra E. Michael, Anitha Gollamudi, Jay Bosamiya, Evan Johnson, Aidan Denlinger, Craig Disselkoen, Conrad Watt, Bryan Parno, Marco Patrignani, Marco Vassena, Deian Stefan | 25m |
Extends Wasm with segmented memory and unforgeable handles that carry colored provenance, a formal semantics, and a proof that well-typed MSWasm modules are… | ||
| Reconciling Shannon and Scott with a Lattice of Computable Information | Sebastian Hunt, Dave Sands, Sandro Stucki | 24m |
Introduces a concrete construction called the Lattice of Computable Information whose elements are complete preorders (equivalence classes ordered by… | ||
| A Core Calculus for Equational Proofs of Cryptographic Protocols | Joshua Gancher, Kristina Sojakova, Xiong Fan, Elaine Shi, Greg Morrisett | 26m |
Introduces a tiny process calculus and an equation-of-logic that proves observational equivalence for distributed crypto by rewriting networks of probabilistic… | ||
| DimSum: A Decentralized Approach to Multi-language Semantics and Verification | Michael Sammler, Simon Spies, Youngju Song, Emanuele D'Osualdo, Robbert Krebbers, Deepak Garg, Derek Dreyer | 25m |
DimSum presents a decentralized method that avoids fixing a source language, memory model, or closed set of languages by giving each language a… | ||
| Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCe... | Aurèle Barrière, Sandrine Blazy, David Pichardie | 24m |
Prototype JIT is implemented and mechanically verified in Coq, reusing the CompCert backend and its correctness proofs to generate x86 code, and modeling… | ||
| Dargent: A Silver Bullet for Verified Data Layout Refinement | Zilin Chen, Ambroise Lafont, Liam O'Connor, Gabriele Keller, Craig McLaughlin, Vincent Jackson, Christine Rizkallah | 23m |
Dargent provides a declarative layout language integrated into Cogent that generates verified C getters and setters so algebraic types map to bit-precise… | ||
| A Type-Based Approach to Divide-and-Conquer Recursion in Coq | Benjamin Delaware, Alex Hubers, Chris Jenkins, J. Garrett Morris, Aaron Stump | 24m |
Presents a type-level interface that encodes divide-and-conquer recursion as Mendler-style algebras, implemented in Coq and expressible in System F_omega plus… | ||
| Elements of Quantitative Rewriting | Francesco Gavazzo, Cecilia Di Florio | 22m |
Defines rewriting over quantales and proves metric versions of Newman and Church‑Rosser plus critical‑pair lemmas, with concrete counterexamples showing… | ||
| The Geometry of Causality: Multi-token Geometry of Interaction and Its Causal Un... | Simon Castellan, Pierre Clairambault | 25m |
A compositional interpreter builds a multi-token machine for Idealized Parallel Algol and implements terms as coloured Petri nets that run concurrent tokens… | ||
| Deconstructing the Calculus of Relations with Tape Diagrams | Filippo Bonchi, Alessandro Di Giorgio, Alessio Santamaria | 23m |
Constructs a concrete diagrammatic syntax — tape diagrams — that embeds ordinary string diagrams inside a second layer and claims a full completeness theorem… | ||
| Probabilistic Resource-Aware Session Types | Ankush Das, Di Wang, Jan Hoffmann | 26m |
Extends binary session types to describe message probability distributions and to infer expected-resource bounds automatically, using a type reconstruction… | ||
| A Calculus for Amortized Expected Runtimes | Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Lena Verscht | 22m |
Develops a weakest-precondition-style aert calculus that composes the potential method with an extended ert for dynamic memory using runtime separation logic… | ||
| A General Noninterference Policy for Polynomial Time | Emmanuel Hainry, Romain Péchoux | 25m |
New noninterference policy claims an exact characterization: programs that are stratified and strongly normalizing compute exactly FP, strictly extending… | ||
| Admissible Types-to-PERs Relativization in Higher-Order Logic | Andrei Popescu, Dmitriy Traytel | 28m |
Proves that for a large practical fragment of HOL (including datatypes and codatatypes) a types-to-PERs relativization is admissible: if a type-based theorem… | ||
| An Order-Theoretic Analysis of Universe Polymorphism | Kuen-Bang Hou (Favonia), Carlo Angiuli, Reed Mullanix | 24m |
Claims that universe polymorphism equals monads on strict partial orders and that every usable universe hierarchy embeds into newly defined displacement… | ||
| Impredicative Observational Equality | Loïc Pujet, Nicolas Tabareau | 23m |
Extends observational TTobs with an impredicative universe of definitionally proof‑irrelevant types and implements transport via a type‑casting/observational… | ||
| A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F... | Nick Rioux, Xuejing Huang, Steve Zdancewic | 24m |
Presents F⋈, a small core language that lets intersection types, union types and overloaded functions coexist with a deterministic merge operator by enforcing… | ||
| Making a Type Difference: Subtraction on Intersection Types as Generalized Recor... | Han Xu, Xuejing Huang | 19m |
Defines a general type difference operator that extends record restriction to intersection, function and other types, gives an algorithm (deterministic) driven… | ||
| Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework | Victor Arrial, Giulio Guerrieri, Delia Kesner | 22m |
Proves decidability of inhabitation for a unifying calculus lambda! by using non-idempotent intersection types to extract quantitative bounds (reduction length… | ||
| Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Ch... | Alejandro Aguirre, Lars Birkedal | 25m |
Paper defines operational notions of may- and must-termination as optimal and pessimal termination probabilities, and builds step-indexed logical relations… | ||
| Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in C... | Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, Steve Zdancewic | 24m |
Introduces a coinductive tree datatype and a ctrees monad in Coq that models nondeterminism, recursion, and effects by three node kinds: external events and… | ||
| Hefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects | Casper Bach Poulsen, Cas van der Rest | 17m |
Presents Hefty algebras that elaborate higher‑order operations into primitive algebraic effects while preserving modularity so handlers can be swapped without… | ||
| Tail Recursion Modulo Context: An Equational Approach | Daan Leijen, Anton Lorenzen | 27m |
Generalizes tail recursion modulo cons into a general TRMC algorithm derived from an equational specification, requiring four instantiation operations and… | ||
| Taking Back Control in an Intermediate Representation for GPU Computing | Vasileios Klimis, Jack Clark, Alan Baker, David Neto, John Wickerson, Alastair F. Donaldson | 27m |
Formal modeling of SPIR-V control flow encodes the rules in an Alloy model, replaces brittle dominance rules with structural dominance that counts control… | ||
| Executing Microservice Applications on Serverless, Correctly | Konstantinos Kallas, Haoran Zhang, Rajeev Alur, Sebastian Angel, Vincent Liu | 24m |
mu2sls is a Python framework that instruments service classes with transactions and asynchronous calls and emits serverless functions plus a logging and… | ||
| An Operational Approach to Library Abstraction under Relaxed Memory Concurrency | Abhishek Kr Singh, Ori Lahav | 23m |
Claims a library-abstraction theorem for RC11-style weak memory by giving an operational semantics exposing knowledge propagation that records propagation… | ||
| The Path to Durable Linearizability | Emanuele D'Osualdo, Azalea Raad, Viktor Vafeiadis | 25m |
Proposes a concrete method that converts an existing linearizability proof into durable correctness by adding small, checkable Delta proof obligations that… | ||
| A Compositional Theory of Linearizability | Arthur Oliveira Vale, Zhong Shao, Yixuan Chen | 24m |
Presents a concrete reformulation of linearizability derived from a base concurrent model via the Karoubi envelope, producing a compositional model by… | ||
| Locally Nameless Sets | Andrew M. Pitts | 25m |
Presents a concrete claim and proofs: equational axiomatization of opening and closing (nine axioms, effectively five independent axioms) lets freshness and… | ||
| Why Are Proofs Relevant in Proof-Relevant Models? | Axel Kerinec, Giulio Manzonetto, Federico Olimpieri | 23m |
Categorifying relational graph models using distributors yields categorified graph models whose denotations are distributors returning full type derivations… | ||
| Towards a Higher-Order Mathematical Operational Semantics | Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, Henning Urbat | 24m |
Defines pointed higher-order GSOS laws as dinatural transformations that take syntax as an endofunctor and higher-order behavior as a bifunctor, replacing… | ||
| Welcome to POPL'23 | Andrew C. Myers, Amal Ahmed | 07m |
Conference opens on the 50th POPL with over 500 in-person attendees (700 counting co-located events) and a technical program of 74 papers from 275 submissions… | ||
| Principles of Persistent Programming | Viktor Vafeiadis | 01h 03m |
Defines a formal semantics that composes weak-memory consistency with a separate persistency order, gives both operational and declarative characterizations… | ||
| Kater: Automating Weak Memory Model Metatheory and Consistency Checking | Michalis Kokologiannakis, Ori Lahav, Viktor Vafeiadis | 26m |
Kater reduces meta theoretic questions about axiomatic weak memory models to language inclusion between CAT expressions, proving decidability for a wide class… | ||
| Stratified Commutativity in Verification Algorithms for Concurrent Programs | Azadeh Farzan, Dominik Klumpp, Andreas Podelski | 23m |
Defines a formal framework for abstract commutativity relations with a simple soundness condition and an automatic method to derive such relations from a… | ||
| A Partial Order View of Message-Passing Communication Models | Cinzia Di Giusto, Davide Ferre', Laetitia Laversa, Etienne Lozes | 22m |
Presents a unified hierarchy of seven communication models from fully asynchronous to realizable with synchronous communication and proves each model is MSO… | ||
| On the Expressive Power of String Constraints | Joel D. Day, Vijay Ganesh, Nathan Grewal, Florin Manea | 28m |
Classifies 20 string-logics built from concatenation, word-equality, length arithmetic and language membership and shows which express which formal languages… | ||
| A Robust Theory of Series Parallel Graphs | Rajeev Alur, Caleb Stanford, Christopher Watson | 24m |
Defines synchronized series-parallel graphs (SSPG) as two-terminal DAGs with sequential and unordered parallel composition plus a synchronization edge, and… | ||
| Inductive Synthesis of Structurally Recursive Functional Programs from Non-recur... | Woosuk Lee, Hangyeol Cho | 25m |
Synthesizes structurally recursive ML-style functions from input-output examples by first enumerating all nonrecursive straight-line expressions per example… | ||
| FlashFill++: Scaling Programming by Example by Cutting to the Chase | José Pablo Cambronero, Sumit Gulwani, Vu Le, Daniel Perelman, Arjun Radhakrishna, Clint Simon, Ashish Tiwari | 25m |
FlashFill++ introduces cut functions, guarded DSLs, and middle-out synthesis to scale programming-by-example to a large DSL with date/time and numeric… | ||
| Unrealizability Logic | Jinwoo Kim, Loris D'Antoni, Thomas Reps | 27m |
A Hoare-style proof system called unrealizability logic gives checkable proofs that a synthesis search space has no solution, overapproximating infinite sets… | ||
| Affine Monads and Lazy Structures for Bayesian Programming | Swaraj Dash, Younesse Kaddar, Hugo Paquet, Sam Staton | 26m |
Argues that infinite-dimensional Bayesian models (Poisson, Gaussian, Dirichlet, Beta, jump processes) are naturally expressed with lazy streams and infinite… | ||
| Type-Preserving, Dependence-Aware Guide Generation for Sound, Effective Amortize... | Jianlin Li, Leni Ven, Pengyuan Shi, Yizhou Zhang | 23m |
An automatic guide synthesizer generates neural-guide programs by a type-preserving, dependence-aware translation that guarantees mutual absolute continuity… | ||
| Smoothness Analysis for Probabilistic Programs with Application to Optimised Var... | Wonyeol Lee, Xavier Rival, Hongseok Yang | 28m |
A static analysis discovers which fragments of a probabilistic program are differentiable and which are not, then applies the pathwise gradient estimator to… | ||
| Panel: Next 50 Years of POPL | Derek Dreyer, Michael Carbin, Nate Foster, Xavier Leroy, Benjamin C. Pierce, Nadia Polikarpova, Azalea Raad, Sharon Shoham | 01h 03m |
Panel discussion surveys POPL's past and future with concrete examples and tensions: cites FlashFill and program synthesis, the 1976 abstract interpretation… | ||
| babble: Learning Better Abstractions with E-Graphs and Anti-unification | David Cao, Rose Kunkel, Chandrakana Nandi, Max Willsey, Zachary Tatlock, Nadia Polikarpova | 22m |
Presents Library Learning Modulo Theory (LLMT) implemented as the tool babble, which uses e-graphs plus a new e-graph anti-unification algorithm and targeted… | ||
| Combining Functional and Automata Synthesis to Discover Causal Reactive Programs | Ria Das, Joshua B. Tenenbaum, Armando Solar-Lezama, Zenna Tavares | 24m |
Algorithm converts sequences of video frames plus actions into Autumn programs by iterating functional synthesis (fit per-object update functions from an… | ||
| Comparative Synthesis: Learning Near-Optimal Network Designs by Query | Yanjun Wang, Zixuan Li, Chuan Jiang, Xiaokang Qiu, Sanjay Rao | 24m |
Framework learns an implicit objective by asking the user Compare or Propose queries and returns a near-optimal allocation after a small budget (ten) of… | ||
| Top-Down Synthesis for Library Learning | Matt Bowers, Theo X. Olausson, Lionel Wong, Gabriel Grand, Joshua B. Tenenbaum, Kevin Ellis, Armando Solar-Lezama | 24m |
Paper introduces corpus-guided top-down synthesis that builds abstractions by expanding holes and using branch-and-bound pruning with quick upper bounds… | ||
| SSA Translation Is an Abstract Interpretation | Matthieu Lemerre | 26m |
Claim: SSA translation is an abstract interpretation and can be implemented as a simple dataflow analysis that is sound and complete, avoids dominance-based… | ||
| Dynamic Race Detection with O(1) Samples | Mosaad Al Thokair, Minjian Zhang, Umang Mathur, Mahesh Viswanathan | 23m |
Claims a randomized, one-sided property tester that samples O(1) samples (constant many events when thread and lock counts are fixed) and runs FastTrack on… | ||
| Statically Resolvable Ambiguity | Viktor Palmkvist, Elias Castegren, Philipp Haller, David Broman | 26m |
Presents a concrete solution that proves every ambiguous program in the supported formalism can be rewritten unambiguously, with a full Coq mechanization and… | ||
| You Only Linearize Once: Tangents Transpose to Gradients | Alexey Radul, Adam Paszke, Roy Frostig, Matthew J. Johnson, DOUGAL MACLAURIN | 25m |
Claim: reverse-mode AD is exactly forward-mode AD followed by unzipping the forward result into nonlinear and linear parts and then transposition of that… | ||
| Efficient Dual-Numbers Reverse AD via Well-Known Program Transformations | Tom J. Smeding, Matthijs I. L. Vákár | 23m |
Presents a semantics-preserving optimization path from naive dual-numbers reverse AD to an implementation with the expected time complexity and a practical… | ||
| ADEV: Sound Automatic Differentiation of Expected Values of Probabilistic Progra... | Alexander K. Lew, Mathieu Huot, Sam Staton, Vikash K. Mansinghka | 26m |
ADEV is a source-to-source extension of forward-mode AD that transforms a probabilistic program into another whose expected return equals the derivative of the… | ||
| When Less Is More: Consequence-Finding in a Weak Theory of Arithmetic | Zachary Kincaid, Nicolas Koh, Shaowei Zhu | 24m |
Presents a decidable first‑order theory called LIRR (linear integer/real with weak multiplication), a concrete axiomatization and an effective model… | ||
| Higher-Order MSL Horn Constraints | Jerome Jochems, Eddie Jones, Steven Ramsay | 23m |
Extends MSL to higher-order Horn constraints and gives a resolution-based decision procedure that preserves decidable satisfiability by introducing nested… | ||
| Fast Coalgebraic Bisimilarity Minimization | Jules Jacobs, Thorsten Wißmann | 26m |
Minimizes coalgebras (DFAs, transition systems, probabilistic/weighted automata) by repeatedly refining states via computed signatures and reusing unchanged… | ||
| Qunity: A Unified Language for Quantum and Classical Computing | Finn Voichick, Liyi Li, Robert Rand, Michael Hicks | 24m |
Qunity defines a unified syntax where sum types → direct sum implements operator sums, exception-handling → projective measurement expresses measurements, and… | ||
| Proto-Quipper with Dynamic Lifting | Peng Fu, Kohei Kishida, Neil Julien Ross, Peter Selinger | 20m |
Extends Proto-Quipper-M with dynamic lifting to let measurement bits become compile-time parameters, implements a new language Proto-Quipper-Dyn, and gives a… | ||
| CoqQ: Foundational Verification of Quantum Programs | Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, Mingsheng Ying | 22m |
CoqQ is a Coq framework that formalizes a quantum language, proves a program logic sound with respect to a denotational semantics built on MathComp and… | ||
| Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification | Hiroshi Unno, Tachio Terauchi, Yu Gu, Eric Koskinen | 26m |
Reduces μCLP validity to a predicate-constraint problem and leverages an existing solver to give a sound and relatively-complete decision method, then improves… | ||
| Optimal CHC Solving via Termination Proofs | Yu Gu, Takeshi Tsukada, Hiroshi Unno | 23m |
Presents a new optimality checker that reduces CHC maximality to program termination, encodes termination-argument synthesis (angelic strategy and… | ||
| From SMT to ASP: Solver-Based Approaches to Solving Datalog Synthesis-as-Rule-Se... | Aaron Bembenek, Michael Greenberg, Stephen Chong | 23m |
Presents a progression of four solver implementations — prosynth, monosynth, loopsynth, and ASPsynth — that move from CEGIS with provenance to a custom… | ||
| The Fine-Grained Complexity of CFL Reachability | Paraschos Koutris, Shaleen Deep | 26m |
Classifies exact polynomial exponents for CFL reachability under standard fine-grained conjectures (BMM, k-Clique, APSP, 3SUM): shows Dyck-2 Ω(n^{2.5}) lower… | ||
| Single-Source-Single-Target Interleaved-Dyck Reachability via Integer Linear Pro... | Yuanbo Li, Qirun Zhang, Thomas Reps | 25m |
Presents a single-source–single-target algorithm that summarizes all source→target paths as path expressions and reduces InterDyck reachability to a… | ||
| Context-Bounded Verification of Context-Free Specifications | Pascal Baumann, Moses Ganardi, Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche | 28m |
Shows that context-bounded refinement where the implementation is a multistack pushdown automaton and the specification is a Dyck or input‑deterministic… | ||
| An Algebra of Alignment for Relational Verification | Timos Antonopoulos, Eric Koskinen, Ton Chanh Le, Ramana Nagasamudram, David Naumann, Minh Ngo | 25m |
Extends Kleene Algebra with Tests into BiKAT and shows it exactly encodes lockstep and asynchronous product alignments so relational specs reduce to algebraic… | ||
| Grisette: Symbolic Compilation as a Functional Programming Library | Sirui Lu, Rastislav Bodík | 23m |
Grisette is a Haskell library that compiles programs symbolically by evaluating all paths and merging states into a normal form that avoids pairwise exclusive… | ||
| HFL(Z) Validity Checking for Automated Program Verification | Naoki Kobayashi, Kento Tanahashi, Ryosuke Sato, Takeshi Tsukada | 22m |
Proposes an automated validity checker for HFL(Z) formulas that encodes higher-order program verification (termination, nontermination, fair variants… | ||
| Witnessability of Undecidable Problems | Shuo Ding, Qirun Zhang | 22m |
Claim: for a wide class of undecidable problems there is a computable transformation that, given the code of any decidable approximation, outputs a concrete… | ||
| nothing matches | ||