| Project/Area Number |
19K24339
|
|---|
| Research Category |
Grant-in-Aid for Research Activity Start-up
|
| Allocation Type | Multi-year Fund |
|---|
| Review Section |
1001:Information science, computer engineering, and related fields
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
Cong Youyou 東京工業大学, 情報理工学院, 助教 (30847629)
|
|---|
| Project Period (FY) |
2019-08-30 – 2024-03-31
|
| Project Status |
Completed (Fiscal Year 2023)
|
| Budget Amount *help |
¥1,950,000 (Direct Cost: ¥1,500,000、Indirect Cost: ¥450,000)
Fiscal Year 2020: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2019: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
|
|---|
| Keywords | 依存型 / 代数的効果 / 制御演算子 / 限定継続命令 / プログラム変換 / 型理論 / 副作用 / 継続 |
|---|
| Outline of Research at the Start |
依存型と代数的効果は、それぞれプログラムの仕様の記述と、複雑な動作の実装に役立つツールである。これらを共存させると、信頼性と表現力を両立できると考えられるが、プログラムが仕様通りに振る舞うことの保証や、言語の実装に多大な労力がかかってしまう。
本研究では、代数的効果をもつ依存型付き言語をなるべく低いコストで実装する。アイディアとしては、制御演算子（実行の流れを操作するための演算子）に関する研究成果と、関数型言語 Racket のインフラを利用することで、証明や実装の手順を単純化する。これによって、意図通りに動作するソフトウェアの実装がより現実的になることが期待される。
|
| Outline of Final Research Achievements |
I developed type systems and program transformations for calculi that have constructs for manipulating continuations. Examples include a type system that can describe the detailed behavior of control operators, a simple type system that ensures safe use of named effect handlers, and program translations that convert between control operators and effect handlers. I also implemented a dependently typed language with effect handlers based on the type systems and program translations I developed and using the Turnstile package of the Racket language.
|
| Academic Significance and Societal Importance of the Research Achievements |
型システムと継続機構はそれぞれプログラムの信頼性とプログラミング言語の表現力の向上に有用である。実際、研究期間中にさまざまなプログラミング言語のコミュニティで強力な型システムやプリミティブの継続機構を導入する動きが見られた。本研究ではこれらの基礎理論を構築したが、その中で得られた成果は安全なソフトウェアの簡潔な実装につながると考えられる。
|
