• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 前のページに戻る

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

研究課題

研究課題/領域番号 10139237
研究種目

特定領域研究(A)

配分区分補助金
研究機関慶応義塾大学

研究代表者

岡田 光弘  慶應義塾大学, 文学部, 教授 (30224025)

研究期間 (年度) 1998
研究課題ステータス 完了 (1998年度)
配分額 *注記
1,400千円 (直接経費: 1,400千円)
1998年度: 1,400千円 (直接経費: 1,400千円)
キーワードタイプ理論 / 項書き換え系 / タイプ推論 / Inductive Types / 停止性 / 並行計算 / 高階関数 / 構成論理
研究概要

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

報告書

(1件)
  • 1998 実績報告書
  • 研究成果

    (8件)

すべて その他

すべて 文献書誌 (8件)

  • [文献書誌] F.Blanqui -J.-P.Jouannaud-M.Okada: "Calculus of Inductive Constructions" Proceedings of the International Conference on Rewriting Technique and Applications. (近刊). (1999)

    • 関連する報告書
      1998 実績報告書
  • [文献書誌] M.Okada-K.Terai: "Finite Model Property for Various Fragments of Intuitionistic Linear Logic" Journal of Symbolic Logic. (近刊). (1999)

    • 関連する報告書
      1998 実績報告書
  • [文献書誌] M.Okada: "An Introduction to Linear Logic : Phase Semantics and Expressiveness" Memoirs of Mathematical Society of Japan. 2. 255-295 (1998)

    • 関連する報告書
      1998 実績報告書
  • [文献書誌] M.Karovitch-M.Okada-A.Scedrov: "Phase Semantics for Light Linear Logic" Theoretical Computer Science. 近刊. (1999)

    • 関連する報告書
      1998 実績報告書
  • [文献書誌] 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)

    • 関連する報告書
      1998 実績報告書
  • [文献書誌] M.Okada: "Phase Semantics for Higer Order Completeness,Cut-Elimination and Normalization Proofs of Classical Linear Logic" Theoretical Computer Science. 近刊. (1999)

    • 関連する報告書
      1998 実績報告書
  • [文献書誌] M.Takahashi-M.Okada-M.Pezani(tds.): "Theories of Types and Proofs" Mathematical Society of JAPAN(日本数学会), 297 (1998)

    • 関連する報告書
      1998 実績報告書
  • [文献書誌] J.-Y.Girard-M.Okada-A.Scedrov(eds.): "Linear Logic Special Volumes I,II of Theoretical Computer Science(近刊)" Elsevier Science Publishing, (1999)

    • 関連する報告書
      1998 実績報告書

URL: 

公開日: 1998-04-01   更新日: 2016-04-21  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi