Home Latest Advanced Search By Year By Division 

Not Logged in. Login 
Fred: An approach to generating real, correct, reusable programs from proofsCrossley, John and Poernomo, Iman (2001) Fred: An approach to generating real, correct, reusable programs from proofs. Journal of Universal Computer Science, 7 (1). pp. 7188.
Official URL: http://www.jukm.org/jucs_7_1/fred_an_approach_to AbstractIn this paper we describe our system for automatically extracting "correct" programs from proofs using a development of the CurryHoward 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 higherorder logic to manysorted (firstorder) 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 nontrivial 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.
Repository Staff Only: item control page 
Accessibility  Terms and Conditions  Last Modified 01 November 2007 
© 2007 DCS, King's College London, Strand, London WC2R 2LS, England, United Kingdom. Tel +44 (0)20 7836 5454 