A Typed and Unified Reflection for Shift and Shift0
summary
Establishes a typed, unified reflection for both shift and shift0 by deriving a two-CPS interpreter and a colon translation that yields a CPS target without administrative redexes, proving an order isomorphism between a ANF-like car calculus and CPS, and a reflection between DS and car. Key lemmas are a substitution-for-continuations split by K’s location and a continuation-existence lemma; all proofs are formalized in Agda formalization assuming functional extensionality and a PHOAS rule.
AI-written summary · about
chapters (11)
- 0:00Typed reflection for shift operators
- 3:32Reflection and control operators
- 5:19Meta continuation for shift
- 7:51Two-CPS translation with annotations
- 10:03Order isomorphism between calculi
- 12:40Proof structure for reflection
- 15:16Substitution lemma for continuations
- 20:46Continuation existence lemma
- 22:57Formalization in Agda
- 23:41Future work on effect handlers
- 24:23Q&A
related talks
19mTowards a Reflection for Effect Handlers
19mType System for Four Delimited Control Operators
13mOne-Pass CPS Translation of Dependent Types (Talk Proposal)
21mSyntax with Shifted Names
12mOn the metatheory of IRs and the CPS-calculus
29mHigher-Order Weakest Precondition Transformers via a CPS Transformation
15mBack to Direct Style: Typed and Tight
12mTowards Dependently-Typed Control Effects (Extended Abstract)