Calculus and Logic of Delimited Continuations

这个为期三年的项目的主要目的是从类型论和逻辑的观点来研究函数式程序设计中的控制操作符，然后发展一个关于控制操作符的理论，使人们能够用控制操作符编写正确的程序。在这个项目中，我们主要研究所谓的定界延拓的控制算子。我们的研究成果可以概括为以下几点。(2)我们证明了移位和重置公理是相对于CALCC公理的保守推广，所增加的公理不是多余的，只有一个例外。这两个结果使人们能够对移位和重置进行推理，从而可以验证移位和重置程序的正确性。(3)我们还将上述结果推广到更高级别的移位和重置，从而可以将移位和重置的各种用法结合起来。由于控制算子操纵程序的元级控制结构，我们还研究了元变量和计算上下文的演算和逻辑，并在简单类型的lambda演算的基础上得到了一个足够简单但功能强大的演算。我们的演算的一个特征是它既有文本替换，也有普通的捕获避免替换

The main purpose of this three-year project is to study the control operators in functional programming from 'the viewpoint of type theory and logic, and then develop a theory on the control operators which enables one to write correct programs with control operators. In this project we focus on the control operators for so called delimited continuations. Our research results can be summarized as follows. (1) We have succesfully given a sound and complete axiomatization for "shift" and "reset", the most well known, and widely used control operators for delimited continuations, (2) We have shown that the axioms for shift and reset are a conservative extension over those for callcc, and that the added axioms are not redundant with one exception. These two results enable one to reason about shift and reset, thus we can verify the correctness of programs with shift and reset. (3) We have also extended the above results to the higher-level shift and reset, by which we can combine various uses of shift and reset. The resulting axioms are surprisingly simple and thus can be used to software verification, tooSince control operators manipulate mete-level control structures of programs, we }lave also study the calculi and logic of mete-variables and computational contexts, and obtained a sufficiently simple, but powerful calculi based on the simply typed lambda calculi. A characteristic feature of our calculus is that it has the textual substitution as well as the ordinary capture-avoiding substitution