A Separation Logic for Effect Handlers
summary
Introduces a Separation Logic that embeds protocols into Iris-style weakest preconditions to specify and verify programs using user-defined effect handlers (deep and shallow), proving the key claim that clients and handlers can be verified modularly. Mechanization (machine-checked) covers case studies: a memory cell with two distinct implementations that both satisfy the same spec, control inversion, and a cooperative-concurrency library. Main limitations: only one-shot continuations, no primitive concurrency, and nearest-handler-only semantics; central proof object is the handler judgment.
AI-written summary · about
chapters (16)
- 0:00Intro
- 0:13EXCEPTION HANDLING
- 0:52EFFECT HANDLERS
- 2:04APPLICATION - MUTABLE STATE
- 6:32A FEW QUESTIONS
- 7:17IN THIS PAPER
- 7:47IN THIS TALK
- 9:18PROTOCOLS - THE KEY IDEA
- 10:59THE SYNTAX OF PROTOCOLS
- 12:27EXAMPLE - ABORT PROTOCOL
- 13:35EXAMPLE - STATE PROTOCOL
- 14:41WEAKEST PRECONDITION - TYING PROGRAMS TO PROTOCOLS
- 15:44REASONING RULES
- 20:32HANDLER JUDGEMENT
- 22:07CASE STUDY - MUTABLE STATE
- 23:37CONCLUSION