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