2009 Fiscal Year Final Research Report
Foundation and Application of Delimited Continuations
| Project/Area Number |
18500005
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Fundamental theory of informatics
|
|---|
| Research Institution | Ochanomizu University |
|---|
Principal Investigator |
ASAI Kenichi Ochanomizu University, 大学院・人間文化創成科学研究科, 准教授 (10262156)
|
|---|
| Co-Investigator(Renkei-kenkyūsha) |
KAMEYAMA Yukiyoshi 筑波大学, 大学院・システム情報工学研究科, 准教授 (10195000)
|
|---|
| Project Period (FY) |
2006 – 2009
|
| Keywords | プログラム理論 / 部分継続 / 情報基礎 |
|---|
| Research Abstract |
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.
|
