Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
|
 |
Protocols between Programs and Proofs
| |
|
2. Protocols between Programs and Proofs
Iman Poernomo5  and John N. Crossley5
| (5) |
School of Computer Science and Software Engineering, Monash University, Clayton, Victoria, Australia, 3168 |
Abstract
In this paper we describe a new protocol that we call the Curry-Howard protocol between a theory and the programs extracted from it. This protocol leads to the expansion of the theory and the production
of more powerful programs. The methodology we use for automatically extracting “correct” programs from proofs is a development
of the well-known Curry-Howard process. Program extraction has been developed by many authors (see, for example, [ 9], [ 5] and [ 12]), but our presentation is ultimately aimed at a practical, usable system and has a number of novel features. These include
| 1. |
a very simple and natural mimicking of ordinary mathematical practice and likewise the use of established computer programs
when we obtain programs from formal proofs, and
|
| 2. |
a conceptual distinction between programs on the one hand, and proofs of theorems that yield programs on the other.
|
An implementation of our methodology is the Fred system.1 As an example of our protocol we describe a constructive proof of
the well-known theorem that every graph of even parity can be decomposed into a list of disjoint cycles. Given such a graph
as input, the extracted program produces a list of the (non-trivial) disjoint cycles as promised.
Research partly supported by ARC grant A 49230989.
The authors are deeply indebted to John S. Jeavons and Bolis Basit who produced the graph-theoretic proof that we use.
Fulltext Preview (Small, Large)
 References secured to subscribers.
|
|
|
|
|
|