Design of a functional logic programming language, and development of proof, vorification and synthosis system based on it.
| Project/Area Number |
60580018
|
|---|
| Research Category |
Grant-in-Aid for General Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
Informatics
|
|---|
| Research Institution | TOHOKU UNIVERSITY (1986)
The University of Tokyo (1985) |
|---|
Principal Investigator |
SATO Masahiko Professor, Research Institn to of Electrical Communication, Tohoku University, 電気通信研究所, 教授 (20027387)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
SAKURAI Takafumi Research Associate, Department of Mathematics, Faculty of Science, Tokyo Metropo, 理学部数学科, 助手 (60183373)
NAKAHARA Hayao Research Associate, Department of Information Science, Faculty of Science, Unive, 理学部情報科学科, 助手 (80115899)
|
|---|
| Project Period (FY) |
1985 – 1986
|
| Project Status |
Completed (Fiscal Year 1986)
|
| Budget Amount *help |
¥1,500,000 (Direct Cost: ¥1,500,000)
Fiscal Year 1986: ¥700,000 (Direct Cost: ¥700,000)
Fiscal Year 1985: ¥800,000 (Direct Cost: ¥800,000)
|
|---|
| Keywords | constructive mathematics / formal semantics of programs / data type / verification of programs / Functional programming language / 論理型プログラム言語 |
|---|
| Research Abstract |
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.
|
Report
(1 results)
Research Products
(8 results)
