Authors: Luís Cruz-Filipe, Pierre Letouzey
Title: Executing Extracted Programs
Abstract: 
It is a well-known fact that algorithms are often hidden inside
mathematical proofs. If these proofs are formalized inside a
proof assistant, then a mechanism called extraction can
generate the corresponding programs automatically.
In previous work, it has been explained how a program has been
(with difficulty) produced from a formalization of the Fundamental
Theorem of Algebra inside the Coq proof assistant. This program
theoretically allows one to compute approximations of polynomial
roots. But there is currently quite a gap between theory and practice.
In this sequel work, we focus on studying the complexity of this
program, and tried to analyze the reasons of its inefficiency by
looking at selected sub-problems, like computation of series giving
values of Euler constant e or \sqrt{2}.