Specification and correctness of lambda lifting This material is based upon work supported by the National Science Foundation under Grant No. 9900918
| Autor: | John Hannan, Adam Fischbach |
|---|---|
| Rok vydání: | 2003 |
| Předmět: | |
| Zdroj: | Journal of Functional Programming. 13:509-543 |
| ISSN: | 1469-7653 0956-7968 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|