The Warshall algorithm and Dickson's lemma: Two examples of realistic program extraction
By means of two well-known examples it is demonstrated that the method of extracting programs from proofs is manageable in practice and may yield efficient programs. The Warshall algorithm computing the transitive closure of a relation is extracted from a constructive proof that repetitions in a path can always be avoided. Second, we extract a program from a classical (i.e., nonconstructive) proof of a special case of Dickson's lemma, by transforming the classical proof into a constructive one. These techniques (as well as the examples) are implemented in the interactive theorem prover MINLOG developed at the University of Munich.
warshall algorithm dickson's lemma program extraction constructive proofs a-translation fealizability provably correct programs