(23) Program Generation System: PAPYRUS

	Machine:     PSI
	Environment: SIMPOS
	Language:    ESP
	Source Code: 4 MB
	Documents:   Manual (English/Japanese)

Overview

This system provids various supports function for extracting a program from constructive proofs of the formula as the program specification.

PAPYRUS consists of two main components:

To define the logic,description format,and program extraction rules,and the other checks proofs and extracts programs according to the definitions.
A proof editor for making proof construction as simple as possible.

PAPYRUS is the system for generating programs based on Curry-Howard Isomorphism.

Main features is as follows:

PAPYRUS manages logical definitions as type data of CC. Therefore,changing that data enables the use of various logics for program generation.
PAPYRUS has a built-in proof checker based on CC,and automatically checks each partial proof as soon as it is made.
PAPYRUS manages program extraction rules as rules of TRS. Therefore,changing that data enables the use of various realizability interpretations. Furthermore,programs can be extracted from the completed proofs according to the rules.
PAPYRUS allows the use of various description formats through a macro definition mechanism based on TRS(Term Rewriting System).
The operator can call the prover freely to construct proofs interactively.
Various support functions are provided by the structure editor,such as the function to jump to unproven portions.