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, N. Magaud, and P. Zimmermann, A Proof of GMP Square Root, Journal of Automated Reasoning, vol.29, issue.3/4, pp.225-252, 2002.
DOI : 10.1023/A:1021987403425
URL : https://hal.archives-ouvertes.fr/inria-00101044

R. P. Brent and P. Zimmermann, Modern Computer Arithmetic, 2006.
DOI : 10.1017/CBO9780511921698
URL : https://hal.archives-ouvertes.fr/cel-01500109

L. Cruz-filipe, H. Geuvers, and F. Wiedijk, C-CoRN, the Constructive Coq Repository at Nijmegen, Mathematical Knowledge Management, Third International Conference, MKM, pp.88-103, 2004.
DOI : 10.1007/3-540-45620-1_12

J. D. Fleuriot, On the Mechanization of Real Analysis in Isabelle/HOL, Theorem Proving in Higher Order Logics: 13th International Conference, pp.146-162, 2000.
DOI : 10.1007/3-540-44659-1_10

R. Gamboa and M. Kaufmann, Nonstandard Analysis in ACL2, Journal of Automated Reasoning, vol.27, issue.4, pp.323-428, 2001.
DOI : 10.1023/A:1011908113514

E. Giménez, Codifying guarded definitions with recursive schemes, Types for proofs and Programs, pp.39-59, 1994.
DOI : 10.1007/3-540-60579-7_3

J. Harrison, Theorem Proving with the Real Numbers, 1998.
DOI : 10.1007/978-1-4471-1591-5

J. Harrison, Formal verification of square root algorithms. Formal Methods in System Design, pp.143-153, 2003.

N. Hur and J. H. Davenport, A Generic Root Operation for Exact Real Arithmetic, p.82, 2001.
DOI : 10.1007/3-540-45335-0_6

N. Julien, Certified Exact Real Arithmetic Using Co-induction in Arbitrary Integer Base, Functional and Logic Programming Symposium (FLOPS), 2008.
DOI : 10.1007/978-3-540-78969-7_6
URL : https://hal.archives-ouvertes.fr/inria-00202744

C. Kaliszyk and R. Connor, Computing with classical real numbers. CoRR, abs/0809, 1644.

R. David and . Lester, Real Number Calculations and Theorem Proving, Lecture Notes in Computer Science, vol.5170, pp.215-229, 2008.

M. Mayero, Formalisation et automatisation de preuves en analyses reelle et numerique, 2001.

M. Niqui, Coinductive Formal Reasoning in Exact Real Arithmetic, Logical Methods in Computer Science, vol.4, issue.3, pp.1-40, 2008.
DOI : 10.2168/LMCS-4(3:6)2008

O. Russell and . Connor, Certified Exact Transcendental Real Number Computation in Coq, Theorem Proving in Higher Order Logics, 21st International Conference, pp.246-261, 2008.

I. Pa¸scapa¸sca, A Formal Verification for Kantorovitch's Theorem, Journées Francophones des Langages Applicatifs, pp.15-29, 2008.

J. Sawada and R. Gamboa, Mechanical Verification of a Square Root Algorithm Using Taylor???s Theorem, Lecture Notes in Computer Science, vol.2517, pp.274-291, 2002.
DOI : 10.1007/3-540-36126-X_17

N. Shankar, S. Owre, and J. M. Rushby, The PVS Proof Checker: A Reference Manual, 1993.