Lexical Effect Handler: Fast by Design, Correct by Proof
summary
Claims a compiler and language named Lexa that outperforms existing effect handler implementations while preserving lexical scoping and formal correctness. Implements low level stack switching via a stacktrack library to make raise and resume O(1), adds a software MMU called SMMU and virtual resumption to support multi‑shot continuations, and introduces a metadata driven “zero overhead” mode to avoid per‑call costs. Benchmarks show state‑of‑the‑art speed and all compilation techniques are mechanically proved correct.
AI-written summary · about
chapters (14)
- 0:00Introduction
- 1:45Modularity problem with handlers
- 4:13Lexical handlers solve collisions
- 5:17Three compilation techniques
- 6:00Direct Lexa: stack addresses
- 8:49Direct Lexa performance
- 9:11Multi-shot limits in Direct Lexa
- 10:55MultiLexa: virtual resumption
- 14:30ZeroLexa: eliminating handler argument overhead
- 15:34ZeroLexa overhead
- 18:02ZeroLexa with higher-order
- 20:12ZeroLexa stack walking
- 21:17Trade-offs between DirectLexa, MultiLexa, and ZeroLexa
- 21:39Conclusion
related talks
18mLexical Effect Handlers, Directly
15mZero-Overhead Lexical Effect Handlers
15mEffect Handlers, Evidently
21mVirtualizing Continuations
21mLift Inference for Lexical Effect Handlers with Second-Class Functions
12mCompiling Effect Handlers in Capability-Passing Style
21mLift Inference for Lexical Effect Handlers with Second-Class Functions
28mFirst-class Names for Effect Handlers