| Project/Area Number |
06452387
|
|---|
| Research Category |
Grant-in-Aid for General Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | KYOTO UNIVERSITY (1995)
Tohoku University (1994) |
|---|
Principal Investigator |
SATO Masahiko Kyoto Univ., Graduate School of Engineering Professor, 工学研究科, 教授 (20027387)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
KAMEYAMA Yukiyoshi Kyoto Univ., Graduate School of Engineering Research Associate, 工学研究科, 助手 (10195000)
TATSUTA Makoto Tohoku Univ., Res.Inst.of Elec.Comm, Associate Professor, 電気通信研究所, 助教授 (80216994)
|
|---|
| Project Period (FY) |
1994 – 1995
|
| Project Status |
Completed (Fiscal Year 1995)
|
| Budget Amount *help |
¥7,200,000 (Direct Cost: ¥7,200,000)
Fiscal Year 1995: ¥2,500,000 (Direct Cost: ¥2,500,000)
Fiscal Year 1994: ¥4,700,000 (Direct Cost: ¥4,700,000)
|
|---|
| Keywords | Constructive Programming / Constructive Logic / Proof Development System / Functional Programming / Assignment Statement / Lazy evaluation / 関数型プロゲーム言語 / 直観主義論理 / プログラム検証 / プログラム合成 |
|---|
| Research Abstract |
In this research project, we designed and improved the constructive logical system RPT and analyzed its properties. We also implemented a proof-development system based on RTP.By using this system, we can demonstrate the paradigm of Constructive Programming.
RPT was designed to be a basic logical system for constructive programming ; a unique feature of RPT is that it has a reflective tower ; we can internally express meta-expressions in RPT.The terms of RPT correspond to programs of a certain functional programming language, which we call A.
We first gave a formal system of RPT,and then proved several proof-theoretic properties of RPT such as consistency. We then implemented an interpreter and a compiler of A on top of UNIX workstations. We pointed out the problem of inefficiency when we adopt lazy-evaluation strategy for programming languages with assignment statements. We proposed a program transformation technique which fixes this problem.
We finally implemented by A a proof-development system which provides supports for developmoent of proofs of RPT.By using this system, we can prove properties of A programs. As a substantial example, we presented a mechanized proof of Church-Rosser theorem. We also presented a concrete example of Constructive Programming ; namely, we developed a proof of a specification formula of a certain program, and the extracted a verified program from the proof.
|
