Closure Conversion in Little Pieces
summary
The paper makes closure conversion a syntactic equality by adding abstract closures to a CBPV-style IL, proving an equational theory sound and complete with respect to an environment abstract machine. Closure conversion and common optimizations become sequences of small β/η rewrites, so lambda lifting and environment-sharing optimizations are derivable as equalities and verified inside the IL rather than by cross-language logical relations; an extended CBPV with sharing captures call-by-need and the operational adequacy claims hold.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 1:06Closure environments
- 2:32Compiling closures
- 4:23Compiler architecture
- 6:11Traditional closure problems
- 9:28Abstract closures
- 11:13Call-by-push-value
- 13:21Placing closures
- 14:51Incremental conversion
- 17:00Lambda lifting
- 18:06Proving correctness of conversions
- 20:18Summary
- 22:25Q&A
related talks
14mAdequacy for Algebraic Effects Revisited
25mA Lazy, Concurrent Convertibility Checker
21mFlow-Analysis-Based Closure Optimization
11mType-Preserving Flat Closure Optimization
01h 05mAll the Languages Together
13mComputation Focusing
17mCalculational design of Incorrectness Separation Logic
30mTowards a Verified Cost Model for Call-by-Push-Value