Research output: Contribution to journal › Article

John N Crossley, Iman Poernomo

Original language | English |
---|---|

Pages (from-to) | 71 - 88 |

Number of pages | 18 |

Journal | Journal of Universal Computer Science |

Volume | 7 |

Issue number | 1 |

DOIs | |

Published | 2001 |

**Fred: An Approach to Generating Real, Correct, Reusable Programs from Proofs**Crossley_Fred_2001.pdf, 274 KB, application/pdf

Version:Final published version

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 (see, for example, [HN88], [Con97] and [HKPM97]), 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 [Hen50] 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.

Although program extraction has been developed by many authors (see, for example, [HN88], [Con97] and [HKPM97]), 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 [Hen50] 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.

No data available

King's College London - Homepage

© 2020 King's College London | Strand | London WC2R 2LS | England | United Kingdom | Tel +44 (0)20 7836 5454