Design of a functional logic programming language, and development of proof, vorification and synthosis system based on it.

研究的目的是提供一个环境，在其中可以统一对待的规格说明的程序，证明的规格，验证和综合的程序。为此，我们设计了一个基于直觉逻辑的构造性逻辑系统QJ和一个作为QJ子系统的函数逻辑程序设计语言Quty。1.它有逻辑符号<not><and>、<or>和<exist>作为其基本元素。这些逻辑符号的意义与直觉逻辑中相应符号的意义相一致。因此，可以编写逻辑上自然的程序。2.它具有丰富的数据类型，包括函数类型。因此，可以编写处理这些更高类型数据的函数程序。3.程序是并行执行的。基于共享变量和流的并行程序设计是可能的。QJ是一个有类型的构造性逻辑系统。QJ被设计成使得QJ的项恰好是Quty的程序。因此，可以在QJ中指定程序，证明规范和验证程序。我们还证明了Quty的操作语义在QJ中的一致性。这意味着Quty的计算对应于QJ的证明，Quty程序中使用的逻辑符号具有自然的逻辑意义。虽然我们只能对系统的实现做一些小的实验，但我们肯定得到了很好的理论结果，这将为实现奠定基础。

The aim of the research was to provide an environment in which one can uniformly treat description of the specification of a program, proof of the specification, verification and synthesis of programs. To this end, we designed a constructive logical system QJ which is based on intuitionistic logic and a functional logic programming language Quty which is a subsystem of QJ.The programming language Quty has the following characteristics. 1. It has the logical symbols <not> , <and> , <or> and <exist> as its basic elements. The meanings of these logical symbols coincide with those of corresponding symbols in intuitionistic logic. It is therefore possible to write logically natural programs. 2. It has rich data types including function types. It is therefore possible to write functional programs which treat these higher type data. 3. Programs are executed in parallel. Parallel programming based on shared variables and streams are possible.QJ is a constructive logical system with types. QJ is designed so that the terms of QJ are exactly the programs of Quty. It is therefore possible to specify programs, prove the specification and verify programs in QJ. We also proved the consistency of the operational semantics of Quty within QJ. This means that a computation in Quty corresponds to a proof in QJ and that the logical symbols used in Quty programs have the natural logical meanings.Although we could only do a small experiments with regard to the implementation of the system, we certainly obtained good theoretical results which would form a basis for the implementation.