Specification and Correctness of Lambda Lifting?

Adam Fischbach, John Hannan

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

7 Scopus citations

Abstract

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
Pages108-128
Number of pages21
ISBN (Print)3540410546, 9783540410546
Publication statusPublished - Jan 1 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)
Volume1924
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

OtherInternational Workshop on Semantics, Applications and Implementation of Program Generation, SAIG 2000
CountryCanada
CityMontreal
Period9/20/009/20/00

    Fingerprint

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Fischbach, A., & Hannan, J. (2000). Specification and Correctness of Lambda Lifting? In W. Taha (Ed.), Semantics, Applications and Implementation of Program Generation - International Workshop, SAIG 2000, Proceedings (pp. 108-128). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1924). Springer Verlag.