Dependent Session Protocols in Separation Logic from First Principles
summary
Three-layer design builds session protocols from mutable references: one-shot channels, then functional session channels, then imperative endpoints; specs use Iris invariants and high-order ghost variants rather than recursive domain equations or higher-order ghost state. Implementation verifies dependent binders, subprotocols, guarded recursion and channel closing, is mechanized in Iris/Coq and composes cleanly; proofs and code fit in less than 1000 lines of Coq, proving crash freedom and functional correctness for message-passing primitives.
AI-written summary · about
chapters (17)
- 0:00Introduction
- 1:03Message passing concurrency
- 3:09Dependent protocols vs session types
- 4:13Goal: Simplify ACTRESS
- 7:21Design from first principles
- 8:22Three-layer approach
- 8:45Oneshot channels
- 11:38Proving oneshot specs
- 14:05Functional session channels
- 16:08Dependent protocols spec
- 19:21Canonicity and invariants
- 20:25Imperative session channels
- 21:30Proving example
- 22:14Additional features
- 23:16Comparison with ACTRESS
- 24:19Conclusion
- 25:02Q&A
related talks
16mVerified Lock-Free Session Channels with Linking
20mDeadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-O...
50mSession Types Meet Polymorphism and Dependent Types
20mTrillium: Higher-Order Concurrent and Distributed Separation Logic for Intension...
54mShared Session Types for Safe, Practical Concurrency
21mContextual Refinement of Higher-Order Concurrent Probabilistic Programs
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
24mSimuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz