Foundation and Application of Delimited Continuations

点击翻译按钮获取中文摘要

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.