1997 Fiscal Year Final Research Report Summary
Optimization in Constructive Programming
| Project/Area Number |
08680367
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Kobe University |
|---|
Principal Investigator |
HAYASHI Susumu Kobe University, Department of Computer and Systems Engineering, Professor, 工学部, 教授 (40156443)
|
|---|
| Project Period (FY) |
1996 – 1997
|
| Keywords | Program verification / Program synthesis / Formal methods |
|---|
| Research Abstract |
The original plan to apply Beradi method to PX system turned to be difficult. Thus we changed the plan. We redesigned PX system so that it has types and so the extracted programs are simply typed. We rebuilt the system throughly even from the basic logical system. The new logical system was called S,and the new implementation is called Proof Works.
The results turned out even better than the original plan, because the system was redone utilizing many new knowledges which were not available at the time PX system was designed and built.
On the course of research, Hayashi got a novel insight on application of constructive programming called "Proof Animation." This new insight, which is a spin-off of the present research, is not only more important than the original aim of the research. It is expected to grow one of central issues of the area in the feature.
One thing we could not achive is that extensive experiments with the system. This is due to the delay caused by the new design and implementation of the entire system. We are continueing it even after the project is officially finished.
|
