Calculus and Logic of Delimited Continuations

定界延续的微积分和逻辑

• 批准号: 13680411
• 负责人: KAMEYAMA Yukiyoshi
• 金额: $ 2.11万
• 依托单位: University of Tsukuba
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2001
• 资助国家: 日本
• 起止时间: 2001 至 2003
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-13680411/
• 关键词: Control Operators; Software Verification; Delimited Continuations; Axiomatization; Functional Programming; Meta-variables; Contexts; 継続; CPS変換; コントロールオペレータ; カリー・ハワードの対応; 古典論理; 型理論

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

这个为期三年的项目的主要目的是从类型论和逻辑的角度研究函数编程中的控制算子，然后发展一种关于控制算子的理论，使人们能够用控制算子编写正确的程序。在这个项目中，我们专注于所谓的定界延续的控制运算符。我们的研究结果可以总结如下。(1)我们成功地给出了定界延拓中最著名和最广泛使用的控制算子“shift”和“reset”的一个合理而完整的公理化。（2）我们证明了shift和reset的公理是callcc公理的保守扩展，并且除了一个例外，增加的公理不是冗余的。这两个结果使我们能够对移位和复位进行推理，从而验证移位和复位程序的正确性。(3)我们还将上述结果推广到更高层次的移位和复位，由此我们可以联合收割机组合移位和复位的各种用途。由于控制算子操纵程序的元级控制结构，我们还研究了元变量和计算上下文的演算和逻辑，并在简单类型lambda演算的基础上得到了一个足够简单但功能强大的演算。我们的演算的一个特点是它既有文本替换，也有普通的捕获避免替换

项目成果

A.Taha: "A Second order context calculus"コンピュータ・ソフトウェア. 19-3. 2-19 (2002)

A.Taha：“二阶上下文微积分”计算机软件 19-3（2002）。

A.A.Taha, M.Sato, Y.Kameyama: "A Second Order Context Calculus"コンピュータソフトウェア. 19:3. 2-19 (2002)

A.A.Taha、M.Sato、Y.Kameyama：“二阶上下文微积分”计算机软件 19:3 (2002)。

Y.Kameyama, M.Hasegawa: "A Sound and Complete Axiomatization for Delimited Continuations"Proceedings of Eighth ACM International Conference on Functional Programming. 177-188 (2003)

Y.Kameyama、M.Hasekawa：“A Sound and Complete Axiomatization for Delimited Continuations”第八届 ACM 国际函数式编程会议论文集。

M.Sato, T.Sakurai, Y.Kameyama: "A Simply Typed Context Calculus with First Class Environments"Journal of Functional and Logic Progrmaming. 2002(4). 1-41 (2002)

M.Sato、T.Sakurai、Y.Kameyama：“具有一流环境的简单类型上下文演算”函数与逻辑编程杂志。

Y.Kameyama, M.Sato: "Strong Norm alizability of the Non-Deterministic Catch/Throw Calculi"Theoretical Computer Science. 272:1・2. 223-245 (2002)

Y.Kameyama、M.Sato：“非确定性 Catch/Throw 演算的强范数可验证性”理论计算机科学 272:1・2 (2002)。