SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed ...
summary
SteelCore provides a semantics for CSL inside F, deriving Hoare rules from effectful non‑deterministic interleaving; it encodes computations as action trees interpreted to NST (non‑deterministic, stateful, possibly divergent) and exposes two effects, Steel and SteelAtomic. It implements dynamically allocated named invariants, atomic CAS, and verified libraries—SpinLock, ForkJoin, protocol‑indexed channels with a PingPong client—and totals about 11,000 lines of mechanized F development.
AI-written summary · about
chapters (12)
- 0:00Intro
- 0:17Verifying Concurrent Programs
- 1:31Steel: A Concurrent Separation Logic (CSL) for F
- 2:40Encoding Computations through Effectful Indexed Action Trees
- 4:59Proving Soundness of the Semantics
- 5:47Instantiating the Program Logic
- 6:43Invariants in Steel
- 8:19Using Invariants
- 10:10Stacking Abstractions in Steel
- 11:05Steel Example: Channel Types
- 12:07Steel Example: PingPong Protocol
- 13:15Conclusion
related talks
15mRethinking Safe Consistency in Distributed Object-Oriented Programming
36mSpecification-Guided Component-Based Synthesis from Effectful Libraries
34mHow I learned to stop worrying and love Functional Design
40mRetrofitting Concurrency – Lessons from the Engine Room
24mTaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Pr
28mWhat You See Is What It Does: A Structural Pattern for Legible Software
54mReasoning about Progress of Concurrent Objects
59mSoftware Engineering Is About Tradeoffs