Sciweavers

Share
PPDP
2010
Springer

Functional derivation of a virtual machine for delimited continuations

9 years 29 days ago
Functional derivation of a virtual machine for delimited continuations
This paper connects the definitional interpreter for the λ-calculus extended with delimited continuation constructs, shift and reset, with a compiler and a low-level virtual machine that copies a part of a data stack to implement delimited continuations. Following the functional derivation approach proposed and popularized by Danvy, we interrelate the two implementations via a series of meaning-preserving program transformations whose validity is independently known. As a result, this work formally establishes the correctness of a compiler and a low-level stack-copying implementation of delimited continuations. In particular, the resulting virtual machine properly models when to store return addresses into a data stack and which part of a data stack to copy. To our knowledge, this work is the first to prove correctness of such low-level features of delimited continuations. It also shows that the functional derivation approach is equally applicable to establish correctness of low-le...
Kenichi Asai, Arisa Kitani
Added 29 Jan 2011
Updated 29 Jan 2011
Type Journal
Year 2010
Where PPDP
Authors Kenichi Asai, Arisa Kitani
Comments (0)
books