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

1989 Fiscal Year Final Research Report Summary

Design of Proving, Verifying, and Synthesizing System based on Constructive

Research Project

Project/Area Number 62460220
Research Category

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

Allocation TypeSingle-year Grants
Research Field Informatics
Research InstitutionTohoku University

Principal Investigator

SATO Masahiko  Res. Inst. of Elec. Comm., Professor, 電気通信研究所, 教授 (20027387)

Co-Investigator(Kenkyū-buntansha) KAMEYAMA Yukiyoshi  Res. Inst. of Elec. Comm., Research Associate, 電気通信研究所, 助手 (10195000)
Project Period (FY) 1987 – 1989
KeywordsConstructive Mathematics / Functional Programming Language / Intuitionistic Logic / Proof / Program Verification / Program Synthesis
Research Abstract

This project has investigated the key-idea constructive programming very thoroughly. Constructive programming is a new paradigm in programming methodology, which takes constructive logical system as an underlying theory and provides a rigid and uniform basis for verifying programs, proving mathematical theorems, and synthesizing programs from its logical specifications.
Our main results are summarized as follows:
1. We designed a well-organized constructive logical system SST. SST is symbolic in the sense that all terms and formulas can be treated mechanically, and therefore, by computers.
SST is a suitable logic for writing specifications (datatypes as sets), and for reasoning about properties of programs, since SST is a first order predicate logic for partial terms.
2. We established the theoretical results. We first made a model of SST to show SST is consistent. This model reflects our intended domain of S-expressions. We proved the representation theorem for general recursive functions … More in SST. We then defined the formalized realizability interpretation of SST. This interpretation resembles so called q-realizabilty, but we refined it to allow arbitrary inductive definition. We proved the soundness of our realizability interpretation.
3. SST contains a pure functional programming language LAMBDA. LAMBDA is formed by taking closed terms in SST. It is purely functional, but for practical conveniences, we extended it to LAMBDA+. We implemented the interpreter of LAMBDA on a workstation.
4. We programmed several systems on top of LAMBDA. We made a metaeircular interpreter of LAMBDA itself, a proof-checking system of SST, and a program-extractor LAMBDA. We can reason about the properties of these programs by the proof-checking system itself. The program-extractor extracts a LAMBDA-program from a proof in SST.
5. Using the above systems, we examined by examples the idea of constructive programming. We made sample proofs, and checked its validity by the proof-checking system, and extracted computational parts by the program-extractor.
As a feed-back of this process, we refined SST and LAMBDA so that these systems become more simple and easy to treat. Less

  • Research Products

    (10 results)

All Other

All Publications (10 results)

  • [Publications] Masahiko Sato・Yukiyoshi Kameyama: "Constructive Programming in SST" Theoretical Fouadations of Knowledge Information Processing. (1989)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] Masahiko Sato: "Qnty:A Concurrent Language Based on Logic and Function" Logic Programming. 1034-1056 (1987)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] Masahiko Sato・Makoto Tatsuta: "Symbolic Set Theory" Mathematical Logic and Its Applications. (1989)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] Masahiko Sato・Yukiyoshi Kameyama: "Constructive Programming based on AAT/Λ" Software-KISORON. 31-6. 1-10 (1989)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] Masahiko Sato: "Symbolic Prof Theory" Jumlage Meeting on Typed Lambda Calcnli. (1989)

    • Description
      「研究成果報告書概要(和文)」より
  • [Publications] Masahiko Sato: "Quty: A Concurrent Language Based on Logic and Function" Logic Programming, MIT Press, pp. 1034-1056, 1987.

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] Masahiko Sato and Makoto Tatsuta: "Symbolic Set Theory" Mathematical Logic and Its Applications, Nagoya, 1989.

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] Masahiko Sato and Yukiyoshi Kameyama: "Constructive Programming in SST" Theoretical Foundations of Knowledge Information Processing, Prague, 1989.

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] Masahiko Sato and Yukiyoshi Kameyama: "Constructive Programming based on SST/A (in Japanese)" Software-KISOTON 31-6, 1989.

    • Description
      「研究成果報告書概要(欧文)」より
  • [Publications] Masahiko Sato: "Symbolic Proof Theory" Jumlage Meeting on Typed Lambda Calculi, Edinburgh, 1989.

    • Description
      「研究成果報告書概要(欧文)」より

URL: 

Published: 1993-03-26  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi