| 研究課題/領域番号 |
19K24339
|
|---|
| 研究種目 |
研究活動スタート支援
|
| 配分区分 | 基金 |
|---|
| 審査区分 |
1001:情報科学、情報工学およびその関連分野
|
|---|
| 研究機関 | 東京工業大学 |
|---|
研究代表者 |
叢 悠悠 東京工業大学, 情報理工学院, 助教 (30847629)
|
|---|
| 研究期間 (年度) |
2019-08-30 – 2024-03-31
|
| 研究課題ステータス |
完了 (2023年度)
|
| 配分額 *注記 |
1,950千円 (直接経費: 1,500千円、間接経費: 450千円)
2020年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2019年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
|
|---|
| キーワード | 依存型 / 代数的効果 / 制御演算子 / 限定継続命令 / プログラム変換 / 型理論 / 副作用 / 継続 |
|---|
| 研究開始時の研究の概要 |
依存型と代数的効果は、それぞれプログラムの仕様の記述と、複雑な動作の実装に役立つツールである。これらを共存させると、信頼性と表現力を両立できると考えられるが、プログラムが仕様通りに振る舞うことの保証や、言語の実装に多大な労力がかかってしまう。
本研究では、代数的効果をもつ依存型付き言語をなるべく低いコストで実装する。アイディアとしては、制御演算子（実行の流れを操作するための演算子）に関する研究成果と、関数型言語 Racket のインフラを利用することで、証明や実装の手順を単純化する。これによって、意図通りに動作するソフトウェアの実装がより現実的になることが期待される。
|
| 研究成果の概要 |
継続（残りの計算を表す概念）を操作するための言語機構を持つ計算体系に対して、型システムおよびプログラム変換を開発した。具体的な例としては、制御演算子の振る舞いを詳細に表現できる型システム、名前付き代数的効果に対する安全かつシンプルな型システム、制御演算子・代数的効果間の型と意味を保存するプログラム変換などが挙げられる。また、開発した型システムとプログラム変換に基づき、依存型と継続機構を持つ言語を Racket の Turnstile パッケージを用いて実装した。
|
| 研究成果の学術的意義や社会的意義 |
型システムと継続機構はそれぞれプログラムの信頼性とプログラミング言語の表現力の向上に有用である。実際、研究期間中にさまざまなプログラミング言語のコミュニティで強力な型システムやプリミティブの継続機構を導入する動きが見られた。本研究ではこれらの基礎理論を構築したが、その中で得られた成果は安全なソフトウェアの簡潔な実装につながると考えられる。
|
