Program Extraction from Large Proof Developments

9 years 5 months ago
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.
Luís Cruz-Filipe, Bas Spitters
Added 05 Jul 2010
Updated 05 Jul 2010
Type Conference
Year 2003
Authors Luís Cruz-Filipe, Bas Spitters
Comments (0)