@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",
year = "2000",
month = "1",
day = "1",
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",
note = "International Workshop on Semantics, Applications and Implementation of Program Generation, SAIG 2000 ; Conference date: 20-09-2000 Through 20-09-2000",
}