高機能高品質ソフトウェアの基礎理論

高機能高品質ソフトウェアの基礎理論に関して,次のような研究を行った。[1]プログラムのモデルと論理に関する研究(担当:伊藤)並列プログラムにおける同時並列性を表現するための理論モデルと論理体系についての研究を行った。結合律を満す並列合成だけでなく,結合律を満さない並列合成をも有する強力な並列プロセス計算σー計算の提案を行った。また,代数的ペトリネットを提案し,プロセスとネットの関係を明らかにした。[2]プログラムの論理と証明に関する研究(担当:佐藤)構成的数学の体系RPTに基づき,構成的プログラミングを実践するための一連のシステムを計算機上に構築し,それを用いて実際に証明を構成することを試みた。[3]プログラミングと証明に関する研究(担当:萩谷)例による証明とプログラミングに関するヒュ-リスティック戦略について研究を深めた。また,構成的体系CCの証明チェッカを開発した。[4]プログラムの証明論と型理論に関する研究(担当:林)論理的仕様からの構成的プログラム抽出のための型理論ATTを改良したATTTという型理論を設計し,その理論的性質について研究を行った。[5]並列プログラミングパラダイムに関する研究(担当:萩原)並列・分散アルゴリズムのためのプログラミングパラダイムを確立する研究の一環として,並列計算モデルのアルゴリズム・アニメ-ション・システムAASをいくつかの計算モデルに対して試作し,改良も行った。また,超立方体状ネットワ-クでの置装ル-ティングに対し決定性アルゴリズムと確率アルゴリズムをシミュレ-ションにより評価した。

高機能高品質ソフトウェアの基礎理論に関して,次のような研究を行った。[1]プログラムのモデルと論理に関する研究(担当:伊藤)並列プログラムにおける同時並列性を表現するための理論モデルと論理体系についての研究を行った。結合律を満す並列合成だけでなく,結合律を満さない並列合成をも有する強力な並列プロセス計算σー計算の提案を行った。また,代数的ペトリネットを提案し,プロセスとネットの関係を明らかにした。[2]プログラムの論理と証明に関する研究(担当:佐藤)構成的数学の体系RPTに基づき,構成的プログラミングを実践するための一連のシステムを計算機上に構築し,それを用いて実際に証明を構成することを試みた。[3]プログラミングと証明に関する研究(担当:萩谷)例による証明とプログラミングに関するヒュ-リスティック戦略について研究を深めた。また,構成的体系CCの証明チェッカを開発した。[4]プログラムの証明論と型理論に関する研究(担当:林)論理的仕様からの構成的プログラム抽出のための型理論ATTを改良したATTTという型理論を設計し,その理論的性質について研究を行った。[5]並列プログラミングパラダイムに関する研究(担当:萩原)並列・分散アルゴリズムのためのプログラミングパラダイムを確立する研究の一環として,並列計算モデルのアルゴリズム・アニメ-ション・システムAASをいくつかの計算モデルに対して試作し,改良も行った。また,超立方体状ネットワ-クでの置装ル-ティングに対し決定性アルゴリズムと確率アルゴリズムをシミュレ-ションにより評価した。