An Extensional Characterization of Lambda-Lifting and Lambda-Dropping; Formalizing Implementation Strategies for First-Class Continuations Seminars/Workshops

Abstract

An Extensional Characterization of Lambda-Lifting and Lambda-Dropping

Lambda-lifting and lambda-dropping respectively transform a block-structured functional program into recursive equations and vice versa. Lambda-lifting was developed in 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 parts. We focus here on the transformation parts and more precisely on their correctness, which appears never to have been proven. To this end, we define extensional versions of lambda-lifting and lambda-dropping and establish their correctness with respect to a least fixed-point semantics.

[presented at FLOPS'99]

We present the first formalization of implementation strategies for first-class continuations. The formalization hinges on abstract machines for continuation-passing style (CPS) programs with a special treatment for the current continuation, accounting for the essence of first-class continuations. These abstract machines are proven equivalent to a standard, substitution-based abstract machine. The proof technique -- stack substitution and induction on derivations -- works uniformly for various representations of continuations. As a byproduct, we also present the first formal proof of the folklore theorem that one register is enough for second-class continuations.

A large body of work exists on implementing first-class continuations, but it is predominantly empirical and implementation-oriented. In contrast, our formalization abstracts the essence of first-class continuations and provides a uniform setting for specifying and formalizing their representation. As an example, we show how to garbage collect unshared continuations incrementally.

[presented at Marktoberdorf'99]