| 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
|
| Project Status |
Completed (Fiscal Year 1992)
|
| Budget Amount *help |
¥11,500,000 (Direct Cost: ¥11,500,000)
Fiscal Year 1992: ¥3,500,000 (Direct Cost: ¥3,500,000)
Fiscal Year 1991: ¥3,700,000 (Direct Cost: ¥3,700,000)
Fiscal Year 1990: ¥4,300,000 (Direct Cost: ¥4,300,000)
|
|---|
| 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.
|
