An Extensional Characterization of Lambda-Lifting and Lambda-Dropping; Formalizing Implementation Strategies for First-Class Continuations Seminars/Workshops
|Place:||Rm.1403, CS Bldg./KAIST|
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
[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]
[ List ]