Functional Derivation of a Virtual Machine for Delimited Continuations
This paper connects the definitional interpreter for the
lambda-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-level implementations.