POPL 2025
79 papers
- A Demonic Outcome Logic for Randomized Nondeterminism
- A Dependent Type Theory for Meta-programming with Intensional Analysis
- A Modal Deconstruction of Löb Induction
- A Primal-Dual Perspective on Program Verification Algorithms
- A Quantitative Probabilistic Relational Hoare Logic
- A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests
- A Verified Foreign Function Interface between Coq and C
- Abstract Operational Methods for Call-by-Push-Value
- Affect: An Affine Type and Effect System
- Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order Programs
- Algebras for Deterministic Computation Are Inherently Incomplete
- All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants
- An Incremental Algorithm for Algebraic Program Analysis
- Approximate Relational Reasoning for Higher-Order Probabilistic Programs
- Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting
- Automated Program Refinement: Guide and Verify Code Large Language Model with Refinement Calculus
- Automating Equational Proofs in Dirac Notation
- Avoiding Signature Avoidance in ML Modules with Zippers
- Axe 'Em: Eliminating Spurious States with Induction Axioms
- Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings
- BiSikkel: A Multimode Logical Framework in Agda
- Bidirectional Higher-Rank Polymorphism with Intersection and Union Types
- Biparsers: Exact Printing for Data Synchronisation
- Bluebell: An Alliance of Relational Lifting and Independence for Probabilistic Reasoning
- CF-GKAT: Efficient Validation of Control-Flow Transformations
- Calculational Design of Hyperlogics by Abstract Interpretation
- Coinductive Proofs for Temporal Hyperliveness
- Compositional Imprecise Probability: A Solution from Graded Monads and Markov Categories
- Consistency of a Dependent Calculus of Indistinguishability
- Data Race Freedom à la Mode
- Denotational Semantics of Gradual Typing using Synthetic Guarded Domain Theory
- Derivative-Guided Symbolic Execution
- Dis/Equality Graphs
- Do You Even Lift? Strengthening Compiler Security Guarantees against Spectre Attacks
- Finite-Choice Logic Programming
- Flexible Type-Based Resource Estimation in Quantum Circuit Description Languages
- Flo: A Semantic Foundation for Progressive Stream Processing
- Formal Foundations for Translational Separation Logic Verifiers
- Formalising Graph Algorithms with Coinduction
- Fulminate: Testing CN Separation-Logic Specifications in C
- Generic Refinement Types
- Generically Automating Separation Logic by Functors, Homomorphisms, and Modules
- Grove: A Bidirectionally Typed Collaborative Structure Editor Calculus
- Guaranteed Bounds on Posterior Distributions of Discrete Probabilistic Programs with Loops
- Inference Plans for Hybrid Particle Filtering
- Interaction Equivalence
- Linear and Non-linear Relational Analyses for Quantum Program Optimization
- Maximal Simplification of Polyhedral Reductions
- MimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age
- Model Checking C/C++ with Mixed-Size Accesses
- Modelling Recursion and Probabilistic Choice in Guarded Type Theory
- On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus
- On Extending Incorrectness Logic with Backwards Reasoning
- Pantograph: A Fluid and Typed Structure Editor
- Preservation of Speculative Constant-Time by Compilation
- Program Analysis via Multiple Context Free Language Reachability
- Program Logics à la Carte
- Progressful Interpreters for Efficient WebAssembly Mechanisation
- QuickSub: Efficient Iso-Recursive Subtyping
- Qurts: Automatic Quantum Uncomputation by Affine Types with Lifetime
- RE#: High Performance Derivative-Based Regex Matching with Intersection, Complement, and Restricted Lookarounds
- RELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency
- Reachability Analysis of the Domain Name System
- Relaxed Memory Concurrency Re-executed
- SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations
- Semantic Logical Relations for Timed Message-Passing Protocols
- Simple Linear Loops: Algebraic Invariants and Applications
- Sound and Complete Proof Rules for Probabilistic Termination
- Symbolic Automata: Omega-Regularity Modulo Theories
- Tail Modulo Cons, OCaml, and Relational Separation Logic
- TensorRight: Automated Verification of Tensor Graph Rewrites
- The Best of Abstract Interpretations
- The Decision Problem for Regular First Order Theories
- The Duality of λ-Abstraction
- Top-Down or Bottom-Up? Complexity Analyses of Synchronous Multiparty Session Types
- Translation of Temporal Logic for Efficient Infinite-State Reactive Synthesis
- Unifying Compositional Verification and Certified Compilation with a Three-Dimensional Refinement Algebra
- VeriRT: An End-to-End Verification Framework for Real-Time Distributed Systems
- Verifying Quantum Circuits with Level-Synchronized Tree Automata