Program Extraction from Large Proof Developments

Abstract. It is well known that mathematical proofs often contain (abstract) algorithms, but although these algorithms can be understood by a human, it still takes a lot of time and effort to implement this algorithm on a computer; moreover, one runs the risk of making mistakes in the process. From a fully formalized constructive proof one can automatically obtain a computer implementation of such an algorithm together with a proof that the program is correct. As an example we consider the fundamental theorem of algebra which states that every non-constant polynomial has a root. This theorem has been fully formalized in the Coq proof assistant. Unfortunately, when we first tried to extract a program, the computer ran out of resources. We will discuss how we used logical techniques to make it possible to extract a feasible program. This example is used as a motivation for a broader perspective on how the formalization of mathematics should be done with program extraction in mind.

• Type: Conference
• Year: 2003
• Where: TPHOL
• Authors: Luís Cruz-Filipe, Bas Spitters
• Keywords: Algorithm, Artificial Intelligence, Coq Proof Assistant, Mathematical Proofs, TPHOL 2003