• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

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

Research Project

Project/Area Number 60580018
Research Category

Grant-in-Aid for General Scientific Research (C)

Allocation TypeSingle-year Grants
Research Field Informatics
Research InstitutionTOHOKU 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)
Keywordsconstructive 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)
  • 1986 Final Research Report Summary

Research Products

(8 results)

All Other

All Publications (8 results)

  • [Publications] 佐藤雅彦: Publ.RIMS,Kyoto Univ.21. 455-540 (1985)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1986 Final Research Report Summary
  • [Publications] 佐藤雅彦: Technical Report,Dept.of Info Science,Univ.Tokyo. 85-13. 1-37 (1985)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1986 Final Research Report Summary
  • [Publications] 佐藤雅彦: France,Japan Artificial Intelligence and Computer Science Symposium86. 159-174 (1986)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1986 Final Research Report Summary
  • [Publications] 佐藤雅彦,桜井貴文: Logic Programming. 131-154 (1986)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1986 Final Research Report Summary
  • [Publications] Masahiko Sato: "Theory of Symbolic Expressions <II> " Publ. RIMS, Kyoto University. 21. 455-540 (1985)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1986 Final Research Report Summary
  • [Publications] Masahiko Sato: "Typed Logical Calculus" Technical Report, Dept. of Into. Science, University of Tokyo. 85-13. 1-37 (1985)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1986 Final Research Report Summary
  • [Publications] Masahiko Sato: "QJ : A Constructive Logical System with Tyges" France-Japan Artificial Intolligence and Computer Science Symposium, 86. 159-174 (1986)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1986 Final Research Report Summary
  • [Publications] Masahiko Sato and Takafumi Sakurai: "Qute : A Functional Langnage Bared on Unification" Logic Programming. 131-154 (1986)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1986 Final Research Report Summary

URL: 

Published: 1987-03-30   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi