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

本研究では,ソフトウエアの基礎理論に関する研究課題のうち,プログラムのモデル・論理・証明・型理論,プログラミングと証明,および並列・分散プログラミングに関する研究を行うことを目的としている。伊藤は,実行モデルに基づくプログラムの論理を構築するという立場から,実行の論理を提案した。実行の論理をもとに,並行プラセスの理論・制御の論理の試みも行っている。佐藤は,RPTと言う構成的数学体系を提案し,その数学的な性質について理論的に明らかにすると共に,Λ(ラムダ)と言う言語をRPTを基に設計し,その処理系をLISPを用いて実現した。萩谷は,例によるプログラミングと例による証明の両者を,関数方程式の形で統一的に定式化し,高階ユニフィケ-ションを用いて関数方程式を解くことにより両者を実現する研究を行い,興味深い結果を得ている。特に,型理論,項書き換え系,LFCLogical Framework)を対象に研究を進め処理系の試作も進めている。萩原は,複数プロセスでの協調的問題解決の仕方を,並列アルゴリズム法と分散アルゴリズム法に分け,それらによるアルゴリズムの解析・設計・改良のソフトウエア・ツ-ルを設計し,試作している。特に,アルゴリズムの動きを可視化するアニメ-ション・システムを開発している。なお,公募研究の林晋氏は,ATTと言う新しい構成的タイプ理論を構築し,構成的プログラミングに応用している。また,榎本肇氏は,ソフトウエア記述プロセスとしての情報構造とその操作をオブジェクト指向の形で詳細化し,手続きを得る方法について研究を行った。

本研究では,ソフトウエアの基礎理論に関する研究課題のうち,プログラムのモデル・論理・証明・型理論,プログラミングと証明,および並列・分散プログラミングに関する研究を行うことを目的としている。伊藤は,実行モデルに基づくプログラムの論理を構築するという立場から,実行の論理を提案した。実行の論理をもとに,並行プラセスの理論・制御の論理の試みも行っている。佐藤は,RPTと言う構成的数学体系を提案し,その数学的な性質について理論的に明らかにすると共に,Λ(ラムダ)と言う言語をRPTを基に設計し,その処理系をLISPを用いて実現した。萩谷は,例によるプログラミングと例による証明の両者を,関数方程式の形で統一的に定式化し,高階ユニフィケ-ションを用いて関数方程式を解くことにより両者を実現する研究を行い,興味深い結果を得ている。特に,型理論,項書き換え系,LFCLogical Framework)を対象に研究を進め処理系の試作も進めている。萩原は,複数プロセスでの協調的問題解決の仕方を,並列アルゴリズム法と分散アルゴリズム法に分け,それらによるアルゴリズムの解析・設計・改良のソフトウエア・ツ-ルを設計し,試作している。特に,アルゴリズムの動きを可視化するアニメ-ション・システムを開発している。なお,公募研究の林晋氏は,ATTと言う新しい構成的タイプ理論を構築し,構成的プログラミングに応用している。また,榎本肇氏は,ソフトウエア記述プロセスとしての情報構造とその操作をオブジェクト指向の形で詳細化し,手続きを得る方法について研究を行った。