Foundation and Application of Delimited Continuations

传统的单形类型系统的界定延续扩展到科普多态性。证明了类型系统的各种性质，如类型可靠性。使用Coq证明助手形式化了类型可靠性。定界延续的低级别实现，复制堆栈的一部分被证明是系统地从他们的定义解释器派生。基于该技术，构造了一个产生机器码的编译器。作为用分隔的延续结构实现的。

The conventional monomorphic type system for delimited continuations is extended to cope with polymorphism. The various properties of the type system are proved, such as type soundness. The type soundness is formalized using the Coq proof assistant. Ther low-level implementation of delimited continuations that copies a part of stack is shown to be systematically derivable from their definitional interpreter. Based on the technique, a compiler that produces machine code is constructed. As annaturally implemented with delimited continuation constructs.