2014 Fiscal Year Final Research Report
Calculi for Call-by-Need and Control Abstraction
| Project/Area Number |
25540023
|
|---|
| Research Category |
Grant-in-Aid for Challenging Exploratory Research
|
| Allocation Type | Multi-year Fund |
|---|
| Research Field |
Software
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
|
|---|
| Research Collaborator |
TANAKA Asami 筑波大学, システム情報工学研究科
KOBORI Ikuo 筑波大学, システム情報工学研究科
|
|---|
| Project Period (FY) |
2013-04-01 – 2015-03-31
|
| Keywords | コントロール抽象 / 関数型プログラム言語 / 計算モデル / 型システム / プログラム変換 |
|---|
| Outline of Final Research Achievements |
This research focused on control abstraction in programming languages. In particular, we have studied how control operators are formulated in terms of foundational calculi, and how they can represent interesting control structures in a sophisticated way. We have revealed that the mechanism of Answer-Type Modification for delimited-control operators is essential for a certain interesting programming idioms, and a program with this mechanism can be translated to a program without it. Our translation is novel and sufficiently general, in that any programs with this mechanism can be translated in main-stream functional programming languages such as OCaml and Haskell, thus widening the application area of control operators drastically. We have given a rigid proof for the type preservation property of this translation as well as a concrete implementation in the tagless-final style.
|
| Free Research Field |
プログラム論理
|
