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

タイプ理論と線形理論のプログラム言語理論への応用

研究課題

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

基盤研究(A)

配分区分補助金
応募区分一般
研究分野 計算機科学
研究機関慶應義塾大学

研究代表者

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

研究分担者 萩谷 雅己 (萩谷 昌己)  東京大学, 大学院・理学研究科, 教授 (30156252)
米澤 昭憲 (米澤 明憲)  東京大学, 大学院・理学研究科, 教授 (00133116)
林 晋  神戸大学, 工学部, 教授 (40156443)
大堀 淳  京都大学, 数理解析研究所, 教授 (60252532)
高橋 正子  東京工業大学, 理学部, 教授 (00015588)
研究期間 (年度) 1998 – 1999
研究課題ステータス 完了 (1999年度)
配分額 *注記
9,500千円 (直接経費: 9,500千円)
1999年度: 4,400千円 (直接経費: 4,400千円)
1998年度: 5,100千円 (直接経費: 5,100千円)
キーワードタイプ理論 / 線形論理 / 関数型言語 / プログラム言語理論 / 証明論 / 形式仕様 / 形式検証 / 実時間システム / プログラミング言語 / プログラム意味論 / 形式的プログラム検証 / 形式的仕様 / 情報科学の論理
研究概要

第1年度は線形論理とタイプ理論を組み合わせた線形タイプ言語の計算モデルの理論を確立した。また第2年度は第1年度に確立した計算モデルの理論に基づいて、線形タイプ理論によるプログラミング言語の設計のための理論を構築した。
これらの研究を通じて、線形タイプ理論言語による並行計算プログラミング設計のための理論とこの言語とを用いた並行計算プログラミング方法論を考察した。また、実現可能計算量(多項式時間計算量及び多項式空間計算量)のための意味論的手法の確立、および我々の線形タイプ・プログラミング言語の設計への応用を行った。
線形論理とタイプ理論を組み合わせた線形タイプ言語に基づく線形タイプ・プログラム言語の線形理論証明システムとプログラム自動検証・自動抽出部分の設計の理論も構築した。特に今年度は米国側共同研究者たちとソフトウェアの形式仕様、形式検証のための方法論の開発を行った。また、フランスを中心とした欧州の共同研究者グループとは線形理論的手法のプログラミング方法論への応用に関する手法を共同で開発してきた。これらの成果はわれわれの言語設計に生かされている。
本研究課題で構築した新しいプログラミング言語をもとにして、フランス国立情報科学研究所(INRIA)などと協力して我々の言語の実装を計画している。

報告書

(3件)
  • 1999 実績報告書   研究成果報告書概要
  • 1998 実績報告書
  • 研究成果

    (41件)

すべて その他

