King's College London

Research portal

Fred: An Approach to Generating Real, Correct, Reusable Programs from Proofs

Research output: Contribution to journalArticle

John N Crossley, Iman Poernomo

Original languageEnglish
Pages (from-to)71 - 88
Number of pages18
JournalJournal of Universal Computer Science
Issue number1


King's Authors


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.

Download statistics

No data available

View graph of relations

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