Derivation of an Abstract Machine for
Lambda-calculus with Delimited Continuation
The goal of our research is to give a verified virtual
machine for the lambda-calculus with delimited continuation
constructs, shift and reset, and ultimately to give a formal
for the direct implementation of shift/reset in the machine language.
Toward this goal,
we derive an abstract machine and transition rules from the CPS
interpreter defining shift/reset, using a series of transformations
whose validity is proved.
Following the "functional correspondence" approach advocated by Danvy,
we first perform the CPS transformation and defunctionalization.
Unlike the previous approach, however, we introduce two new
transformations, stack introduction and environment storing, to turn
the interpreter closer to the actual implementation.
After stack introduction, the abstract machine stores the result of
execution in a stack rather than holding it in machine instructions.
After environment storing, the bindings of necessary variables after
function calls are stored explicitly in a stack, mimicking the
standard calling convention of the compiled programs.
In this article, we show correctness proofs of the two transformations
using the bisimulation method.
Consequently, we succeeded in deriving an abstract machine that stores
bindings in the stack from the original CPS interpreter using
validated transformations only.