Specification and Correctness of Lambda Lifting?

Adam Fischbach, John Hannan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Scopus citations


We present a formal and general specification of lambda lift- ing and prove its correctness with respect to an operational semantics. Lambda lifting is a program transformation which eliminates free vari- ables from functions by introducing additional formal parameters to func- tion definition and additional actual parameters to function calls. This operation supports the transformation from a lexically-structured func- tional 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 trans- lation 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.

Original languageEnglish (US)
Title of host publicationSemantics, Applications and Implementation of Program Generation - International Workshop, SAIG 2000, Proceedings
EditorsWalid Taha
PublisherSpringer Verlag
Number of pages21
ISBN (Print)3540410546, 9783540410546
StatePublished - 2000
EventInternational Workshop on Semantics, Applications and Implementation of Program Generation, SAIG 2000 - Montreal, Canada
Duration: Sep 20 2000Sep 20 2000

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


OtherInternational Workshop on Semantics, Applications and Implementation of Program Generation, SAIG 2000

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Specification and Correctness of Lambda Lifting?'. Together they form a unique fingerprint.

Cite this