研究課題
研究活動スタート支援
継続（残りの計算を表す概念）を操作するための言語機構を持つ計算体系に対して、型システムおよびプログラム変換を開発した。具体的な例としては、制御演算子の振る舞いを詳細に表現できる型システム、名前付き代数的効果に対する安全かつシンプルな型システム、制御演算子・代数的効果間の型と意味を保存するプログラム変換などが挙げられる。また、開発した型システムとプログラム変換に基づき、依存型と継続機構を持つ言語を Racket の Turnstile パッケージを用いて実装した。
プログラミング言語
型システムと継続機構はそれぞれプログラムの信頼性とプログラミング言語の表現力の向上に有用である。実際、研究期間中にさまざまなプログラミング言語のコミュニティで強力な型システムやプリミティブの継続機構を導入する動きが見られた。本研究ではこれらの基礎理論を構築したが、その中で得られた成果は安全なソフトウェアの簡潔な実装につながると考えられる。
