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

1998 Fiscal Year Annual Research Report

• Project/Area Number: 10139237
• Research Institution: Keio University
• Principal Investigator: 岡田 光弘 慶應義塾大学, 文学部, 教授 (30224025)
• Keywords: タイプ理論 / 項書き換え系 / タイプ推論 / Inductive Types / 停止性 / 並行計算 / 高階関数 / 構成論理

Research Abstract

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

Research Products

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