@inproceedings{c686fc64f03d423daa23b9ddce686a9c,

title = "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 these algorithms 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.",

author = "L. Cruz-Filipe and B.A.W. Spitters",

year = "2003",

doi = "10.1007/10930755_14",

language = "English",

isbn = "3-540-40664-6",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "205--220",

editor = "D.A. Basin and B. Wolff",

booktitle = "Theorem Proving in Higher Order Logics (Proceedings 16th International Conference, TPHOLs 2003, Rome, Italy, September 8-12, 2003)",

address = "Germany",

}