A layered approach to extracting programs from proofs with an application in graph theory

In this paper we describe our system for automatically extracting "correct" programs from proofs using a development for the Curry-Howard process. Although program extraction has been developed by many authors (see [5,?,?]), our system has a number of novel features designed to make it very easy to use and as close as possible to ordinary mathematical terminology and practice. These features include 1. the use of Henkin's technique [6] to reduce higher-order logic to many-sorted (first-order) logic 2. the free use of new rules for induction subject to certain conditions 3. the extensive use of previously programmed (primitive) recursive functions. 4. the use of templates to make the reasoning much closer to normal mathematical proffs. 5. an extension of the technique of the use of Harrop formulae to classically true formulae (cf. the footnote on p.101 in Kreisel [9]); As an example of our system we give a constructive proof of the well-known theorem that every graph of even parity, which is non-trivial in the sense that it does not consist of isolated vertices, has a cycle. Given such a graph as input, the extracted program produces a cycle as promised.