Specification and correctness of lambda lifting

Adam Fischbach, John Hannan

Research output: Contribution to journalArticlepeer-review

5 Scopus citations


We present a formal and general specification of lambda lifting and prove its correctness with respect to a call-by-name operational semantics. We use this specification to prove the correctness of a lambda lifting algorithm similar to the one proposed by Johnsson. Lambda lifting is a program transformation that eliminates free variables from functions by introducing additional formal parameters to function definitions 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 and only limited correctness results. Our work provides a more general specification of lambda lifting (and related operations) that 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 optimisations can be studied and from which new algorithms might be obtained.

Original languageEnglish (US)
Pages (from-to)509-543
Number of pages35
JournalJournal of Functional Programming
Issue number3
StatePublished - May 2003

All Science Journal Classification (ASJC) codes

  • Software


Dive into the research topics of 'Specification and correctness of lambda lifting'. Together they form a unique fingerprint.

Cite this