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

1996 Fiscal Year Annual Research Report

• Project/Area Number: 07044093
• Research Institution: Keio University
• Principal Investigator: 岡田 光弘 慶応義塾大学, 文学部, 教授 (30224025)
• Co-Investigator(Kenkyū-buntansha): 林 晋 神戸大学, 工学部, 教授 (40156443) ; 高橋 正子 東京工業大学, 理学部, 助教授 (00015588) ; 大堀 淳 京都大学, 数理解析研究所, 助教授 (60252532) ; 萩谷 昌己 東京大学, 理学部, 教授 (30156252) ; 佐藤 雅彦 京都大学, 工学部, 教授 (20027387)
• Keywords: タイプ理論 / 線形理論 / 構成的証明 / プログラミング言語 / プログラム検証 / プログラム意味論 / 平行計算 / 直観主義理論

Research Abstract

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

Research Products

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