1991 Fiscal Year Annual Research Report

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

Research Project

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

Research Products
(6 results)

All Other

All Publications (6 results)

[Publications] Takayasu Ito(伊藤貴康): "Lisp and parallelism" Artificial Intelligence and Mathematical Theory of Computation(Academic Press). 187-206 (1991)
[Publications] Masahiko Sato(佐藤雅彦): "An Abstraction Mechanism for Symbolic Expressions" Artificial Intelligence and Mathematical Theory of Computation(Academic Press). 381-391 (1991)
[Publications] Masahiko Sato(佐藤雅彦): "Adding Proof Objects and Inductive Definition Mechanisms to Frege Structures" Lecture Notes in Computer Science (SpringerーVerlag). 526. 53-87 (1991)
[Publications] Masami Hagiya(萩谷昌己): "From programmingーbyーexample to provingーbyーexample" Lecture Notes in Computer Science (SpringerーVerlag). 526. 387-419 (1991)
[Publications] 萩原兼一: "分散協調問題解決と分散アルゴリズム" 大阪大学知識科学研究会第6回年次大会資料集. 96-111 (1991)
[Publications] Susumu Hayashi(林晋): "Singletor,Union and Intersection Types for Program Extraction" Lecture Notes in Computer Science (SpringerーVerlag). 526. 710-730 (1991)

1991 Fiscal Year Annual Research Report

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

Principal Investigator

伊藤 貴康 東北大学, 工学部, 教授 (80124551)

Research Products

[Publications] Takayasu Ito(伊藤 貴康): "Lisp and parallelism" Artificial Intelligence and Mathematical Theory of Computation(Academic Press). 187-206 (1991)

[Publications] Masahiko Sato(佐藤 雅彦): "An Abstraction Mechanism for Symbolic Expressions" Artificial Intelligence and Mathematical Theory of Computation(Academic Press). 381-391 (1991)

[Publications] Masahiko Sato(佐藤 雅彦): "Adding Proof Objects and Inductive Definition Mechanisms to Frege Structures" Lecture Notes in Computer Science (SpringerーVerlag). 526. 53-87 (1991)

[Publications] Masami Hagiya(萩谷 昌己): "From programmingーbyーexample to provingーbyーexample" Lecture Notes in Computer Science (SpringerーVerlag). 526. 387-419 (1991)

[Publications] 萩原 兼一: "分散協調問題解決と分散アルゴリズム" 大阪大学知識科学研究会第6回年次大会資料集. 96-111 (1991)

[Publications] Susumu Hayashi(林 晋): "Singletor,Union and Intersection Types for Program Extraction" Lecture Notes in Computer Science (SpringerーVerlag). 526. 710-730 (1991)

伊藤貴康東北大学, 工学部, 教授 (80124551)

[Publications] Takayasu Ito(伊藤貴康): "Lisp and parallelism" Artificial Intelligence and Mathematical Theory of Computation(Academic Press). 187-206 (1991)

[Publications] Masahiko Sato(佐藤雅彦): "An Abstraction Mechanism for Symbolic Expressions" Artificial Intelligence and Mathematical Theory of Computation(Academic Press). 381-391 (1991)

[Publications] Masahiko Sato(佐藤雅彦): "Adding Proof Objects and Inductive Definition Mechanisms to Frege Structures" Lecture Notes in Computer Science (SpringerーVerlag). 526. 53-87 (1991)

[Publications] Masami Hagiya(萩谷昌己): "From programmingーbyーexample to provingーbyーexample" Lecture Notes in Computer Science (SpringerーVerlag). 526. 387-419 (1991)

[Publications] 萩原兼一: "分散協調問題解決と分散アルゴリズム" 大阪大学知識科学研究会第6回年次大会資料集. 96-111 (1991)

[Publications] Susumu Hayashi(林晋): "Singletor,Union and Intersection Types for Program Extraction" Lecture Notes in Computer Science (SpringerーVerlag). 526. 710-730 (1991)