Analysis of proofs and computations via deepening the Curry-Howard isomorphism

• Project/Area Number: 25K07097
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Review Section: Basic Section 12030:Basic mathematics-related
• Research Institution: Tokyo Denki University
• Principal Investigator: 藤田 憲悦 東京電機大学, 理工学研究科, 特別専任教授 (30228994)
• Project Period (FY): 2025-04-01 – 2029-03-31
• Project Status: Granted (Fiscal Year 2025)
• Budget Amount: ¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000); Fiscal Year 2028: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000); Fiscal Year 2027: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000); Fiscal Year 2026: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000); Fiscal Year 2025: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
• Keywords: カリー・ハワード同型 / 証明 / 計算 / 型 / Girard's Paradox

Outline of Research at the Start

カリー・ハワード同型を深化させて，証明と計算の相互作用の解析にフィードバックさせる．研究の核心は，計算可能性・計算量を本質的に特徴付けている基本概念は何か？という根本問題である．そのために，証明と形式化された計算の関係からこの問題を追求する．まず，型理論，論理体系，そして意味論の関係を俯瞰して，健全かつ完全な意味論を精査して計算的複雑さを解析する．並行して，カリー・ハワード同型を掘り下げて，ラムダ計算におけるプログラム変換と論理的埋め込みとの対応関係を，双対性と決定可能性の観点から分析する．これらにより証明と計算の関係の深化を図り，可解性・計算量の基本問題を一層深く追求する基礎の構築を目指す．