M. Armand, B. Grégoire, A. Spiwack, and L. Théry, Extending Coq with Imperative Features and Its Application to SAT Verification, Interactive Theorem Proving, First International Conference, pp.83-98, 2010.
DOI : 10.1007/978-3-642-14052-5_8
URL : https://hal.archives-ouvertes.fr/inria-00502496

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

F. Besson, Fast Reflexive Arithmetic Tactics the Linear Case and Beyond, Types for Proofs and Programs, pp.48-62, 2006.
DOI : 10.1007/978-3-540-74464-1_4

F. Besson, P. Cornilleau, and D. Pichardie, Modular SMT Proofs for Fast Reflexive Checking Inside Coq, Certified Programs and Proofs -First International Conference, pp.151-166, 2011.
DOI : 10.1016/j.jal.2007.07.003
URL : https://hal.archives-ouvertes.fr/hal-00646960

M. Jonathan, P. B. Borwein, and . Borwein, Pi and the AGM, 1987.

R. P. Brent, Fast Multiple-Precision Evaluation of Elementary Functions, Journal of the ACM, vol.23, issue.2, pp.242-251, 1976.
DOI : 10.1145/321941.321944

M. Daumas, D. R. Lester, and C. Muñoz, Verified Real Number Calculations: A Library for Interval Arithmetic, IEEE Transactions on Computers, vol.58, issue.2, pp.226-237, 2009.
DOI : 10.1109/TC.2008.213
URL : https://hal.archives-ouvertes.fr/hal-00168402

M. Daumas, G. Melquiond, and C. Muñoz, Guaranteed Proofs Using Interval Arithmetic, 17th IEEE Symposium on Computer Arithmetic (ARITH'05), pp.188-195, 2005.
DOI : 10.1109/ARITH.2005.25
URL : https://hal.archives-ouvertes.fr/hal-00164621

B. Grégoire and L. Théry, A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers, Automated Reasoning, Third International Joint Conference Proceedings, pp.423-437, 2006.
DOI : 10.1007/11814771_36

J. Harrison, The HOL Light theorem prover, 2010.

C. Kaliszyk and R. O. Connor, Computing with Classical Real Numbers, Journal of Formalized Reasoning, vol.2, issue.1, 2009.

G. Melquiond, Floating-point arithmetic in the Coq system, 8th Conference on Real Numbers and Computers, pp.93-102, 2008.
DOI : 10.1016/j.ic.2011.09.005
URL : https://hal.archives-ouvertes.fr/hal-00797913

E. Salamin, Computation of ? Using Arithmetic-Geometric Mean, Mathematics of Computation, vol.30, issue.135, pp.565-570, 1976.

A. Solovyev, Formal Computations and Methods, 2012.

A. Solovyev and T. C. Hales, Formal Verification of Nonlinear Inequalities with Taylor Interval Approximations, NASA Formal Methods , 5th International Symposium, NFM 2013, pp.383-397, 2013.
DOI : 10.1007/978-3-642-38088-4_26

P. Zimmermann, Reliable computing with GNU MPFR Joris van der Hoeven, Komei Fukuda Third International Congress on Mathematical Software, ICMS 2010, pp.42-45, 2010.