Lift Inference for Lexical Effect Handlers with Second-Class Functions
summary
Claims a concrete compiler pass that infers lifting information for a core language with second‑class functions and emits explicit region evidence so lexical handlers compile without runtime handler search. It implements a translation from System_Xi to Lambda_cap that performs region inference to produce subregion evidence, reuses an existing iterated CPS backend, and proves the pass semantics‑ and type‑preserving; an implementation exists and plugs into the Effekt compiler pipeline.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:49Motivation for efficient compilation
- 2:55System XI recap
- 5:24CPS semantics with lifting
- 6:26Big Lambda Cap intro
- 8:54Region evidence and lifting
- 10:39Evaluation example
- 12:03Region inference core
- 13:30Translation System XI to BLC
- 17:44Higher-order functions handling
- 20:14Summary
related talks
19mFrom Capabilities to Regions: Enabling Efficient Compilation of Lexical Effect ...
18mLexical Effect Handlers, Directly
15mZero-Overhead Lexical Effect Handlers
22mLexical Effect Handler: Fast by Design, Correct by Proof
15mEffect Handlers, Evidently
12mCompiling Effect Handlers in Capability-Passing Style
23mBetter Defunctionalization through Lambda Set Specialization
16mContextual Effect Polymorphism Meets Bidirectional Effects (Extended Abstract)