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...

• Type: Journal
• Year: 2010
• Where: PPDP
• Authors: Kenichi Asai, Arisa Kitani
• Keywords: Data Stack, Delimited, Functional Derivation Approach, PPDP 2010, Programming Languages