POPL 2026
92 papers
- A Complementary Approach to Incorrectness Typing
- A Family of Sims with Diverging Interests
- A Lazy, Concurrent Convertibility Checker
- A Logic for the Imprecision of Abstract Interpretations
- A Modular Static Cost Analysis for GPU Warp-Level Parallelism
- A Relational Separation Logic for Effect Handlers
- A Synthetic Reconstruction of Multiparty Session Types
- A Verified High-Performance Composable Object Library for Remote Direct Memory Access
- Abstraction Functions as Types: Modular Verification of Cost and Behavior in Dependent Type Theory
- Accelerating Syntax-Guided Program Synthesis by Optimizing Domain-Specific Languages
- AdapTT: Functoriality for Dependent Type Casts
- Algorithmic Conversion with Surjective Pairing: A Syntactic and Untyped Approach
- All for One and One for All: Program Logics for Exploiting Internal Determinism in Parallel Programs
- An Equational Axiomatization of Dynamic Threads via Algebraic Effects: Presheaves on Finite Relations, Labelled Posets, and Parameterized Algebraic Theories
- An Expressive Assertion Language for Quantum Programs
- Arbitration-Free Consistency Is Available (and Vice Versa)
- ArchSem: Reusable Rigorous Semantics of Relaxed Architectures
- Bayesian Separation Logic: A Logical Foundation and Axiomatic Semantics for Probabilistic Programming
- Big-Stop Semantics: Small-Step Semantics in a Big-Step Judgment
- Bounded Sort Polymorphism with Elimination Constraints
- Bounded Treewidth, Multiple Context-Free Grammars, and Downward Closures
- Canonicity for Indexed Inductive-Recursive Types
- Characterizing Sets of Theories That Can Be Disjointly Combined
- ChiSA: Static Analysis for Lightweight Chisel Verification
- ChopChop: A Programmable Framework for Semantically Constraining the Output of Language Models
- Classical Notions of Computation and the Hasegawa-Thielecke Theorem
- Coco: Corecursion with Compositional Heterogeneous Productivity
- Compiling to Linear Neurons
- Consistent Updates for Scalable Microservices
- Context-Free-Language Reachability for Almost-Commuting Transition Systems
- Corrigendum: Unrealizability Logic
- Counting and Sampling Traces in Regular Languages
- Cryptis: Cryptographic Reasoning in Separation Logic
- DafnyMPI: A Dafny Library for Verifying Message-Passing Concurrent Programs
- Dependent Coeffects for Local Sensitivity Analysis
- Determination Problems for Orbit Closures and Matrix Groups
- Di- is for Directed: First-Order Directed Type Theory via Dinaturality
- Domain-Theoretic Semantics for Functional Logic Programming
- Encode the Cake and Eat It Too: Controlling Computation in Type Theory, Locally
- Endangered by the Language But Saved by the Compiler: Robust Safety via Semantic Back-Translation
- Extensible Data Types with Ad-Hoc Polymorphism
- Formal Verification for JavaScript Regular Expressions: A Proven Mechanized Semantics and Its Applications
- Foundational Multi-Modal Program Verifiers
- From Semantics to Syntax: A Type Theory for Comprehension Categories
- Fuzzing Guided by Bayesian Program Analysis
- General Decidability Results for Systems with Continuous Counters
- Generating Compilers for Qubit Mapping and Routing
- Hadamard-Pi: Equational Quantum Programming
- Handling Higher-Order Effectful Operations with Judgemental Monadic Laws
- Handling Scope Checks: A Comparative Framework for Dynamic Scope Extrusion Checks
- Higher-Order Behavioural Conformances via Fibrations
- Hyperfunctions: Communicating Continuations
- Inductive Program Synthesis by Meta-Analysis-Guided Hole Filling
- JAX Autodiff from a Linear Logic Perspective
- Lazy Linearity for a Core Functional Language
- Let Generalization, Polymorphic Recursion, and Variable Minimization in Boolean-Kinded Type Systems
- Local Contextual Type Inference
- Miri: Practical Undefined Behavior Detection for Rust
- Network Change Validation with Relational NetKAT
- Nice to Meet You: Synthesizing Practical MLIR Abstract Transformers
- Normalisation for First-Class Universe Levels
- On Circuit Description Languages, Indexed Monads, and Resource Analysis
- Optimising Density Computations in Probabilistic Programs via Automatic Loop Vectorisation
- Oriented Metrics for Bottom-Up Enumerative Synthesis
- Parameterized Infinite-State Reactive Synthesis
- Parameterized Verification of Quantum Circuits
- Parametrised Verification of Intel-x86 Programs
- Piecewise Analysis of Probabilistic Programs via 𝑘-Induction
- Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants
- Probabilistic Programming with Vectorized Programmable Inference
- Quantum Circuits Are Just a Phase
- Qudit Quantum Programming with Projective Cliffords
- Quotient Polymorphism
- RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing
- Recurrence Sets for Proving Fair Non-termination under Axiomatic Memory Consistency Models
- Rows and Capabilities as Modal Effects
- Security Reasoning via Substructural Dependency Tracking
- Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions
- Stateful Differential Operators for Incremental Computing
- The Complexity of Testing Message-Passing Concurrency
- The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs
- The Relative Monadic Metalanguage
- The Simple Essence of Boolean-Algebraic Subtyping: Semantic Soundness for Algebraic Union, Intersection, Negation, and Equi-recursive Types
- Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by Equality Saturation
- Tropical Mathematics and the Lambda-Calculus II: Tropical Geometry of Probabilistic Programming Languages
- TypeDis: A Type System for Disentanglement
- Typing Strictness
- U-Turn: Enhancing Incorrectness Analysis by Reversing Direction
- Verifying Almost-Sure Termination for Randomized Distributed Algorithms
- Welterweight Go: Boxing, Structural Subtyping, and Generics
- What Is a Monoid?
- Zoo: A Framework for the Verification of Concurrent OCaml 5 Programs using Separation Logic