高度な制御機構の基礎理論の確立 - その安全で効率的な実装に向けて

• Project/Area Number: 25K14986
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Review Section: Basic Section 60010:Theory of informatics-related
• Research Institution: Ochanomizu University
• Principal Investigator: 浅井 健一 お茶の水女子大学, 基幹研究院, 教授 (10262156)
• Co-Investigator(Kenkyū-buntansha): 叢 悠悠 東京科学大学, 情報理工学院, 助教 (30847629)
• Project Period (FY): 2025-04-01 – 2029-03-31
• Project Status: Granted (Fiscal Year 2025)
• Budget Amount: ¥4,680,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥1,080,000); Fiscal Year 2028: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000); Fiscal Year 2027: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000); Fiscal Year 2026: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000); Fiscal Year 2025: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
• Keywords: 限定継続 / エフェクトハンドラ / 型システム

Outline of Research at the Start

４種類の限定継続演算子および２種類のエフェクトハンドラについて、定義を与えるインタプリタをベースにして、そこから最も一般的な型システムを与え、反映の証明および公理系の構築を行う。これを通して限定継続演算子、エフェクトハンドラの基礎理論を網羅的に確立する。この目標が達成されれば、複雑な制御機構を伴うプログラムの安全性が高まるだけでなく、プログラムの等価性の証明や効率的な実装などへ道を開くと期待される。