Construction of a framework for proving the correctness of program using computational effects

• Project/Area Number: 25K03098
• Research Category: Grant-in-Aid for Scientific Research (B)
• Allocation Type: Multi-year Fund
• Section: 一般
• Review Section: Basic Section 60050:Software-related
• Research Institution: Nagoya University
• Principal Investigator: J Garrigue 名古屋大学, 多元数理科学研究科, 教授 (80273530)
• Co-Investigator(Kenkyū-buntansha): 才川 隆文 名古屋大学, 多元数理科学研究科, 研究員 (00897100) ; Affeldt Reynald 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 上級主任研究員 (40415641) ; 田中 哲 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 主任研究員 (10357452) ; 勝股 審也 京都産業大学, 理学部, 教授 (30378963)
• Project Period (FY): 2025-04-01 – 2029-03-31
• Project Status: Granted (Fiscal Year 2025)
• Budget Amount: ¥18,720,000 (Direct Cost: ¥14,400,000、Indirect Cost: ¥4,320,000); Fiscal Year 2028: ¥4,550,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥1,050,000); Fiscal Year 2027: ¥4,550,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥1,050,000); Fiscal Year 2026: ¥4,810,000 (Direct Cost: ¥3,700,000、Indirect Cost: ¥1,110,000); Fiscal Year 2025: ¥4,810,000 (Direct Cost: ¥3,700,000、Indirect Cost: ¥1,110,000)
• Keywords: 等式理論 / 関数型プログラミング言語 / 計算効果 / 定理証明支援系

Outline of Research at the Start

実用的なプログラムの正しさの検証は，純粋なアルゴリズムの数学的正しさの検証に加えて, プログラムと外界や内部リソースとの相互作用（計算効果）の検証を含む．
本研究では計算効果を含む関数型プログラムの新しい検証枠組みを実装する．具体的には，モナドを使って書かれたOCamlのプログラムをRocq(旧Coq)に翻訳し，変換されたプログラムをモナド等式理論に基いて検証する．それによって，従来のホーア論理に基いたアプローチより直感的な検証方法の実現可能性を実証する．