Lift Inference for Lexical Effect Handlers with Second-Class Functions
summary
Presents an algorithm that infers lifting information for lexical effect handlers by translating System Xi (with second-class functions) into Lambda_cap with explicit regions and separation evidence, so capabilities carry evidence matching the distance to their handler. Uses region inference to generate and thread fresh regions and evidence, then reuses an existing iterated CPS translation to remove handler overhead. Claims semantics and safety preservation and reports a working implementation.
AI-written summary · about
chapters (7)
- 0:00Start
- 0:16Quick Motivation
- 0:27Motivation
- 3:31Semantics
- 5:15Cps Semantics
- 12:15Core Ideas
- 17:34Higher Order Functions
related talks
19mFrom Capabilities to Regions: Enabling Efficient Compilation of Lexical Effect ...
18mLexical Effect Handlers, Directly
15mZero-Overhead Lexical Effect Handlers
15mEffect Handlers, Evidently
22mLexical Effect Handler: Fast by Design, Correct by Proof
29mLogical Relations for Effect Capabilities
12mCompiling Effect Handlers in Capability-Passing Style
16mContextual Effect Polymorphism Meets Bidirectional Effects (Extended Abstract)