An Extensional Characterization of Lambda-Lifting and Lambda-Dropping

Olivier Danvy


Lambda-lifting and lambda-dropping respectively transform a block-structured functional program into recursive equations and vice versa. Lambda-lifting is known since the early 80's, whereas lambda-dropping is more recent. Both are split into an analysis and a transformation. Published work, however, has only concentrated on the analysis part. We focus here on the transformation part and more precisely on its formal correctness, which is an open problem. One of our two main theorems suggests us to define extensional versions of lambda-lifting and lambda-dropping, which we visualize both using ML and using type-directed partial evaluation.

See revised version BRICS-RS-99-21.

This website uses cookies to allow us to see how the site is used. The cookies cannot identify you or any content at your own computer.

ISSN: 0909-0878 

Hosted by the Royal Danish Library and Aarhus University Library