1992 Fiscal Year Final Research Report Summary
Co-operative research on foundational theories of programs
| Project/Area Number |
02302009
|
|---|
| Research Category |
Grant-in-Aid for Co-operative Research (A)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
General mathematics (including Probability theory/Statistical mathematics)
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
SATO Masahiko Tohoku University,Research Institute of Electrical Communications,Professor, 電気通信研究所, 教授 (20027387)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
KAMEYAMA Yukiyoshi Tohoku University,Research Institute of Electrical Communications,Research assoc, 電気通信研究所, 助手 (10195000)
TATSUTA Makoto Tohoku University,Research Institute of Electrical Communications,Research assoc, 電気通信研究所, 助手 (80216994)
|
|---|
| Project Period (FY) |
1990 – 1992
|
| Keywords | Theory of programs / Constructive logic / Type theory / Graph theory |
|---|
| Research Abstract |
We have studied (1) mathematical foundations,(2) applied mathematics and (3) programming. We have constructed foundational theories of programming,researched methods of software development based on the theories and developed actual application software. By studying variety of foundational theories of programming and discussing relationship among these theories, We have deepened knowledge about these theories. Particularly the research have got the following results.
Sato constructed a logical system RPT, which has proofs as internal objects and gave foundations of theory of programs. Tatsuta studied realizability interpretations of inductive definitions for constructive programming. Kameyama implemented a constructive programming system and studied computer network, which gives infrastructures of the research. Ito studied structured models of concurrent processes and term rewriting systems and implemented software based on the results as an experiment. Hayashi presented a new framework of type theories by singleton, union and intersection types and showed that it is more expressive for constructive programming than other frameworks. Hagiya studied basic techniques to implement computer environment for describing formal proofs, such as user interfaces of a proof checker which include proofs by examples and visualization of proofs. Ono studied semantics of logics without structural rules, decision problems and finite model properties. Noshita developed fast search techniques for game trees and applied it to software which solves Tsume-shogi. Ushijima studied foundational theories and actual implementation of testing and debugging methods of concurrent programs.
|
