• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

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

Research Project

Project/Area Number 03235102
Research Category

Grant-in-Aid for Scientific Research on Priority Areas

Allocation TypeSingle-year Grants
Research InstitutionTohoku 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)
  • 1991 Annual Research Report
  • 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)

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

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

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

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

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

    • Related Report
      1991 Annual Research Report

URL: 

Published: 1991-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi