A Typed Continuation-Passing Translation for Lexical Effect Handlers
summary
Claims a sound translation of lexical effect handlers to pure System F via a continuation-passing translation that needs no runtime support. Handlers, regions and capabilities become types, abstractions and functions; regions map to answer types. Proved type preservation and a simulation theorem, with a mechanized (weaker) proof mechanized in Coq. Produces ordinary beta-reducible terms (no labels, no stack frames), and the authors are building a compiler and running benchmarks.
AI-written summary · about
chapters (5)
- 0:00Start
- 0:39Overview of How Effect Handlers Work Using an Example
- 0:51An Example of an Effect Signature
- 3:48Using Effect Handlers for Exceptions
- 8:24Effect Safety
related talks
12mCompiling Effect Handlers in Capability-Passing Style
15mZero-Overhead Lexical Effect Handlers
18mLexical Effect Handlers, Directly
15mEffect Handlers, Evidently
19mFrom Capabilities to Regions: Enabling Efficient Compilation of Lexical Effect ...
22mLexical Effect Handler: Fast by Design, Correct by Proof
21mLift Inference for Lexical Effect Handlers with Second-Class Functions
21mLift Inference for Lexical Effect Handlers with Second-Class Functions