論理的手法を用いたプログラミング言語の計算モデルの理論

1998 年度 実績報告書

• 研究課題/領域番号: 09480058
• 研究機関: 慶応義塾大学
• 研究代表者: 岡田 光弘 慶應義塾大学, 文学部, 教授 (30224025)
• キーワード: 線形論理 / 相意味論 / 証明の正規化定理 / (強)停止性 / 計算モデル / 高階論理 / 並行計算 / カット消去定理

研究概要

昨年度までに与えた「証明の正規化定理」に対する相意味論による意味論的証明手法をさらに改良して、種々の論理体系の違いに依存しない統一的な意味論的証明法を与えた。又、この統一的な意味論的証明法を応用して、種々の論理体系に対する「証明の正規化定理」を与えた。特に、種々の異なる関数型言語(タイプ付ラムダ計算言語、項書換え系言語、線形論理言語)を融合したマルチパラダイム関数型プログラミング言語に対する計算モデル(特に、その計算モデルの上での強停止性)を確立した。又、高階並行計算言語、ペトリネット計算モデル、実現可能計算量に対する関数型言語、実時間並行計算システムの仕様・検証用言語等に対する計算モデルを与え、その強停止性を示すために、上記の意味論的証明が応用された。

研究成果

• [文献書誌] M.Okada: "Phase Semantics for Higher Order Completeness,Cut-Elimination and Normalization Proofs of Classical Linear Logic" Theoretical Computer Science. (近刊). (1999)
• [文献書誌] M.Okada-K.Terui: "Finite Model Property for Various Fragments of Intuitionistic Linear Logic" Journal of Symbolic Logic. (近刊). (1999)
• [文献書誌] M.Okada: "An Introduction to Linear Logic:Phase Semantics and Expressiveness" Memories of Mathematical Society of Japan. 2. 255-295 (1998)
• [文献書誌] M.Kanovitch-M.Okada-A.Scedrov: "Phase Semantics for Light Linear Logic" Theoretical Computer Science. (近刊). (1999)
• [文献書誌] M.Kanovitch-M.Okada-A.Scedrov: "Specifying Real-Time Finite Stote Systems by Linear Logic" Electronic Notes of Theoretical Computer Science. 16(1998). 1-14 (1998)
• [文献書誌] M.Hamano-M.Okada: "A Direct Independence Proof of Buchholz's Hydra Game" Archive for Mathematical Logic. 37. 67-89 (1998)
• [文献書誌] M.Takahashi-M.Okada-M.Dezani(eds.): "Theories of Types and Proofs" Mathematical Society of JAPAN(日本数学会), 297 (1998)
• [文献書誌] J.-Y.Girard-M.Okada-A.Scedrov(eds.): "Linear Logic Special Volumes I,II,of Theoretical Computer Science(近刊)" Elsevier Science Publishing, (1999)