一句话：提出 Flat-Closure Calculus，用类型保持的闭包表示支持常见闭包优化，并证明类型安全与类型保持。
类型保持编译将类型所表达的意图保留到编译和链接阶段，以提供轻量级保证，但通常妨碍重要优化。本文研究带类型的闭包表示与优化，分析既有 typed closure conversion 表示的局限，以及多种重要闭包优化对表示的要求。作者提出 Flat-Closure Calculus（FCC），设计新的带类型闭包表示，使其能够容纳这些优化；证明 FCC 的类型安全与 subject reduction，证明从已有 closure-converted IR 到 FCC 的类型保持，并为 FCC 实现常见闭包优化。
Type-preserving compilation seeks to make intent as much as a part of compilation as computation . Specifications of intent in the form of types are preserved and exploited during compilation and linking, alongside the mere computation of a program. This provides lightweight guarantees for compilation, optimization, and linking. Unfortunately, type-preserving compilation typically interferes with important optimizations. In this paper, we study typed closure representation and optimization. We analyze limitations in prior typed closure conversion representations, and the requirements of many important closure optimizations. We design a new typed closure representation in our Flat-Closure Calculus (FCC) that admits all these optimizations, prove type safety and subject reduction of FCC, prove type preservation from an existing closure converted IR to FCC, and implement common closure optimizations for FCC.
@article{paperbot3200,
title = {Type-Preserving Flat Closure Optimization},
author = {Adam T. Geller and Sean Bocirnea and Chester J. F. Gould and Paulette Koronkevich and William J. Bowman},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA1},
year = {2025},
doi = {10.1145/3720437}
}