Specification and correctness of lambda lifting

Adam Fischbach, John Hannan

Research output: Contribution to journalArticle

4 Citations (Scopus)

Abstract

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

Original languageEnglish (US)
Pages (from-to)509-543
Number of pages35
JournalJournal of Functional Programming
Volume13
Issue number3
DOIs
StatePublished - May 2003

Fingerprint

Specifications
Semantics

All Science Journal Classification (ASJC) codes

  • Software

Cite this

@article{e30da5c3abd446b091292af3cc4625dc,
title = "Specification and correctness of lambda lifting",
abstract = "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 optimisations can be studied and from which new algorithms might be obtained.",
author = "Adam Fischbach and John Hannan",
year = "2003",
month = "5",
doi = "10.1017/S0956796802004604",
language = "English (US)",
volume = "13",
pages = "509--543",
journal = "Journal of Functional Programming",
issn = "0956-7968",
publisher = "Cambridge University Press",
number = "3",

}

Specification and correctness of lambda lifting. / Fischbach, Adam; Hannan, John.

In: Journal of Functional Programming, Vol. 13, No. 3, 05.2003, p. 509-543.

Research output: Contribution to journalArticle

TY - JOUR

T1 - Specification and correctness of lambda lifting

AU - Fischbach, Adam

AU - Hannan, John

PY - 2003/5

Y1 - 2003/5

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

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

UR - http://www.scopus.com/inward/record.url?scp=0037851828&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0037851828&partnerID=8YFLogxK

U2 - 10.1017/S0956796802004604

DO - 10.1017/S0956796802004604

M3 - Article

AN - SCOPUS:0037851828

VL - 13

SP - 509

EP - 543

JO - Journal of Functional Programming

JF - Journal of Functional Programming

SN - 0956-7968

IS - 3

ER -