Protocols between Programs and Proofs

Abstract. In this paper we describe a new protocol that we call the Curry-Howard protocol between a theory and the programs extracted from it. This protocol leads to the expansion of the theory and the pro-duction of more powerful programs. The methodology we use for auto-matically extracting “correct ” programs from proofs is a development of the well-known Curry-Howard process. Program extraction has been developed by many authors (see, for example, [9], [5] and [12]), 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 prac-tice 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.1 As an ex-ample of our protocol we describe a constructive proof of the well-known 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 (non-trivial) disjoint cycles as promised.