構成的論理と代数的仕様言語を融合した発展的ソフトウェア開発言語

1998 年度 実績報告書

• 研究課題/領域番号: 10139237
• 研究機関: 慶応義塾大学
• 研究代表者: 岡田 光弘 慶應義塾大学, 文学部, 教授 (30224025)
• キーワード: タイプ理論 / 項書き換え系 / タイプ推論 / Inductive Types / 停止性 / 並行計算 / 高階関数 / 構成論理

研究概要

昨年までに確立した融合言語の計算モデル〔これは構成論理と頭書き換え系との両停止性証明(強制規化定理証明)を融合して得られた〕に基づいて、マルチパラダイム・プログラミング方法論の開発を行った。特に、昨年度までに与えたInductive Type推論機構をさらに強めることによって、より一般的なInductive Type推論を我々の融合言語の中で供給できることとなった。また、それに合わせたrecursors等の高階関数定義の枠組の拡張がなされ、これによって高階関数の使用に関して、項書換え(代数的仕様)パラダイムとタイプ理論パラダイムを融合した新しいプログラミング方法論が導入された。
他方、項書き換えパラダイムを、伝統的な項書き換え系のかわりに、並行書き換え処理を遂行うるマルチセット書き換え系(しばしば、並行項書き換え系とも呼ばれる)を利用して拡張することにより、我々の融合言語の枠組が、並行計算プログラミングや実時間システムのプログラミングに適していることも示された。

研究成果

• [文献書誌] F.Blanqui -J.-P.Jouannaud-M.Okada: "Calculus of Inductive Constructions" Proceedings of the International Conference on Rewriting Technique and Applications. (近刊). (1999)
• [文献書誌] M.Okada-K.Terai: "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" Memoirs of Mathematical Society of Japan. 2. 255-295 (1998)
• [文献書誌] M.Karovitch-M.Okada-A.Scedrov: "Phase Semantics for Light Linear Logic" Theoretical Computer Science. 近刊. (1999)
• [文献書誌] M.Kanovitch-M.Okada-A.Scedrov: "Specifying Real-Time Finite State Systems by Linear Logic" Electronic Notes of Theoretical Computer Science. 16(1998). 1-14 (1998)
• [文献書誌] M.Okada: "Phase Semantics for Higer Order Completeness,Cut-Elimination and Normalization Proofs of Classical Linear Logic" Theoretical Computer Science. 近刊. (1999)
• [文献書誌] M.Takahashi-M.Okada-M.Pezani(tds.): "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)