Closure Conversion, Flat Environments, and the Complexity of Abstract Machines
Beniamino Accattoli, Cláudio Belo Lourenço, Dan R. Ghica, Giulio Guerrieri, Claudio Sacerdoti Coen · 2025
Closure conversion is a program transformation at work in compilers for functional languages to turn inner functions into global ones, by building closures pairing the transformed functions with the environment of their free variables. Abstract machines rely on similar and yet different concepts of closures and environments. We study the relationship between the two approaches. We adopt a simple λ -calculus with tuples as source language and study abstract machines for both the source language and the target of closure conversion. Moreover, we focus on the simple case of flat closures/environments (no sharing of environments). We provide three contributions. Firstly, a new simple proof technique for the correctness of closure conversion, inspired by abstract machines. Secondly, we show how the closure invariants of the target language allow us to design a new way of handling environments in abstract machines, not suffering the shortcomings of other styles.