Hostname: page-component-586b7cd67f-l7hp2 Total loading time: 0 Render date: 2024-12-02T21:46:58.135Z Has data issue: false hasContentIssue false
  • English
  • Français

Specification and correctness of lambda lifting

Published online by Cambridge University Press:  13 May 2003

ADAM FISCHBACH  and
JOHN HANNAN
ADAM FISCHBACH
Affiliation:
Department of Computer Science and Engineering, The Pennsylvania State University, University Park, PA 16802, USA (email: [email protected]
JOHN HANNAN
Affiliation:
Department of Computer Science and Engineering, The Pennsylvania State University, University Park, PA 16802, USA (email: [email protected]
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

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 optimizations can be studied and from which new algorithms might be obtained.

Type
Research Article
Information
Journal of Functional Programming , Volume 13 , Issue 3 , May 2003 , pp. 509 - 543
Copyright
© 2003 Cambridge University Press

Footnotes

This material is based upon work supported by the National Science Foundation under Grant No. 9900918.
Submit a response

Discussions

No Discussions have been published for this article.