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

在本研究项目中，我们对构造性逻辑系统RPT进行了设计和改进，并分析了它的性质。我们还实现了一个基于RTP的证明开发系统，通过该系统，我们可以展示构造性程序设计的范型。RPT被设计成一个构造性程序设计的基本逻辑系统；RPT的一个独特之处在于它有一个反射塔，我们可以用RPT内部表示元表达式。RPT的术语对应于某种函数式编程语言的程序，我们称之为A。我们首先给出了RPT的形式化系统，然后证明了RPT的几个证明论性质，如一致性。然后，我们在Unix工作站上实现了A的解释器和编译器。指出了对带有赋值语句的程序设计语言采用惰性求值策略时效率低下的问题。我们提出了一种程序转换技术来解决这一问题，并最终在A公司实现了一个证明开发系统，该系统为RPT的证明开发提供了支持。通过该系统，我们可以证明A程序的性质。作为一个具体的例子，我们给出了Church-Rosser定理的一个机械化证明。我们还给出了构造性程序设计的一个具体例子，即我们给出了一个程序规格说明公式的证明，并从证明中提取了一个验证程序。

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.