Home Latest Advanced Search By Year By Division 

Not Logged in. Login 
Protocols between programs and proofsPoernomo, Iman and Crossley, John (2001) Protocols between programs and proofs. In: Logic Based Program Synthesis and Transformation, 10th International Workshop, LOPSTR 2000 London, UK, July 24–28, 2000 Selected Papers.
AbstractIn this paper we describe a new protocol that we call the CurryHoward 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 wellknown CurryHoward process. Program extraction has been developed by many authors, 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. As an example of our protocol we describe a constructive proof of the wellknown 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 (nontrivial) disjoint cycles 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 