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

Optimization in Constructive Programming

Research Project

Project/Area Number 08680367
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeSingle-year Grants
Section一般
Research Field 計算機科学
Research InstitutionKobe University

Principal Investigator

HAYASHI Susumu  Kobe University, Department of Computer and Systems Engineering, Professor, 工学部, 教授 (40156443)

Project Period (FY) 1996 – 1997
Project Status Completed (Fiscal Year 1997)
Budget Amount *help
¥1,800,000 (Direct Cost: ¥1,800,000)
Fiscal Year 1997: ¥400,000 (Direct Cost: ¥400,000)
Fiscal Year 1996: ¥1,400,000 (Direct Cost: ¥1,400,000)
KeywordsProgram verification / Program synthesis / Formal methods / 形式的技法 / 構成的プログラミング / 最適化 / 形式的仕様記述
Research Abstract

The original plan to apply Beradi method to PX system turned to be difficult. Thus we changed the plan. We redesigned PX system so that it has types and so the extracted programs are simply typed. We rebuilt the system throughly even from the basic logical system. The new logical system was called S,and the new implementation is called Proof Works.
The results turned out even better than the original plan, because the system was redone utilizing many new knowledges which were not available at the time PX system was designed and built.
On the course of research, Hayashi got a novel insight on application of constructive programming called "Proof Animation." This new insight, which is a spin-off of the present research, is not only more important than the original aim of the research. It is expected to grow one of central issues of the area in the feature.
One thing we could not achive is that extensive experiments with the system. This is due to the delay caused by the new design and implementation of the entire system. We are continueing it even after the project is officially finished.

Report

(3 results)
  • 1997 Annual Research Report   Final Research Report Summary
  • 1996 Annual Research Report
  • Research Products

    (4 results)

All Other

All Publications (4 results)

  • [Publications] Susumu Hayashi: "Constructive Programming-a personal view-" Combinatorics,Complexity,Logic,Proceedings of DMTCS'96,Springer-Verlag,Singapore. 38-51 (1996)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Susumu Hayashi: "Constructive programming - a personal view -" in Combinatorics, Complexity, Logic, Proceedings of DMTCS'96, Springer-Verlag, Singapore. 38-51 (1996)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Susumu Hayashi: "Constructive Programming -a personal view-" Combinatorics,Complexity,Logic,Proceedings of DMTCS '96,Springer-Verlag,Singapore. 38-51 (1996)

    • Related Report
      1997 Annual Research Report
  • [Publications] D.S.Bridgts: "Combinatorics,Complexity,Logic ; Proceedings of DMTCS'96" Springer-Verlag,Singapore, 422 (1996)

    • Related Report
      1996 Annual Research Report

URL: 

Published: 1996-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi