One-Pass CPS Translation of Dependent Types (Talk Proposal)
summary
Claims a one-pass CPS translation of Calculus of Constructions with Sigma (dependent pair) types that preserves dependent typing while producing no administrative redexes. Adapts prior techniques: making the answer type polymorphic, adding target equivalences like naturality, and introducing a new definition lambda whose typing records the exact value a continuation will receive. Main obstacle is that translating types now refers to source terms, forcing simultaneous term-and-type translation and complicating the type-preservation proof; preliminary results target Sigma types.
AI-written summary · about
chapters (10)
- 0:00One-pass CPS translation intro
- 1:27Naive CPS translation challenges
- 2:36Type mismatch in product CPS
- 4:05Bman’s type preservation
- 5:54One-pass CPS translation details
- 7:40Lambda’s role in translation
- 8:51Parallel translation complications
- 9:38Q&A on Lambda
- 10:23Q&A on sigma types
- 11:26Q&A on B transformation
related talks
12mTowards Dependently-Typed Control Effects (Extended Abstract)
29mHigher-Order Weakest Precondition Transformers via a CPS Transformation
19mTowards a Reflection for Effect Handlers
15mBack to Direct Style: Typed and Tight
19mDeriving Dependently-Typed OOP from First Principles
29mA Typed and Unified Reflection for Shift and Shift0
18mSpace-Efficient Polymorphic Gradual Typing, Mostly Parametric
56mOn Type-Based Techniques for Program Manipulation