| 研究課題/領域番号 |
09245102
|
|---|
| 研究種目 |
重点領域研究
|
| 配分区分 | 補助金 |
|---|
| 研究機関 | 東北大学 |
|---|
研究代表者 |
伊藤 貴康 東北大学, 大学院・情報科学研究科, 教授 (80124551)
|
|---|
| 研究分担者 |
井田 哲雄 筑波大学, 電子情報工学系, 教授 (70100047)
米崎 直樹 東京工業大学, 大学院・情報理工学研究科, 教授 (00126286)
萩谷 昌己 東京大学, 大学院・理学研究科, 教授 (30156252)
外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
坂部 俊樹 名古屋大学, 大学院・工学研究科, 教授 (60111829)
|
|---|
| 研究期間 (年度) |
1997 – 1999
|
| キーワード | 発展的プログラミング機構 / 健全並列化 / 検証 / リアクティブシステム / 時相論理 / 関数論理型プログラミング / 項書き換え系 / 線形論理 |
|---|
| 研究概要 |
1.発展的プログラミング機構の研究(担当:伊藤):逐次プログラムを並列環境に発展的に進化させるときに問題となる健全並列化メカニズムの理論的基礎を並列関数型プログラミングを対象として与え、試作システムにより実証した。
2.検証系の検証と検証情報の発展(担当:萩谷):モデル検査系などの検証系の検証を高階論理に基づいて行った。また、検証情報を発展させるため述語の帰納的定義を発展させる方法を提案し実現した。
3.実時間環境のための発展的ソフトウェアの理論(担当:米崎):リアクテイブシステムの仕様の時相論理による実現可能性の判定法とその正しさの証明を与え、更に、この方法に基づく検証システムを作成した。
4.実行可能仕様理論のための関数論理型プログラムの計算モデル(担当:井田):遅延ナローイング計算系の理論的性質を解析し、これに基づく関数論理型プログラミングシステムを分散環境の下に作成した。
5.適応的書き換え系とその理論(担当:坂部):書き換え規則や項書換え系をFirst Class Objectとして扱える書換え型の計算モデルを与え、その理論的性質を解析した。
6.発展的プログラミングを書き換えシステムの諸性質(担当:外山):書き換えシステムによって発展過程を形式化したときに問題となる書き換えシステムの分解・合成、停止性判定について新しい定理を得た。
その他、線形論理の拡張について、時間概念の導入(伊藤)、場所と時間を表す様相の導入(東京大学:小林直樹)、書き換え系との融合による実時間システムの記述と検証への応用(慶應義塾大学:岡田光弘)、線形論理型言語の高速コンパイラ(神戸大学:田村直之)などに関する研究が行われた。また、デッドロックフリーダムを保証する型システム(小林直樹)、環境を明示的に導入した型付き環境計算体系(東京工業大学:西崎真也)、簡明なパッケージの設計と実現(伊藤)などについての研究も行われた。
|
