Specification and Correctness of Lambda Lifting

We present a formal and general specification of lambda lifting and prove its correctness with respect to an operational semantics. Lambda lifting is a program transformation which eliminates free variables from functions by introducing additional formal parameters to function definition and additional actual parameters to function calls. This operation supports the transformation from a lexically-structured functional program into a set of recursive equations. Existing results provide specific algorithms with no flexibility, no general specification, and only limited correctness results. Our work provides a general specification of lambda lifting (and related operations) which supports flexible translation strategies which may result in new implementation techniques. Our work also supports a simple framework in which the interaction of lambda lifting and other optimizations can be studied and from which new algorithms might be obtained.