Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development, Coq'Art:the Calculus of Inductive Constructions, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

Y. Bertot, G. Gonthier, S. Ould-biha, and I. Pa¸scapa¸sca, Canonical Big Operators, Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics, pp.12-16, 2008.
DOI : 10.1007/3-540-44659-1_29

URL : https://hal.archives-ouvertes.fr/inria-00331193

S. Basu, R. Pollack, and M. Roy, Algorithms in Real ALgebraic Geometry, Algorithms and Computations in Mathematics, vol.10, 2006.
DOI : 10.1007/978-3-662-05355-3

URL : https://hal.archives-ouvertes.fr/hal-01083587

L. Cruz-filipe, H. Geuvers, and F. Wiedijk, C-CoRN, the Constructive Coq Repository at Nijmegen, Lecture Notes in Computer Science, vol.3119, pp.88-103, 2004.
DOI : 10.1007/3-540-45620-1_12

C. Cohen, Formalizing real analysis for polynomials, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00545778

C. Paul-de, FormesàFormes`Formesà pôles. Hermès, 1985.

R. Descartes and . Géométrie, A source book in Mathematics, 1636.

G. Gonthier and A. Mahboubi, A Small Scale Reflection Extension for the Coq system, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00258384

G. Gonthier and A. Mahboubi, An introduction to small scale reflection in Coq, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00515548

G. Gonthier, A. Mahboubi, L. Rideau, E. Tassi, and L. Théry, A Modular Formalisation of Finite Group Theory, Lecture Notes in Computer Science, vol.4732, pp.86-101, 2007.
DOI : 10.1007/978-3-540-74591-4_8

URL : https://hal.archives-ouvertes.fr/inria-00139131

D. Knuth, Metafont: the Program, 1986.

A. Mahboubi, Implementing the cylindrical algebraic decomposition within the Coq system, Mathematical Structures in Computer Science, vol.17, issue.01, pp.99-127, 2007.
DOI : 10.1017/S096012950600586X

URL : https://hal.archives-ouvertes.fr/hal-00819489

B. Mourrain, F. Rouillier, and M. Roy, Bernstein's basis and real root isolation, Mathematical Sciences Research Institute Publications, 2005.

O. Russell and . Connor, A monadic, functional implementation of real numbers, Mathematical Structures in Computer Science, vol.17, issue.1, pp.129-159, 2007.

O. Russell and . Connor, Certified exact transcendental real number computation in coq, TPHOLs, Lecture Notes in Computer Science, pp.246-261, 2008.

I. Pa¸scapa¸sca, Formal proofs for theoretical properties of newton's method, Mathematical Structures in Computer Science, 2010.

F. Rouillier and P. Zimmermann, Efficient isolation of polynomial's real roots, Journal of Computational and Applied Mathematics, vol.162, issue.1, pp.33-50, 2003.
DOI : 10.1016/j.cam.2003.08.015

A. Sjerp, T. , and D. Van-dalen, Constructivism in Mathematics, an introduction, 1988.

J. Victor and U. , Theory of Equations, 1948.

R. Zumkeller, Global Optimization in Type Theory, 2008.