Optimization in Constructive Programming

点击翻译按钮获取中文摘要

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.