Menu_Home Home   Menu_Latest Latest   Menu_Search Advanced Search   Menu_Browse_by_Year By Year   Menu_Browse_by_Division By Division
Screen decoration graphicsLogo

Fred: An approach to generating real, correct, reusable programs from proofs

Crossley, John and Poernomo, Iman (2001) Fred: An approach to generating real, correct, reusable programs from proofs. Journal of Universal Computer Science, 7 (1). pp. 71-88.

PDF - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL:


In this paper we describe our system for automatically extracting "correct" programs from proofs using a development of the Curry-Howard process. Although program extraction has been developed by many authors, 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 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 (total, recursive) functions; 4. the use of templates to make the reasoning much closer to normal mathematical proofs and 5. a conceptual distinction between the computational type theory (for representing programs)and the logical type theory (for reasoning about programs). 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.

Item Type:Article
ID Code:250
Deposited By:Dr Iman Poernomo
Deposited On:08 Nov 2007 17:14
Last Modified:06 Feb 2008 14:41

Repository Staff Only: item control page