すべて 文献書誌 (41件)

  • [文献書誌] M. Okada and K. Terui: "Finite Model Property for Various Fragments of Intuitionistic Linear Logic"Journal of Symbolic Logic. 64. 790-801 (1999)

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      1999 研究成果報告書概要
  • [文献書誌] M. Okada: "A Phase-Semantic Higher Cut-elimination and Normalization Proofs of Classical Linear Logic"Theoretical Computer Science. 227. 333-396 (1999)

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      1999 研究成果報告書概要
  • [文献書誌] M. Kanovitch, M. Okada, A Scedrov: "Specifying Real-Time Finite State Systems by Linear Logic"Electronic Notes of Theoretical Computer-Science. 16, PartI. (1998)

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      1999 研究成果報告書概要
  • [文献書誌] F. Blanqui, J-P Jouannaud and M. Okada: "Inductive Data Type Systems"Theoretical Computer Science. (近刊).

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      1999 研究成果報告書概要
  • [文献書誌] F. Blanqui, J-P. Jouannaud and M. Okada: "Calculus of Inductive Construction"Proc of Rewriting Technique and Application (RTA99). Springer-Lecture Note in Computer Science. 1631. 301-316 (1999)

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      1999 研究成果報告書概要
  • [文献書誌] M. Konovitch, M. Okada and A. Scedrov: "Phase Semantics for Light Linear Logic"Theoretical Computer Science. (近刊).

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      1999 研究成果報告書概要
  • [文献書誌] M. Takahashi, M. Okada et al(eds): "Theories of Types and Proofs, second edition. Memoir of Mathematical Society of Japan vol.2"Mathematical Society of Japan. 295 (1999)

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      1999 研究成果報告書概要
  • [文献書誌] J-Y Girard, M. Okada, A. Scedrov (eds.): "Linear Logic Special Issue"Elsevier Science Publishing. (1999)

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      1999 研究成果報告書概要
  • [文献書誌] N. Hamano, M. Okada: "A Direct Independence Proof of Buchholz's Hydra Game"Archive for Mathematical Logic. 37. 67-89 (1998)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1999 研究成果報告書概要
  • [文献書誌] M. Okada: "Introduction to Linear Logic: Its Expressiveness and Phase semantics"Memoir of Mathematical Society of Japan. Vol. 2. 376-420 (1998)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1999 研究成果報告書概要
  • [文献書誌] M. Takahashi: "A primer on proofs and types"Memoir of Mathematical Society of Japan. Vol. 2. 1-42 (1998)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1999 研究成果報告書概要
  • [文献書誌] M. Kanovitch, M. Okada, A. Scedrov: "Specifying Real-Time Finite state Systems by Linear Logic"Electoronic Notes of Theoretical Computer Science ( Elsevier Science Publishing ). Vol, 16 Part I,. (1998)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1999 研究成果報告書概要
  • [文献書誌] M. Okada , K.Terui: "The imite Model Property for Various Fragments of Intuitionistic Linear Logic"Journal of Symbolic Logic. 64. 790-802 (1999)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1999 研究成果報告書概要
  • [文献書誌] M. Okada: "Phase semantic Higher Order Cur- Elimination and Normalization Proofs of ClassicalLinear Logic"Theoretical Computer Science. 227. 333-396 (1999)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1999 研究成果報告書概要
  • [文献書誌] F, Blanqui, J-P. Jouannaud, M. Okada: "Calculus of Algebraic Construction"Proc of Rewriting Technique and Application ( RTA99 ), Springer Lecture Note in Computer Science. 301-316 (1999)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1999 研究成果報告書概要
  • [文献書誌] M. Okada , P. J, Scott: "A Note on Rewriting Theory for Uniqueness of Itaration"Theory and Application of categories. Vol.6 No. 4. 47-64 (1999)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1999 研究成果報告書概要
  • [文献書誌] M. Nagayama, M. Okada: "A Graph-Theoretic Characterization Theorem for Non -Commutative Multiplicative Linear Logic"Theoretical Computer Science. (to appear). (2000)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1999 研究成果報告書概要
  • [文献書誌] M. Kanovitch, M. Okada, A. Scedrov: "Phase Semantics for Light Linear Logic"Theoretical Computer Science. (to appear). (2000)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1999 研究成果報告書概要
  • [文献書誌] F, Blanqui, J-P. Jouannaud, M. Okada: "Inductive Data Type Systems"Theoretical Computer Science. (to appear). (2000)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1999 研究成果報告書概要
  • [文献書誌] M. Nagayama, M. Okada: "A New Correctness Criterion for the Proof-Nets of Non-Commutative Multiplicative Linear Logic"Journal of Symbolic Logic. (to appear). (2000)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1999 研究成果報告書概要
  • [文献書誌] S. Hayashi: "Proof Animation"Theoretical Computer Science. (to appear). (2000)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1999 研究成果報告書概要
  • [文献書誌] M. Takahashi, M. Okada, M. Dezani: "Theories of Types and Proofs"Mathematical Society of Japan, MSJ Memoir. Vol. 2. (1998)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1999 研究成果報告書概要
  • [文献書誌] J-Y. Girard, M. Okada, A. Scedrov: "Special Issue on Linear Logic ( I )"Theoretical Computer Science. 227. (1999)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1999 研究成果報告書概要
  • [文献書誌] M. Takahashi, M. Okada, M. Dezani: "Special Issue on Theories of Types and Proofs"Theoretical Computer Science. (to appear). (2000)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1999 研究成果報告書概要
  • [文献書誌] J-Y. Girard, M. Okada, A. Scedrov: "Special Issue on Linear Logic ( II )"Theoretical Computer Science. (to appear). (2000)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1999 研究成果報告書概要
  • [文献書誌] M.Okada and K.Terui: "Finite Model Property for Various Fragments of Intuitionistic Linear Logic"Journal of Symbolic Logic. 64. 790-801 (1999)

    • 関連する報告書
      1999 実績報告書
  • [文献書誌] M.Okada: "A Phase-Semantic Higher Cut-elimination and Normalization Proofs of Classical Linear Logic"Theoretical Computer Science. 227. 333-396 (1999)

    • 関連する報告書
      1999 実績報告書
  • [文献書誌] M.Okada and P.J.Scott: "A Note on Rewriting Theory for Uniquenss of Iteration"Journal of Theory ahd Applications of Categories. 6. 47-64 (1999)

    • 関連する報告書
      1999 実績報告書
  • [文献書誌] F.Blanqui,J-P.Jouannaud and M.Okada: "Inductive data Type Systems:"Theoretical Computer Science. (近刊).

    • 関連する報告書
      1999 実績報告書
  • [文献書誌] F.Blanqui,J-P.Jouannaud and M.Okada: "Calculus of Inductive Construction"Proc.Of Rewriting Technique and Application(RTA99),Springer-Lecture Note in Computer Science. 1631. 301-316 (1999)

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

    • 関連する報告書
      1999 実績報告書
  • [文献書誌] M.Okada: "Theories of Types and Proofs,second edition,Memoir of Mathematical society of Japan vol.2"Mathematical Society of Japan. (1999)

    • 関連する報告書
      1999 実績報告書
  • [文献書誌] 岡田 光弘: "法律人工知能(共著)"創成社出版. (2000)

    • 関連する報告書
      1999 実績報告書
  • [文献書誌] M.Okada: "Phase Semantics for Higher order Completeness,cut Elimination and Normalization proofs" Theoretical Computer Science. (近刊). (1999)

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

    • 関連する報告書
      1998 実績報告書
  • [文献書誌] M.Okada-M.Kanovitch-A.Scedrov: "Specifying Real-Time Finite State Systems by Linear Logic" Electronic Notes of Theoretical Computer Science. 16. 1-14 (1988)

    • 関連する報告書
      1998 実績報告書
  • [文献書誌] M.Takahashi: "Introduction to Types and Proofs" Memoir of Math.Soc.of Japan. 2. 1-30 (1998)

    • 関連する報告書
      1998 実績報告書
  • [文献書誌] S.Hayashi: "Animating Proof systems" Theoretical Computer Science. (近刊). (1999)

    • 関連する報告書
      1998 実績報告書
  • [文献書誌] M.Sato: "Intuitionistic and Classical Natural Deduction Systems with Catch and Throw Rules" Theoretical Computer Science. (近刊). (1999)

    • 関連する報告書
      1998 実績報告書
  • [文献書誌] M.Takahashi-M.Okada: "Theories of Types and Proofs" Mathematical Society of Japan, 420 (1998)

    • 関連する報告書
      1998 実績報告書
  • [文献書誌] J.-Y.Girard-M.OKADA-A.Scedrov: "Special Volume on Linear Logic,Theoretical computer science(予定)" Elsevier Science Publishing, 462 (1999)

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

URL: 

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

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

Powered by NII kakenhi