| Project/Area Number |
03235102
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research on Priority Areas
|
| Allocation Type | Single-year Grants |
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
伊藤 貴康 東北大学, 工学部, 教授 (80124551)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
林 晋 龍谷大学, 理工学部, 助教授 (40156443)
萩原 兼一 大阪大学, 基礎工学部, 助教授 (00133140)
萩谷 昌己 京都大学, 数理解析研究所, 助教授 (30156252)
佐藤 雅彦 東北大学, 電気通信研究所, 教授 (20027387)
|
|---|
| Project Period (FY) |
1991
|
| Project Status |
Completed (Fiscal Year 1991)
|
| Budget Amount *help |
¥11,500,000 (Direct Cost: ¥11,500,000)
Fiscal Year 1991: ¥11,500,000 (Direct Cost: ¥11,500,000)
|
|---|
| Keywords | プログラム・モデル / 論理と証明 / 型理論ATTT / 並列プログラミング / 並列プロセス計算σー計算 / 構成的数学体系RPT / 例による証明 / アルゴリズム・アニメ-ション |
|---|
| Research Abstract |
高機能高品質ソフトウェアの基礎理論に関して,次のような研究を行った。
[1]プログラムのモデルと論理に関する研究(担当:伊藤)
並列プログラムにおける同時並列性を表現するための理論モデルと論理体系についての研究を行った。結合律を満す並列合成だけでなく,結合律を満さない並列合成をも有する強力な並列プロセス計算σー計算の提案を行った。また,代数的ペトリネットを提案し,プロセスとネットの関係を明らかにした。
[2]プログラムの論理と証明に関する研究(担当:佐藤)
構成的数学の体系RPTに基づき,構成的プログラミングを実践するための一連のシステムを計算機上に構築し,それを用いて実際に証明を構成することを試みた。
[3]プログラミングと証明に関する研究(担当:萩谷)
例による証明とプログラミングに関するヒュ-リスティック戦略について研究を深めた。また,構成的体系CCの証明チェッカを開発した。
[4]プログラムの証明論と型理論に関する研究(担当:林)
論理的仕様からの構成的プログラム抽出のための型理論ATTを改良したATTTという型理論を設計し,その理論的性質について研究を行った。
[5]並列プログラミングパラダイムに関する研究(担当:萩原)
並列・分散アルゴリズムのためのプログラミングパラダイムを確立する研究の一環として,並列計算モデルのアルゴリズム・アニメ-ション・システムAASをいくつかの計算モデルに対して試作し,改良も行った。また,超立方体状ネットワ-クでの置装ル-ティングに対し決定性アルゴリズムと確率アルゴリズムをシミュレ-ションにより評価した。
|
Report
(1 results)
Research Products
(6 results)
