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

1998 Fiscal Year Annual Research Report

• Project/Area Number: 09480058
• Research Institution: Keio University
• Principal Investigator: 岡田 光弘 慶應義塾大学, 文学部, 教授 (30224025)
• Keywords: 線形論理 / 相意味論 / 証明の正規化定理 / (強)停止性 / 計算モデル / 高階論理 / 並行計算 / カット消去定理

Research Abstract

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

Research Products

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