. Anonymous, Premì ere composition de Mathématiques " , concours externe de recrutement de professeurs certifiés, 1995.

D. Bailey, P. Borwein, and S. Plouffe, On the rapid computation of various polylogarithmic constants, Mathematics of Computation, vol.66, issue.218, pp.903-913, 1997.
DOI : 10.1090/S0025-5718-97-00856-9

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

Y. Bertot and G. Allais, Views of PI: Definition and computation, Journal of Formalized Reasoning, vol.7, issue.1, pp.105-129, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01074926

Y. Bertot, Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations, Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP '15, pp.147-155, 2015.
DOI : 10.1145/321941.321944
URL : https://hal.archives-ouvertes.fr/hal-01074927

Y. Bertot, L. Rideau, and L. Théry, Distant Decimals of PI " , https: //www-sop.inria.fr/marelle/distant-decimals-pi, 2017.

F. Besson, Fast Reflexive Arithmetic Tactics the Linear Case and Beyond, Lecture Notes in Computer Science, vol.4502, pp.48-62, 2006.
DOI : 10.1007/978-3-540-74464-1_4
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.96.8457

M. Boepsflug, M. Dénès, and B. Grégoire, Full reduction at full throttle, Proceedings of the 2011 Conference on Certified Programs and Proofs, CPP, Springer LNCS 7086, pp.362-377, 2011.

S. Boldo, C. Lelay, and G. Melquiond, Coquelicot: A User-Friendly Library of Real Analysis for Coq, Mathematics in Computer Science, vol.24, issue.9, pp.41-62, 2015.
DOI : 10.1109/32.713327
URL : https://hal.archives-ouvertes.fr/hal-00860648

S. Boldo and G. Melquiond, Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq, 2011 IEEE 20th Symposium on Computer Arithmetic, pp.243-252, 2011.
DOI : 10.1109/ARITH.2011.40
URL : https://hal.archives-ouvertes.fr/inria-00534854

R. 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
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.98.4721

R. W. Butler, Formalization of the integral Calculus in the PVS Theorem Prover, Journal of Formalized Reasoning, vol.2, issue.1, 2009.

C. Cohen, M. Dénès, and A. Mörtberg, Refinements for Free!, Proceedings of the conference on Certified Programs and Proofs Melbourne , Australia, Springer Lecture Notes in Computer Science 8307, pp.147-162, 2013.
DOI : 10.1007/978-3-319-03545-1_10
URL : https://hal.archives-ouvertes.fr/hal-01113453

L. Cruz-filipe, Constructuve Real Analysis: a Type-Theoretical Formalization and Applications, 2004.

M. Dénès, A. Mörtberg, and V. Siles, A Refinement-Based Approach to Computational Algebra in Coq, proceedings of 3rd international conference on Interactive Theorem Proving, pp.83-98, 2012.
DOI : 10.1007/978-3-642-32347-8_7

J. Filliâtre and A. Paskevich, Why3 ??? Where Programs Meet Provers, Proceedings of the 22nd European Symposium on Programming, pp.125-128, 2013.
DOI : 10.1007/978-3-642-37036-6_8

L. Fousse, G. Hanrot, V. Lefèvre, P. Pélissier, and P. Zimmermann, MPFR, ACM Transactions on Mathematical Software, vol.33, issue.2, 2007.
DOI : 10.1145/1236463.1236468
URL : https://hal.archives-ouvertes.fr/inria-00070266

B. Gourevitch, The World of Pi " , web-site www, 1999.

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

T. Hales, A FORMAL PROOF OF THE KEPLER CONJECTURE, Forum of Mathematics, Pi, vol.41, 2015.
DOI : 10.1007/978-3-642-03359-9_4

J. Harrison, Formalizing basic complex analysis From insight to Proof: Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar and Rhetoric, vol.10, issue.23, pp.151-165, 2007.

J. Hölzl, Proving Inequalities over Reals with Computation in Isabelle, proceedings of PLMMS, 2009.

J. Hölzl, F. Immler, F. , and B. Huffman, Type classes and filters for mathematical analysis in isabelle, Proceedings of the 4th International Conference on Interactive Theorem Proving'13, pp.279-294978, 2013.

R. Krebbers and B. Spitters, Type classes for efficient exact real arithmetic in Coq, Logical Methods in Computer Science, vol.9, issue.1, pp.1-27, 2013.
DOI : 10.2168/LMCS-9(1:1)2013
URL : http://arxiv.org/abs/1106.3448

X. Leroy, Formal verification of a realistic compiler, Communications of the ACM, vol.52, issue.7, pp.107-115, 2009.
DOI : 10.1145/1538788.1538814
URL : https://hal.archives-ouvertes.fr/inria-00415861

´. Erik-martin-dorel and G. Melquiond, Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq, Journal of Automated Reasoning, vol.17, issue.3, pp.187-217, 2016.
DOI : 10.1145/114697.116813

T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle/HOL ? A Proof Assistant for Higher-Order Logic, LNCS, vol.2283, 2002.

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

A. Schönhage and V. Strassen, Fast multiplication of large numbers, Computing, vol.150, issue.3-4, pp.281-292, 1971.
DOI : 10.1007/BF02242355

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