Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages
summary
An abstract-interpretation analysis discovers which free-variable bindings are always shared so callers can supply environments instead of heap-allocating closures, formalized in the Rocq proof assistant and shipped with evaluated artifacts. On benchmarks the analysis often matches the ground truth, yields up to 1.5× more precise sharing than lightweight closure conversion, and scales (a 30,000-line program runs in ≈20 ms). An instrumented interpreter shows the transformation meaningfully reduces dynamic allocations when decisions follow the paper’s heuristics.
AI-written summary · about
chapters (12)
- 0:00Environment sharing analysis intro
- 1:02Optimizing closure space
- 3:133CPS compiler phases
- 4:15Tracking sharing info
- 7:42Abstract interpretation for sharing
- 9:26Precision and scalability of analysis
- 10:51Transforming with caller environments
- 14:02Heuristics for transformations
- 14:23Evaluating closure savings
- 15:26Frame pointers for closures
- 17:53Conclusion and future
- 18:34Q&A