POPL 2022
2022-01-16..2022-01-22
Philadelphia, United States
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
Welcome to the website of the 49th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2022). The annual Symposium on Principles of Programming Languages is a forum for the discussion of all aspects of programming languages and programming systems. Both theoretical and experimental papers are welcome, on topics ranging from formal frameworks to experience reports. We seek submissions that make principled, enduring contributions to the theory, design, understanding, implementation or application of programming languages. The symposium is sponsored by ACM SIGPLAN, in cooperati ...
who it's for
programming languages researchers, formal methods researchers, verification engineers, compiler engineers, language designers, theorem-prover developers, concurrency and parallelism researchers, systems and networking programmers
topics
separation logic for concurrency; termination reasoning for fine-grained concurrency; property-directed reachability as abstract interpretation; Dyck reachability algorithms; profile-guided optimization reconstruction; gradualization of dependent type theory; refinement types for Solidity overflow; symbolic evaluation with merging; dynamic partial order reduction; staged typed Template Haskell specification
| title | author | length |
|---|---|---|
| TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Pr | Emanuele D'Osualdo, Julian Sutherland, Azadeh Farzan, Philippa Gardner, Andrew C. Myers | 24m |
TaDA Live claims compositional proofs of termination for blocking fine‑grained concurrent programs by extending separation logic with a semantic model of… | ||
| Formal Metatheory of Second-Order Abstract Syntax | Marcelo Fiore, Dmitrij Szamozvancev | 30m |
An Agda-based generator turns a concise syntax signature into an Agda code generator that produces an intrinsically-encoded inductive datatype plus weakening… | ||
| Property-Directed Reachability as Abstract Interpretation in the Monotone Theory | Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, James R. Wilcox | 26m |
Claims that propositional PDR is an instance of abstract interpretation by defining Lambda-PDR (take all counterexample generalizations) and a logical abstract… | ||
| Coalgebra for the working programming languages researcher | Alexandra Silva | 58m |
Coalgebraic methods center on a functor that generates syntax, denotational and operational semantics, and equivalence proofs; from that one structure… | ||
| The Decidability and Complexity of Interleaved Bidirected Dyck Reachability | Adam Husted Kjelstrøm, Andreas Pavlogiannis | 18m |
Proves D1⟂D1 reachability runs in O(n^3 α(n)) time, improving on the prior O(n^7) bound; shows Dk⟂D1 reachability is decidable and its linearly bounded variant… | ||
| Learning Formulas in Finite Variable Logics | Paul Krogmeier, P. Madhusudan | 25m |
Decision procedures synthesize separating sentences, query formulas, and terms over finite structures for finite-variable logics (FO^k), FO^k with nested or… | ||
| Profile Inference Revisited | Wenlei He, Julian Mestre, Sergey Pupyrev, Lei Wang, Hongtao Yu | 22m |
Sampling-based PGO produces incomplete CFG counts and profile inference is NP-hard and hard to approximate, so a new algorithm called profi reconstructs vertex… | ||
| Reasoning about 'Reasoning about Reasoning' Semantics and Contextual Equivalence | Yizhou Zhang, Nada Amin | 22m |
Formal semantics for a core PPL with continuous distributions, scoring, nested queries and general recursion defines mutually recursive semantics so… | ||
| A Separation Logic for Negative Dependence | Jialu Bao, Marco Gaboardi, Justin Hsu, Joseph Tassarotti | 18m |
Design of LINA, a probabilistic separation logic that adds a second separating conjunction for negative dependence alongside the independence star, with… | ||
| Static Prediction of Parallel Computation Graphs | Stefan K. Muller | 24m |
Claims a new static abstraction, graph types, that compactly represent all runtime computation graphs and supports a Hindley-Milner–style inference algorithm… | ||
| One Polynomial Approximation to Produce Correctly Rounded Results of an Elementa | Jay P. Lim, Santosh Nagarakatte | 22m |
Claims a single polynomial, found by solving linear programs over rounding intervals, yields correctly rounded elementary-function results across multiple… | ||
| Verified Tensor-Program Optimization Via High-Level Scheduling Rewrites | Amanda Liu, Gilbert Louis Bernstein, Adam Chlipala, Jonathan Ragan-Kelley | 24m |
A Coq-verified framework implements a pure functional tensor IR called ATL and a suite of semantics-preserving, source-to-source rewrites plus reshape… | ||
| Bottom-Up Synthesis of Recursive Functional Programs using Angelic Execution | Anders Miltner, Adrian Trejo Nuñez, Ana Brendel, Swarat Chaudhuri, Isil Dillig | 25m |
The paper presents a bottom-up synthesis method that actually builds recursive functional programs by executing incomplete programs under angelic semantics… | ||
| Observational Equality: Now for Good | Loïc Pujet, Nicolas Tabareau | 26m |
TTobs extends MLTT with a proof-irrelevant universe and an observational equality that satisfies function and propositional extensionality plus UIP while… | ||
| A Cost-Aware Logical Framework | Yue Niu, Jonathan Sterling, Harrison Grodin, Robert Harper | 23m |
Presents calf, a full-spectrum dependent type theory that treats cost as an effect and enforces an internal noninterference property so I/O behavior cannot… | ||
| Verified Compilation of C Programs with a Nominal Memory Model | Yuting Wang, Ling Zhang, Zhong Shao, Jérémie Koenig | 23m |
The paper claims a drop-in generalization of CompCert’s block memory model into a nominal memory model that uses atoms/supports to rename and separate blocks… | ||
| VIP: Verifying Real-World C Idioms with Integer-Pointer Casts | Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, Peter Sewell | 21m |
Presents VIP, a memory-object model that proves compatible with PNVI while making integer→pointer casts verifiable by adding an explicit provenance-copying… | ||
| Certifying Derivation of State Machines from Coroutines | Mirai Ikebuchi, Andres Erbsen, Adam Chlipala | 18m |
A compiler implemented as a Coq tactic turns programs written with freer-monad coroutines into explicit state-machine code by searching for equivalence proofs… | ||
| Gradualizing the Calculus of Inductive Constructions | Meven Lennon-Bertrand | 24m |
Proposes a no‑go theorem: you cannot keep graduality, normalization and conservativity (closure of universes under dependent product) all at once—the Fire… | ||
| Armed cats: formal concurrency modelling at Arm | Andrew C. Myers | 26m |
Arm formalizes its CPU memory model in the cat language and runs litmus suites with herd+diy; the work yields two provably equivalent reformulations of the… | ||
| Effectful Program Distancing | Ugo Dal Lago, Francesco Gavazzo | 26m |
Proposes a semantic framework that extends differential logical relations to effectful higher-order languages and proves a fundamental lemma that yields… | ||
| A Relational Theory of Effects and Coeffects | Ugo Dal Lago, Francesco Gavazzo | 25m |
Paper gives an operational, relational framework for higher-order languages with graded modal types and algebraic effects, using a monadic semantics (Maybe… | ||
| Symmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible | Vikraman Choudhury, Jacek Karwowski, Amr Sabry | 22m |
Presents a concrete equivalence: the Pi reversible language is shown equivalent to the free symmetric rig groupoid of finite sets and bijections via a… | ||
| Layered and Object-Based Game Semantics | Arthur Oliveira Vale, Paul-André Melliès, Zhong Shao, Jérémie Koenig, Leo Stefanesco | 23m |
Presents a concrete game-semantics model where a layer interface is an object type plus an object strategy, implementations are regular maps from underlay to… | ||
| Fully Abstract Models for Effectful λ-Calculi via Category-Theoretic Logica | Ohad Kammar, Shin-ya Katsumata, Philip Saville | 20m |
Construction takes a model of Moggi’s computational λ-calculus with sums, effect operations and primitives and produces an adequate, fully abstract refinement… | ||
| From Enhanced Coinduction towards Enhanced Induction | Davide Sangiorgi | 24m |
Claims a reusable theory that lifts bisimulation-style semiprogressions to inductive behavioral preorders by introducing inductive observables with numeric… | ||
| Dependently-Typed Data Plane Programming | Matthias Eichholz, Eric Hayden Campbell, Matthias Krebs, Nate Foster, Mira Mezini | 22m |
A dependently-typed P4 called pi4 dependently-typed P4 defines heap types and refinement transformers (a “chomp” Brzozowski derivative) to track bit-level… | ||
| Safe, Modular Packet Pipeline Programming | Devon Loehr, David Walker | 28m |
Introduces Lucid 2.0, a language and type system that guarantees programs are pipeline-safe on pipelined switches (P4/Intel Tofino targets), adding… | ||
| Fair Termination of Binary Sessions | Luca Ciccone, Luca Padovani | 21m |
Claims the first type system ensuring fair termination of binary sessions and a liveness-preserving fair subtyping relation that rejects unsafe substitutions… | ||
| Pirouette: Higher-Order Typed Functional Choreographies | Andrew K. Hirsch, Deepak Garg | 20m |
Pirouette is a choreographic language that compiles a single higher-order functional program into one program per node via endpoint projection, with two… | ||
| Type-Level Programming with Match Types | Olivier Blanvillain, Jonathan Immanuel Brachthuser, Maxime Kjaer, Martin Odersky | 23m |
Formalizes a type‑level pattern matching mechanism in a System F sub calculus and proves soundness with a Coq mechanization of about 6,000 lines, implements… | ||
| Moebius: Metaprogramming using Contextual Types | Junyoung Jang, Samuel Gélineau, Stefan Monnier, Brigitte Pientka | 22m |
Moebius provides a formal metaprogramming core: a multi-level contextual modal lambda-calculus that generates System F–style polymorphic code, lets open code… | ||
| Staging with Class: A Specification for Typed Template Haskell | Ningning Xie, Matthew Pickering, Andres Löh, Nicolas Wu, Jeremy Yallop, Meng Wang | 25m |
Shows that Template Haskell’s interaction with overloading is unsound: splicing well-typed code can produce missing-dictionary errors. Proposes staged type… | ||
| Linked Visualisations via Galois Dependencies | Roly Perera, Minh Nguyen, Tomas Petricek, Meng Wang | 21m |
Presents a concrete, language-based dynamic analysis that links parts of visual outputs back to the input by computing Galois-style forward/backward slices… | ||
| Relational E-matching | Yihong Zhang, Yisu Remy Wang, Max Willsey, Zachary Tatlock | 26m |
Transforms e-graphs into relational tables and patterns into conjunctive queries, then runs worst-case optimal joins (generic join) to guarantee asymptotic… | ||
| Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFI | Matthew Kolosick, Shravan Ravi Narayan, Evan Johnson, Conrad Watt, Michael LeMay, Deepak Garg, Ranjit Jhala, Deian Stefan | 22m |
Paper claims that adding static invariants lets sandboxed code use simple function calls instead of heavyweight wrappers, and implements this end-to-end. A… | ||
| SolType: Refinement Types for Arithmetic Overflow in Solidity | Bryan Tan, Benjamin Mariano, Shuvendu K. Lahiri, Isil Dillig, Yu Feng | 26m |
SolType is a refinement-type system for Solidity with an implementation called Solid that translates contracts to a miniSol SSA IR, encodes overflow checks as… | ||
| Oblivious Algebraic Data Types | Qianchuan Ye, Benjamin Delaware | 23m |
Presents Lambda OADT, a dependently typed calculus that encodes recursive private data by tagging each type with a public view (e.g. max tree depth) and… | ||
| On Type-Cases, Union Elimination, and Occurrence Typing | Giuseppe Castagna, Mickaël Laurent, Kim Nguyen, Matthew Lutze | 24m |
Extends union/intersection type systems with a concrete type-case construct and proves the union-elimination plus type-case rules capture occurrence typing… | ||
| Logarithm and Program Testing | Kuen-Bang Hou (Favonia), Zhuyang Wang | 23m |
Proposes a mechanical monomorphization that, for prenex System F with products, sums, functions and strictly positive inductive types, computes a special type… | ||
| A Formal Foundation for Symbolic Evaluation with Merging | Sorawee Porncharoenwase, Luke Nelson, Xi Wang, Emina Torlak | 22m |
New formal symbolic semantics incorporates state merging and a parameterized symbolic factory and is mechanized in Lean, proving soundness, completeness… | ||
| Semantics for Variational Quantum Programming | Xiaodong Jia, Andre Kornell, Bert Lindenhovius, Michael Mislove, Vladimir Zamdzhiev | 24m |
A type-safe language combines a higher-order probabilistic classical core (PFPC) with a first-order linear quantum core and a new first-order quantum-function… | ||
| A Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantu | Xuan-Bach Le, Shang Wei Lin, Jun Sun, David Sanan | 20m |
Proposes a Hoare-style logic that gives a quantum separating conjunction and a quantum frame rule so local reasoning carries over when multi-qubit states… | ||
| Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs | Charles Yuan, Christopher McNally, Michael Carbin | 20m |
Twist presents a concrete language and the semantic property purity that guarantees an expression is unentangled from the rest of the program, implemented via… | ||
| Quantum Information Effects | Chris Heunen, Robin Kaarsgaard | 23m |
A type-and-effect system (languages: yuppie, yuppie-a, yuppie-chi-a) models two quantum information effects — allocation and hiding — and proves the system is… | ||
| PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull | Mark Niklas Møller, Gleb Makarchuk, Gagandeep Singh, Markus Pöschel, Martin Vechev | 23m |
PRIMA presents a verifier that computes scalable convex-hull abstractions for groups of neurons using a novel dual-space partial double description method and… | ||
| Interval Universal Approximation for Neural Networks | Zi Wang, Aws Albarghouthi, Gautam Prakriya, Somesh Jha | 19m |
Proves an interval universal approximation theorem: for any continuous target and any practical squashable functions (monotone with one-sided limits) there… | ||
| Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic | Faustyna Krawiec, Simon Peyton Jones, Neel Krishnaswami, Tom Ellis, Richard A. Eisenberg, Andrew Fitzgibbon | 27m |
Claims a source to source transformation that produces dual numbers then generalizes to multi dual numbers and a compact symbolic delta representation… | ||
| A Dual Number Abstraction for Static Analysis of Clarke Jacobians | Jacob Laurel, Rem Yang, Gagandeep Singh, Sasa Misailovic | 27m |
Paper presents a dual-interval abstract domain that lifts dual-number forward-mode differentiation to interval arithmetic and proves the transformer semantics… | ||
| Better Learning through Programming Languages | Armando Solar-Lezama, Michael Hicks | 01h 00m |
Argues that combining program synthesis with ML lets search scale and tolerate noise by directing search with a network rather than exhaustive enumeration… | ||
| What's Decidable about Linear Loops? | Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, David Purser, Anton Varonka, Markus A. Whiteland, James Worrell | 26m |
The paper proves decidability of MSO model checking for discrete-time linear dynamical systems with semialgebraic predicates provided every predicate is either… | ||
| Context-Bounded Verification of Thread Pools | Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche | 22m |
The work proves safety for thread-pooled Boolean programs with per-task context bound k and pool size n (both given in binary) is EXPSPACE-complete, while… | ||
| Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation L | Jules Jacobs, Stephanie Balzer, Robbert Krebbers | 23m |
Introduces connectivity graphs as a generic, parametric graph abstraction plus local Separation Logic predicates that let one prove preservation and global… | ||
| Visibility Reasoning for Concurrent Snapshot Algorithms | Joakim Ånöhman, Aleksandar Nanevski | 20m |
Applies visibility relations to prove linearizability for three Jayanti algorithms, giving a reusable, layered proof instead of locating linearization points… | ||
| Subcubic Certificates for CFL Reachability | Dmitry Chistikov, Rupak Majumdar, Philipp Schepper | 29m |
Claims existence of O(n^2) certificates for both yes and no instances of Dyck-2/CFL reachability, where positive certificates use grammar-based compression of… | ||
| Efficient Algorithms for Dynamic Bidirected Dyck-Reachability | Yuanbo Li, Kris Satya, Qirun Zhang | 24m |
Presents a dynamic algorithm that maintains all-pairs bidirected Dyck-reachability with O(n α(n)) update time per edge and O(1) queries, using a merged-graph… | ||
| Return of CFA: Call-Site Sensitivity Can Be Superior to Object Sensitivity Even | Minseok Jeon, Hakjoo Oh | 24m |
Paper claims call-site sensitivity with context tunneling can be strictly more precise and more scalable than object sensitivity, and demonstrates a toolchain… | ||
| Partial (In)Completeness in Abstract Interpretation: Limiting the Imprecision in | Marco Campion, Mila Dalla Preda, Roberto Giacobazzi | 23m |
Defines a quasi-metric a-compatible on abstract domains (examples: weighted path length for sign and interval domains) and formalizes epsilon-partial… | ||
| Truly Stateless, Optimal Dynamic Partial Order Reduction | Michalis Kokologiannakis, Iason Marmanis, Vladimir Gladstein, Viktor Vafeiadis | 20m |
Claim: TruSt explores exactly one interleaving per Mazurkiewicz-equivalence class while using linear (paper shows how to get from N^2 to linear) memory instead… | ||
| Extending Intel-x86 Consistency and Persistency: Formalising the Semantics of In | Azalea Raad, Luc Maranget, Viktor Vafeiadis | 22m |
Extends x86 semantics to cover non-temporal stores and page memory types, delivering EX86/PEx86 models in both operational and declarative forms and proving… | ||
| The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Conc | Alan Jeffrey, James Riely, Mark Batty, Simon Cooksey, Ilya Kaysin, Anton Podkopaev | 20m |
Defines a compositional event semantics that attaches preconditions and families of predicate transformers to events, so sequential composition picks a… | ||
| On Incorrectness Logic and Kleene Algebra with Top and Tests | Cheng Zhang, Arthur Azevedo de Amorim, Marco Gaboardi | 17m |
Kleene Algebra with Tests (KAT) cannot express incorrectness triples because it lacks an explicit codomain operation; adding a single top element yields… | ||
| Concurrent Incorrectness Separation Logic | Azalea Raad, Josh Berdine, Derek Dreyer, Peter W. O'Hearn | 27m |
Develops CISL as a parametric extension of Incorrectness Separation Logic that models concurrency with histories and lock-aware events, instantiates to race… | ||
| Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz | Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, Derek Dreyer | 24m |
Framework claims a mechanically checked simulation that preserves contextual refinement and termination under a fair scheduler for real concurrent compiler… | ||
| A Separation Logic for Heap Space under Garbage Collection | Jean-Marie Madiot, François Pottier | 19m |
A separation logic (called SLgc in the paper) models heap space under tracing GC by treating allocation budget as space credits consumed on allocation and… | ||
| Solving String Constraints with Regex-Dependent Functions through Transducers wi | Taolue Chen, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony W. Lin, Philipp Römmer, Zhilin Wu | 24m |
Introduces a new automata model, prioritized streaming string transducers, that encodes JavaScript-style regex features (greedy/lazy star, capturing groups… | ||
| Solving Constrained Horn Clauses Modulo Algebraic Data Types and Recursive Funct | Hari Govind V K, Sharon Shoham, Arie Gurfinkel | 25m |
Presents an IC3/PDR-inspired solver called Racer that combines relationification, controlled unfolding of recursive definitions, and uninterpreted-function… | ||
| Induction Duality: Primal-Dual Search for Invariants | Oded Padon, James R. Wilcox, Jason R. Koenig, Kenneth L. McMillan, Alex Aiken | 21m |
Presents a formal induction duality linking execution traces and bounded incremental proofs, and derives primal-dual Houdini, a symmetric algorithm that… | ||
| Software Model-Checking as Cyclic-Proof Search | Takeshi Tsukada, Hiroshi Unno | 27m |
Claims that many software model-checking algorithms are exactly proof-search strategies for a cyclic proof system, so a single logical framework reconstructs… | ||
| Principles of Programming Language Translators | ALFRED V. AHO | 59m |
Thesis: abstractions and algorithms turn compiler design from craft to engineering by giving precise models, tools and fast implementations. Examples… | ||
| nothing matches | ||