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

1999 年度 実績報告書

• 研究課題/領域番号: 10044094
• 研究機関: 慶應義塾大学
• 研究代表者: 岡田 光弘 慶応義塾大学, 文学部, 教授 (30224025)
• 研究分担者: 萩谷 昌己 東京大学, 大学院・理学系研究科, 教授 (30156252) ; 米澤 明憲 東京大学, 大学院・理学系研究科, 教授 (00133116) ; 林 晋 神戸大学, 工学部, 教授 (40156443) ; 大堀 淳 京都大学, 数理解析研究所, 教授 (60252532) ; 高橋 正子 東京工業大学, 理学部, 教授 (00015588)
• キーワード: プログラミング言語 / 線形論理 / タイプ理論

研究概要

昨年度は線形論理とタイプ理論とを組み合わせた線形タイプ言語の計算モデルの理論を確立したが、本年度は前年度に確立した計算モデルの理論に基づいて、線形タイプ理論によるプログラミング言語の設計のための理論を構築した。
線形タイプ理論言語による並行計算プログラミング設計のための理論とこの言語を用いた並行計算プログラミング方法論を考察した。また、実現可能計算量(多項式時間計算量および多項式空間計算量)のための意味論的手法の確立、および我々の線形タイプ・プログラミング言語の設計への応用を行った。
線形理論とタイプ理論を組み合わせた線形タイプ言語に基づく線形タイプ・プログラム言語の線形論理証明システムとプログラム自動検証・自動抽出部分の設計の理論も構築した。特に今年度は米国側共同研究者たちとソフトウェアの形式仕様、形式検証のための方法論の開発を行った。また、フランス、イタリアを中心とした欧州の共同研究者グループとは、線形論理的手法のプログラミング方法論への応用に関する手法を共同で開発してきた。これらの成果はわれわれの言語設計に生かされている。
本研究課題で構築した新しいプログラミング言語理論を基にして、フランス国立情報科学研究所(INRIA)などと協力して言語の実装を計画している。

研究成果

• [文献書誌] M.Okada and K.Terui: "Finite Model Property for Various Fragments of Intuitionistic Linear Logic"Journal of Symbolic Logic. 64. 790-801 (1999)
• [文献書誌] M.Okada: "A Phase-Semantic Higher Cut-elimination and Normalization Proofs of Classical Linear Logic"Theoretical Computer Science. 227. 333-396 (1999)
• [文献書誌] M.Okada and P.J.Scott: "A Note on Rewriting Theory for Uniquenss of Iteration"Journal of Theory ahd Applications of Categories. 6. 47-64 (1999)
• [文献書誌] F.Blanqui,J-P.Jouannaud and M.Okada: "Inductive data Type Systems:"Theoretical Computer Science. (近刊).
• [文献書誌] F.Blanqui,J-P.Jouannaud and M.Okada: "Calculus of Inductive Construction"Proc.Of Rewriting Technique and Application(RTA99),Springer-Lecture Note in Computer Science. 1631. 301-316 (1999)
• [文献書誌] M.Kanovitch,M.Okada and A.Scedrov: "Phase Semantics for Light Linear Logic"Theoretical Computer Science. (近刊).
• [文献書誌] M.Okada: "Theories of Types and Proofs,second edition,Memoir of Mathematical society of Japan vol.2"Mathematical Society of Japan. (1999)
• [文献書誌] 岡田 光弘: "法律人工知能(共著)"創成社出版. (2000)