PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs
summary
PulseCore is a new, mechanized concurrent separation logic implemented inside F★ that claims to support impredicative invariants and higher‑order ghost state for dependently typed, higher‑order programs. It uses a ghost heap, a higher‑order heap with level stratification via interaction theory to solve the domain equation, step‑indexing with later credits, and a Pulse surface language. The authors extract proofs to C/Rust/OCaml and validate the design with 31,000 lines verified code: task pools, a barrier needing higher‑order ghost state, and a verified DICE secure‑boot implementation.
AI-written summary · about
chapters (9)
- 0:00PulseCore at PLLDI 2026
- 1:23Limitations of verification
- 3:54PulseCore design with F*
- 7:26Invariants in PulseCore
- 9:58Impredicative invariants
- 12:47PulseCore foundations
- 16:21Encoding actions and credits
- 17:43Case studies and future work
- 18:11Q&A
related talks
21mKuiper: Correct and Efficient GPU Programming with Dependent Types and Separation Logic
19mBeyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic
22mImplementing separation logic using an SMT-backed Frame Rule
19mDeriving Dependently-Typed OOP from First Principles
20mA Graded Modal Type Theory for Pulse Schedules
01h 28mInto the Core Squeezing Haskell into nine Constructors
01h 38mGHC Core Optimisations
25mA Relational Separation Logic for Effect Handlers