Specification and Correctness of Lambda Lifting?

Adam Fischbach; John Hannan

doi:10.1007/3-540-45350-4_10

Specification and Correctness of Lambda Lifting?

Adam Fischbach, John Hannan

Computer Science and Engineering

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English (US)
Title of host publication	Semantics, Applications and Implementation of Program Generation - International Workshop, SAIG 2000, Proceedings
Editors	Walid Taha
Publisher	Springer Verlag
Pages	108-128
Number of pages	21
ISBN (Print)	3540410546, 9783540410546
DOIs	https://doi.org/10.1007/3-540-45350-4_10
State	Published - 2000
Event	International Workshop on Semantics, Applications and Implementation of Program Generation, SAIG 2000 - Montreal, Canada Duration: Sep 20 2000 → Sep 20 2000

Publication series

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

Other

Other	International Workshop on Semantics, Applications and Implementation of Program Generation, SAIG 2000
Country/Territory	Canada
City	Montreal
Period	9/20/00 → 9/20/00

All Science Journal Classification (ASJC) codes

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/3-540-45350-4_10

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. https://doi.org/10.1007/3-540-45350-4_10

Fischbach, Adam ; Hannan, John. / Specification and Correctness of Lambda Lifting?. Semantics, Applications and Implementation of Program Generation - International Workshop, SAIG 2000, Proceedings. editor / Walid Taha. Springer Verlag, 2000. pp. 108-128 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{0d896e7973e0442c8dc5349357ef9bdf,

title = "Specification and Correctness of Lambda Lifting?",

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.",

author = "Adam Fischbach and John Hannan",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 2000.; International Workshop on Semantics, Applications and Implementation of Program Generation, SAIG 2000 ; Conference date: 20-09-2000 Through 20-09-2000",

year = "2000",

doi = "10.1007/3-540-45350-4_10",

language = "English (US)",

isbn = "3540410546",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "108--128",

editor = "Walid Taha",

booktitle = "Semantics, Applications and Implementation of Program Generation - International Workshop, SAIG 2000, Proceedings",

address = "Germany",

}

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. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1924, Springer Verlag, pp. 108-128, International Workshop on Semantics, Applications and Implementation of Program Generation, SAIG 2000, Montreal, Canada, 9/20/00. https://doi.org/10.1007/3-540-45350-4_10

Specification and Correctness of Lambda Lifting? / Fischbach, Adam; Hannan, John.
Semantics, Applications and Implementation of Program Generation - International Workshop, SAIG 2000, Proceedings. ed. / Walid Taha. Springer Verlag, 2000. p. 108-128 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1924).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution