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

1996 年度 研究成果報告書概要

• 研究課題/領域番号: 07044093
• 研究種目: 国際学術研究
• 配分区分: 補助金
• 応募区分: 共同研究
• 研究機関: 慶応義塾大学
• 研究代表者: 岡田 光弘 慶応義塾大学, 文学部, 教授 (30224025)
• 研究分担者: 林 晋 神戸大学, 工学部, 教授 (40156443) ; 高橋 正子 東京工業大学, 理学部, 助教授 (00015588) ; 大堀 淳 京都大学, 数理解析研究所, 助教授 (60252532) ; 萩谷 昌巳 東京大学, 理学部, 教授 (30156252) ; 佐藤 雅彦 京都大学, 工学部, 教授 (20027387) ; PARIGOT Michel Universite Paris VII ; HUET Gerard INRIA,France ; JOUANNAUD Jean-Pierre Universite Paris XI,L.R.I. ; CURIEN Pierre-Luis Ecole Normale Superiuer-Paris ; GIRARD Jan-Yves CNRS Mathematics Instutute-Marseille
• 研究期間 (年度): 1995 – 1996
• キーワード: タイプ理論 / 線形論理 / 構成的証明 / プログラミング言語 / プログラム検証 / プログラム意味論 / 平行計算 / 直観主義論理 / Proof Theory

研究概要

現在、理論学界及び理論情報科学会において最も注目を集めている分野の一つであるタイプ理論及び線形論理を基にして新しいプログラミング言語理論を確立し、次世代高度知的プログラミング言語を設計することを目標とした。
本分野の国際学界において最も活発に研究を進めているフランス側及び日本側の指導的立場にある研究者達がチームを組み、本共同研究プロジェクトを実現させた。
これまでにもタイプ理論はプログラムの構成的開発、プログラムの形式的検証、プログラムの自動抽出(形式的仕様からの自動抽出)等の観点から注目されてきており、そのプログラミング言語への応用が期待されてきた。又、一方線形論理は、計算資源の消費関係や並行計算概念や計算状態の推移概念等が顕在的に表現できるまったく新しい論理体系としてその情報科学への応用が大いに期待されてきた。
我々共同研究チームの目的は、この両者を組み合わせて、これまでにないまったく新しい知的関数型プログラミング言語を構成することにある。特に本課題研究においては、この両者を組み合わせたプログラミング言語実現のための基礎理論の構築を目指した。
そのために、線形論理とタイプ理論を組み合わせて線形タイプ言語を構成し、その意味論(未来的意味論)、計算モデルの理論を完成させた。又、これら意味論・計算モデル理論に基づいて平行計算プログラミング、プログラム自動検証・自動抽出、構成的プログラム開発等がどのように実現できるかを研究した。
これまでのタイプ理論言語は伝統的な直観主義論理体系に基づいて作られていたが、これを線形論理体系で入れ換えて線形タイプ理論言語が構成されたため、線形論理の特徴である計算資源の消費関係を並行計算概念や計算状態概念などの種々のプログラミング・コントロールに必要な概念が表示可能なタイプ理論的関数型プログラム言語の実現可能性が立証された。

研究成果

