Closure conversion, an essential step in compiling functional programs, is traditionally presented as a global transformation from a language with higher-order functions to one without. Optimizing this transformation can be done at any of its three stages with various tradeoffs. After conversion, optimizations will be in the target language at the cost of a weaker equational theory. During conversion, optimizations may be embedded into the transformation itself at the cost of increasing its complexity and correctness. And before conversion, optimizations may be planned and anticipated in a specialized intermediate language (IL) where all the properties of the source program are still known, with the hope that they will survive the rest of the compilation process.

By building on the notion of abstract closures, we blur the distinctions between these three approaches to closure conversion and optimizations thereof, by combining all of their strengths and avoiding their weaknesses. Specifically, we develop an IL that includes closures alongside unclosed higher-order code, even inhabiting the same type. The IL comes equipped with an equational theory that is shown sound and complete with respect to an environment abstract machine. Thereby, a baseline closure conversion and common optimizations become provable equalities and thus are correct by construction. Moreover, the transformation and its correctness proof are broken down into little steps—as instances of the $\beta$ and $\eta$ axioms—instead of being expressed in terms of a recursive procedure.

Our proposed IL is based on call-by-push-value which we extend with sharing in order to capture closure conversion for both strict and lazy languages.