Design and Implementation of Constructive Programming Systems

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

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