An Intrinsically Typed Compiler for Algebraic Effect Handlers
summary
Implements a type preserving compiler from an algebraic effect handler calculus to a stack‑machine assembly and proves type preservation by writing the compiler as intrinsically typed ASTs in Agda implementation. Solves safe capture and resumption of first‑class continuations by adopting stack polymorphism so captured continuations quantify over unknown stacks. The compiler typechecks in Agda so the preservation statement is mechanized; next steps are semantic preservation proofs and continuation‑usage optimizations.
AI-written summary · about
chapters (4)
related talks
22mType-Safe Code Generation With Algebraic Effects and Handlers
15mEfficient Compilation of Algebraic Effect Handlers
19mTowards a Reflection for Effect Handlers
25mIntrinsically Typed Compilation with Nameless Labels
18mLexical Effect Handlers, Directly
14mType-Sensitive Algebraic Macros
15mHandling Bidirectional Control Flow
12mCompiling Effect Handlers in Capability-Passing Style