Type-Preserving Flat Closure Optimization
summary
Proposes a new Flat-Closure Calculus (FCC) that encodes the flat closure calling convention with singleton types so the projected code pointer is typechecked to accept the closure itself as the environment, proving type safety and subject reduction and giving a type-preserving translation from an existing closure-converted IR. Implements the system in Redex, documents seven concrete closure-optimization requirements that FCC satisfies, and ships reproducible artifacts and evaluations.
AI-written summary · about
chapters (10)
- 0:00Type-safe compiler optimizations
- 1:03Closure conversion problems
- 2:29Safety property of closures
- 2:51Flat closure optimization
- 3:33Existential closure representation
- 4:18Flat Closure Calculus (FCC)
- 5:23Singleton types in FCC
- 6:29Requirements for typed optimizations
- 7:11FCC implementation
- 7:52Q&A on row and recursive types
related talks
21mFlow-Analysis-Based Closure Optimization
29mClosure Conversion in Little Pieces
13mComputation Focusing
24mLocal Contextual Type Inference
13mOne-Pass CPS Translation of Dependent Types (Talk Proposal)
56mOn Type-Based Techniques for Program Manipulation
26mTemporal refinements for Call-By-Push-Value with fixpoint
35mFlattening Meets Effects: A Surprising Connection