Foundation and Application of Delimited Continuations

定界延续的基础和应用

• 批准号: 18500005
• 负责人: ASAI Kenichi
• 金额: $ 2.49万
• 依托单位: Ochanomizu University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2006
• 资助国家: 日本
• 起止时间: 2006 至 2009
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-18500005/
• 关键词: プログラム理論; 部分継続; 情報基礎

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.

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

项目成果

限定継続を含む仮想機械導出のためのプログラム変換

用于派生虚拟机（包括有限延续）的程序转换

• 发表时间: 2009
• 期刊: 第1 1回プログラミングおよびプログラミング言語ワークショップ
• 作者: 木谷有沙;浅井健一
• 通讯作者: 浅井健一

shift/reset による Caml Light の拡張に向けて

通过移位/重置来扩展 Caml Light

• 发表时间: 2010
• 期刊: 第12回プログラミングおよびプログラミング言語ワークショップ
• 作者: 増子萌;浅井健一
• 通讯作者: 浅井健一

Locally Nameless手法を使った継続計算に対する型システムの健全性の証明

使用局部无名技术证明连续计算的类型系统的健全性

• 发表时间: 2008
• 作者: 廣田知子;浅井健一
• 通讯作者: 浅井健一

Polymorphic Delimited Continuations

多态分隔延续

• 发表时间: 2007
• 期刊: Proc. Fifth Asian Symposium onProgramming Languages and Systems(APLAS 2007), Singapore, LectureNotes in Computer Science 4807
• 作者: Kenichi Asai;Yukiyoshi Kameyama
• 通讯作者: Yukiyoshi Kameyama

On Typing Delimited Continuations : Three New Solutions to the Printf Problem

关于输入定界延续：Printf 问题的三种新解决方案

• 发表时间: 2009
• 期刊: Higher-Order and Symbolic Computation 22:3
• 作者: 木谷有沙;浅井健一;J. Tarui;浅井健一
• 通讯作者: 浅井健一