A Relational Separation Logic for Effect Handlers
summary
Presents blaze, the first mechanised relational separation logic for effect handlers, implemented on Rocq/Iris and proved inside Coq; key idea is a refinement relation parameterised by a user-supplied theory that lets effects on one side refine non‑effecting code on the other. Adds context‑closure and traversible theories for modular bind/frame reasoning and two new concurrency rules, logical-fork and thread-swap. Case studies relate several asynchronous effect‑library implementations to truly concurrent versions and reproduce handler correctness criteria; artifacts and proofs are available.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:05Relational separation logic goal
- 3:13Fork effect example
- 5:03Challenges in handlers
- 7:11Parameterized refinement idea
- 9:34Solving with refinement
- 11:21Compositional exhaustion rule
- 13:05Context local reasoning
- 15:36Verifying fork effect
- 16:59Novel concurrency rules
- 20:12Conclusion
- 21:40Q&A
related talks
29mLogical Relations for Effect Capabilities
21mOutcome Separation Logic: Local Reasoning for Correctness and Incorrectness with(…)
15mHandling Bidirectional Control Flow
21mEffectful Software Contracts
11mLocal algebraic effect theories
15mEffect Handlers, Evidently
19mCausality and Semantic Separation
14mAdequacy for Algebraic Effects Revisited