タイプ理論及び線形理論のプログラム言語理論への応用

1996 年度 実績報告書

• 研究課題/領域番号: 07044093
• 研究機関: 慶応義塾大学
• 研究代表者: 岡田 光弘 慶応義塾大学, 文学部, 教授 (30224025)
• 研究分担者: 林 晋 神戸大学, 工学部, 教授 (40156443) ; 高橋 正子 東京工業大学, 理学部, 助教授 (00015588) ; 大堀 淳 京都大学, 数理解析研究所, 助教授 (60252532) ; 萩谷 昌己 東京大学, 理学部, 教授 (30156252) ; 佐藤 雅彦 京都大学, 工学部, 教授 (20027387)
• キーワード: タイプ理論 / 線形理論 / 構成的証明 / プログラミング言語 / プログラム検証 / プログラム意味論 / 平行計算 / 直観主義理論

研究概要

タイプ理論及び線形論理に基づいて新しいプログラム言語を設計することを目指して、その基礎理論、特にプログラム言語の計算モデルの理論を研究し、その成果を基にして、プログラム検証、プログラム自動抽出、プログラムの構成的開発の理論等を、この線形タイプ理論言語(タイプ理論と線形論理を組み合わせた形式言語)の上で発展させた。この言語によるプログラムはcurry-Howard同型定理により、論理的証明と同一視できる。よって、プログラム検証、プログラム自動抽出、プログラム構成的開発等の理論は、論理的(形式的)証明の検証、自動抽出、構成的開発の理論を直接的に応用して得ることができた。特に線形論理の証明概念をこれまでの伝統的直観主義論理の証明概念のかかわりに用いることにより、計算資源の消費概念や並行計算プログラミングの概念等これまでの伝統的タイプ理論では得られなかったプログラミングのコントロールがタイプ理論言語上で可能となった。

研究成果

• [文献書誌] J-P. Jouannaud 岡田光弘: "Abstract Data Type Systems" Theoretical Computer Science. (近刊). (1997)
• [文献書誌] 岡田光弘(研究協力者浜野正浩との共著): "A Direct Independent Proof of Buchholz's Hydra Game on Lableled Finite Trees" Archive for Mathematical Logic. (近刊). (1997)
• [文献書誌] 岡田光弘(研究協力者浜野正浩との共著): "A Relationship Among Gentzen's Proof -Reduction, Kirby-Paris Hydra Game and Buchholz's Hydra Game" Mathematical Logic Quarterly. 43. 105-120 (1997)
• [文献書誌] 林晋: "Two Extensions of PX Systems" Electronic Notes of Theoretical Computer Science. 3. 12 (1996)
• [文献書誌] Jean-Yves Girard: "Coherent Banach Spaces" Electronic Notes of Theoretical Computer Science. 3. 13 (1996)
• [文献書誌] Jean-Yves Girard: "Denotational Completeness" Electronic Notes of Theoretical Computer Science. 3. 9 (1996)
• [文献書誌] J-Y. Girard 岡田光弘 Andre Scedrove: "Linear Logic (Special Issue of Theoretial Computer Science)" Elsevier-EATCS(オランダ)(予定), 190 (1997)
• [文献書誌] 岡田光弘: "情報科学のための論理学" 産業図書(近刊)(予定), (1997)
• [文献書誌] 大堀淳: "プログラミング言語の基礎理論" 共立出版, 273 (1997)
• [文献書誌] J-Y. Girard(研究協力者Y. Lafont, L. Regnierとの共著): "Advances in Linear Logic" Cambridge University Press, 389 (1996)
• [文献書誌] J-Y. Girard(研究協力者Y. Lafont, L. Regnierとの共編): "Advances in Linear Logic" Cambridge University Press, 389 (1996)
• [文献書誌] J-Y. Girard 岡田光弘 Andre Scedrov(共編): "Linear Logic, A special issue of Electronic Notes of Theoretical Computer Science" Elsevier-EATCS(オランダ)(欧州理論情報学会), 256 (1996)