| 研究課題/領域番号 |
10044094
|
|---|
| 研究種目 |
基盤研究(A)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 慶應義塾大学 |
|---|
研究代表者 |
岡田 光弘 慶応義塾大学, 文学部, 教授 (30224025)
|
|---|
| 研究分担者 |
萩谷 雅己 東京大学, 大学院・理学研究科, 教授 (30156252)
米澤 昭憲 東京大学, 大学院・理学研究科, 教授 (00133116)
林 晋 神戸大学, 工学部, 教授 (40156443)
大堀 淳 京都大学, 数理解析研究所, 教授 (60252532)
高橋 正子 東京工業大学, 理学部, 教授 (00015588)
|
|---|
| 研究期間 (年度) |
1998 – 1999
|
| キーワード | タイプ理論 / 線形論理 / 関数型言語 / プログラム言語理論 / 証明論 / 形式仕様 / 形式検証 / 実時間システム |
|---|
| 研究概要 |
第1年度は線形論理とタイプ理論を組み合わせた線形タイプ言語の計算モデルの理論を確立した。また第2年度は第1年度に確立した計算モデルの理論に基づいて、線形タイプ理論によるプログラミング言語の設計のための理論を構築した。
これらの研究を通じて、線形タイプ理論言語による並行計算プログラミング設計のための理論とこの言語とを用いた並行計算プログラミング方法論を考察した。また、実現可能計算量(多項式時間計算量及び多項式空間計算量)のための意味論的手法の確立、および我々の線形タイプ・プログラミング言語の設計への応用を行った。
線形論理とタイプ理論を組み合わせた線形タイプ言語に基づく線形タイプ・プログラム言語の線形理論証明システムとプログラム自動検証・自動抽出部分の設計の理論も構築した。特に今年度は米国側共同研究者たちとソフトウェアの形式仕様、形式検証のための方法論の開発を行った。また、フランスを中心とした欧州の共同研究者グループとは線形理論的手法のプログラミング方法論への応用に関する手法を共同で開発してきた。これらの成果はわれわれの言語設計に生かされている。
本研究課題で構築した新しいプログラミング言語をもとにして、フランス国立情報科学研究所(INRIA)などと協力して我々の言語の実装を計画している。
|