• [文献書誌] J-P.Jouannaud 岡田光弘: "Abstract Data Type Systems" Theoretical Computer Science. (近刊). 43- (1997)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] 岡田光弘(研究協力者 浜野正浩との共著): "A Direct Independence Proof of Buchholz's Hydra Game on Labeled Finite Trees" Archive for Mathematical Logic. (近刊). (1997)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] 岡田光弘(研究協力者 浜野正浩との共著): "A Relationship Among Gentzen's Proof Reduction,Rirby-Paris Hydra Game and Buchholz's Hydra Game" Mathematical Logic Quarterly. 43. 103-120 (1997)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] 高橋正子: "Parallel reduction in λ-calculus" Information and Computation. 118. 120-127 (1995)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] 林晋: "TWO Extensions of PX Systems" Electronic Notes of Theoretical Computer Science. 3. 13 (1996)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] Jean-Yues Girard: "Coherent Barach Space" Electronic Notes of Theoretical Computer Science. 3. 13 (1996)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] J-Y,Girard 岡田光弘 Andre Soedrov(共編): "Linear Logic (A special issue of Theoretical Computer Science)" Elsevier(オランダ)(近刊), 190 (1997)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] 岡田光弘: "情報科学のための論理学" 産業図書(近刊), 273 (1997)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] 大堀淳: "プログラム言語の基礎理論" 共立出版, 272 (1997)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] 林晋: "プログラミング検証理論" 共立出版, 211 (1995)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] J-Y,Girard(研究協力者Y,Lafonts L.Regnierとの共著): "Advances in Linear Logic" Cambridge University Press, 389 (1996)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] J-Y,Girard 岡田光弘 Andre Scedrov(共編): "Linear Logic,A special issue of Electronic Notes of Theoretical computer Science" Elsevier-EATCS(オランダ)(欧州理論情報学会), 256 (1996)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] Jean-Pierre Jouannaud and Mitsuhiro Okada: "Abstract Data Type Systems" Theoretical Computer Science. (to appear). 43 (1997)
  • 説明: 「研究成果報告書概要(欧文)」より
• [文献書誌] Mitsuhiro Okada (with Masahitro Hamano): "A Relationship Among Gentzen's Proof Reduction, Kirby-Paris Hydra Game and Buchholz's Hydra Game" 43. 103-120 (1997)
  • 説明: 「研究成果報告書概要(欧文)」より
• [文献書誌] Mitsuhiro Okada (with Masahiro Hamano): "A Direct Independence Proof of Buchholz's Hydra Game for Labeled Finite Trees" Archive for Mathematical Logic. (to appear). (1997)
  • 説明: 「研究成果報告書概要(欧文)」より
• [文献書誌] Susumu HAYASHI et al.: "Two Extensions of PX Systems" Electronic Notes of Theoretical Computer Science. 3. 12 (1996)
  • 説明: 「研究成果報告書概要(欧文)」より
• [文献書誌] Jean-Yves Girard: "Coherent Banach Space" Electronic Notes of Theoretical Computer Science. 3. 13 (1996)
  • 説明: 「研究成果報告書概要(欧文)」より
• [文献書誌] Masako Tokahashi: "Parallel reduction in lambda calculus" Information and Computation. 118. 120-127 (1995)
  • 説明: 「研究成果報告書概要(欧文)」より
• [文献書誌] Jean-Yves Girard-Mitsuhiro Okada-Andre Scedrov: Elsevier Science Publishing, The Netherlands (to appear). Linear Logic Special Issue, THeoretical Computer Science, 190 (1997)
  • 説明: 「研究成果報告書概要(欧文)」より
• [文献書誌] Mitsuhiro Okada: Sangyo Tosto Publishing, Tokyo (to appear). Logic for Computer Science (in Japanese), 273 (1997)
  • 説明: 「研究成果報告書概要(欧文)」より
• [文献書誌] Atsushi Ohori: Kyoritsu Tokyo, Tokyo. The Foundations of Programming Language Theory (in Japanese)., 272 (1997)
  • 説明: 「研究成果報告書概要(欧文)」より
• [文献書誌] Susumu Hayashi: Kyoritsu Tosyo, Tokyo. Theory of Program Verification (in Japanese), 211 (1995)
  • 説明: 「研究成果報告書概要(欧文)」より
• [文献書誌] Jean-Yves Girard (with Yves Lafont and L.Regnier): Cambridge University Press. Advances in Linear Logic, 389 (1996)
  • 説明: 「研究成果報告書概要(欧文)」より
• [文献書誌] Jean-Yves Girard-Mitsuhiro Okada-Andre Scedrov: Elsevier and EATCS (European Association for Theoretical Computer SCience).Linear Logic, A Special Issue of Electronic Notes of Theoretical Computer Science, 256 (1996)
  • 説明: 「研究成果報告書概要(欧文)」より