A General Fine-Grained Reduction Theory for Effect Handlers
summary
Presents a fine-grained reduction semantics for deep effect handlers that gives confluence and standardisation proofs (adapting Takahashi/McKinna techniques), a standard evaluation strategy that simulates classical non-local semantics and preserves observational equivalence, and the first normalisation-by-evaluation algorithm for handlers with proofs of soundness and completeness. Also proves non-expressibility of the lift operator. Paper supplies evaluated artifacts and a supplementary archive; proofs are detailed and the NBE construction succeeds subject to the usual termination caveats.
AI-written summary · about
chapters (9)
- 0:00Effect handlers introduction
- 1:02What effect handlers are
- 5:17Deep handler reduction rules
- 10:59Good reduction theory
- 13:28Standardization in reductions
- 18:18Hybrid evaluation strategies
- 20:47Fine-grained versus context-capturing
- 21:52Applications and future work
- 22:55Q&A
related talks
25mHandling Higher-Order Effectful Operations with Judgemental Monadic Laws
24mTyped Equivalence of Labeled Effect Handlers and Labeled Delimited Control Operat...
33mRethinking Effects with Effect Systems
46mFunctional effects in perspective
33mExtensible Effects: A Leaner Cake for Purely Functional Code
49mFinite functional programming via graded effects and relevance types
32mExperience Report: Graph Rewriting with Lexical Effect Handlers
26mEffect Handlers for Programmable Inference