Back to Direct Style: Typed and Tight
summary
Two typed languages are presented: a direct-style language and a CPS language, each with an abstract-machine semantics, plus translations both ways that are total, type-preserving and give an operational correspondence with bottom-up translation that tracks which continuation each subterm returns to. The back-translation inserts limited control operators only when needed, using suspend to capture a stack and run to mount it. Compositions are one-sided syntactic inverses on the full language and full inverses on the pure fragment.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 0:21Direct vs continuation style
- 2:27Compilation vision
- 3:49Key contributions
- 4:11CPS to direct style
- 5:15Complex control flow
- 6:42Inserting control operators
- 7:46Async operator translation
- 9:36Translation properties
- 11:02Q&A
related talks
12mTowards Dependently-Typed Control Effects (Extended Abstract)
13mOne-Pass CPS Translation of Dependent Types (Talk Proposal)
19mIll-Typed Programs Don't Evaluate
56mOn Type-Based Techniques for Program Manipulation
19mType System for Four Delimited Control Operators
02h 50mIntro to Type Systems and Operational Semantics
22mA Dependent Language with Type-Safe Program Extraction
20mA Dependent Type Theory for Meta-programming with Intensional Analysis