Design and Implementation of Constructive Programming Systems

在这个为期两年的研究项目中，我们设计并实现了一个原型软件系统，以帮助建设性的编程。我们还通过使用它的编程示例对系统进行了评估。1996年，(1)我们实现了函数式编程语言LAMBDA的解释器，它是本领域所有软件系统的基础，(2)我们实现了一个用于直觉一阶谓词演算的交互式定理证明系统。基于这些结果，在1997年，(3)我们实现了一个用于各种逻辑系统的交互式定理证明系统，如模态逻辑的许多变体；(4)我们实现了一个用于经典逻辑的构造性规划系统。(2)：我们基于X窗口系统实现了一个具有复杂图形用户界面的交互式定理证明系统。我们的一部分实现是用编程语言JAVA编写的，我们的设计旨在通过模块进行分布式编程（分布式证明）。(3)：我们…More扩展了系统(2)，使目标逻辑系统不必是直觉的一阶逻辑。我们的实现包括模态逻辑的许多变体，如T、S4、S5、B等。该系统可以看作是一个独立于特定逻辑的证明策略系统。(4)：从经典证明中提取算法内容是构造规划中一个相当新的课题。我们设计和实现了两种不同的方式，一种使用catch/throw机制，另一种使用一等延续。然后，我们从经典证明中提取算法。使用(2)-(4)中的系统，我们编写了许多编程（证明）示例。通常可以观察到，当一个程序的规范是严格编写的时候，所指定的程序是很顺利地合成的。因此，我们已经表明，建设性编程可以适用于比以前更广泛的目标，并且我们的系统可以成为在实际工业中构建建设性编程系统的第一步。少

In this two-year research project, we designed and implemented a prototypical software system which assists constructive programming. We also evaluated the system by making programming examples using it. In 1996, (1) we implemented an interpreter of a functional programming langauge LAMBDA which is a basis for all the software systems in this profect, and (2) we implemented an interactive theorem proving system for an intuitionistic first-order predicate calculus. Based on these results, in 1997, (3) we implemented an interactive theorem proving system for various logical systems such as many variants of modal logics, and (4) we implemented a constructive programming system for a classical logic.(2) : We implemented an interactive theorem proving system with a sophisticated graphical user interface based on X window system. A part of our implementation is written in the programming language JAVA,and our design aimed at distributed programming (distributed proving) by modules. (3) : We … More extended the system (2) so that the target logical system need not be an intuitionistic first-order logic. Our implementation includes many variants of modal logics such as T,S4, S5, B and so on. The system can be regarded as a system towards a proving strategy independent of specific logics. (4) : Extracting algorithmic contents from classical proofs is a quite recent topic in constructive programming. We designed and implemented two different ways, one uses the catch/throw mechanism, and the other uses the first-class continuation. We then extracted algorithms from classical proofs.Using the systems in (2)-(4), we wrote many programming (proving) examples. It is generally observed that, when specification of a program is rigidly written, the specified program is synthesized quite smoothly. As a result, we have shown that constructive programming can be applicable to much wider targets than befor, and our systems can be a first step towards a constructive programming system in the real industry. Less