Grant-in-Aid for Scientific Research on Priority Areas (A).
|Research Institution||Tohoku University|
ITO Takayasu Tohoku University, Graduate School of Information Sciences, Professor, 大学院・情報科学研究科, 教授 (80124551)
HAGIYA Masami University of Tokyo, Graduate School of Sciences, Professor, 大学院・理学研究科, 教授 (30156252)
YONEZAKI Naoki Tokyo Institute of Technology, Graduate School of Mathematical and Computer Sciences, Professor, 大学院・情報理工学研究科, 教授 (00126286)
SAKABE Toshiki Nagoya University, Graduate School of Engineering, Professor, 大学院・工学研究科, 教授 (60111829)
IDA Tetsuo University of Tsukuba, Institute of Information Sciences and Electronics, Professor, 電子情報工学系, 教授 (70100047)
TOYAMA Yoshihito Tohoku University, Research Institute of Electrical Communication, Professor, 電気通信研究所, 教授 (00251968)
|Project Fiscal Year
1997 – 1999
Completed(Fiscal Year 1999)
|Budget Amount *help
¥41,000,000 (Direct Cost : ¥41,000,000)
Fiscal Year 1999 : ¥22,000,000 (Direct Cost : ¥22,000,000)
Fiscal Year 1998 : ¥10,000,000 (Direct Cost : ¥10,000,000)
Fiscal Year 1997 : ¥9,000,000 (Direct Cost : ¥9,000,000)
|Keywords||evolutionary programming mechanism / sound parallelization / verification / reactive system / temporal logic / functional logic programming / term rewriting system / linear logic / 発展的プログラミング機構 / 健全並列化 / 検証 / リアクティブシステム / 時相論理 / 関数論理型プログラミング / 項書き換え系 / 線形論理 / 発展的ソフトウェア / ソフトウェア仕様記述 / 論理・関数型プログラミング / 書換え型メタ計算モデル / 実時間論理 / 検証系 / 検証情報 / 発展的計算モデル / 適応的発展機構|
Computational environments are evolving from "sequential" into "parallel and/or distributed", and applications are evolving into the ones that require finer demands and requirements in efficiency, time, specification and verification, etc.
With this background models of evolvable computer software and their theoretical aspects were studied in this project.
A sound parallelization framework of transforming a sequential program into a parallel program that the resultant parallel program runs faster than the original sequential one was given for functional programs by T. Ito.
Verification and specification of distributed programs that evolve under internet environments are of important issues. M. Hagiya proposed an interesting idea of verification of verification methods and how to evolve verification conditions.
N. Yonezaki studied bow to specify and verify real-time reactive systems, using temporal logics and linear logic, and he gave various basic formal properties on temporal structures.
T. Ida studied some basic properties of functional logic programs with applications to executable specifications, and he implemented a functional logic programming system under a distributed system.
Term rewriting systems (TRS) provide fine-grained operational mechanisms for executions of various structures, including evolvable programs and mechanisms.
T. Sakabe gave a model of adaptive TRSs. Y. Toyama gave an analysis and synthesis method of TRSs, and a powerful procedure of proving termination of TRSs.
Also, a number of interesting works on linear logic and its extensions were done, including 1) a proposal of introducing temporal linear logic (T. Ito), 2) a linear logic language with locality and temporality (K. Kobayashi), 3) a proposal of combining linear logic and concurrent TRSs for specification and verification of real-time systems (M. Okada), 4) an efficient compiler of linear logic programming language (N. Tamura). In addition, K. Kobayashi proposed a type system of distributed systems that guarantees deadlock-freedom, and S. Nishizaki proposed an environment calculus which is an extension of ML to incorporate environments into ML. Less