Constructive Programming System for Proof Development, Verification, and Program Synthesis

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

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.