The idea that programs are data forms the bedrock of functional programming languages, but it is also found in object-oriented languages and recent iterations of systems languages. Since passing and returning programs as data is incompatible with the architecture of modern machines, implementations of such a feature gives rise to closures, which package code with the environment that it needs to run. The first implementations of these objects are as part of the runtime system of an abstract machine. However, to be able to optimize these structures, compiler writers often choose instead to embed this structure in their code when compiling to lower-level languages in a transformation called closure conversion. While this transformation and closures more generally are well studied with respect to certain types of programming languages, how such a language interacts with different evaluation strategies still remains unstudied in a theoretical setting. Moreover, the current approaches to performing, optimizing, and proving correct this transformation lack the flexibility of other language features.

This thesis develops these ideas by presenting closure conversions for missing evaluation strategies, specifying a new implementation approach that allows for the flexible implementation and optimization of closures, and formalizing them in an intermediate language that captures multiple notions of closures and evaluation strategies in one. Our approach follows from first principles meaning that our closures are a reflection of the environment-based abstract machines that birth them. We develop an approach to reasoning about closures that connects their equational properties with the abstract machines on which they run. Thereby, we can prove not only that closure conversion does not change the output of programs, but that closure conversion removes the need for the runtime system to capture closures.

This dissertation includes previously published, co-authored material.