G. Gonthier, Formal proof the four-color theorem, Notices of the AMS, p.13821393, 2008.

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

B. Grégoire and L. Théry, A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers, Proceedings of the 3rd International Joint Conference on Automated Reasoning, p.423437, 2006.
DOI : 10.1007/11814771_36

T. C. Hales, A proof of the Kepler conjecture, Annals of Mathematics, vol.162, issue.3, p.10651185, 2005.
DOI : 10.4007/annals.2005.162.1065

G. Melquiond, Proving Bounds on Real-Valued Functions with Computations, Proceedings of the 4th International Joint Conference on Automated Reasoning, p.217, 2008.
DOI : 10.1007/978-3-540-71070-7_2
URL : https://hal.archives-ouvertes.fr/hal-00180138

D. Stevenson, An American national standard: IEEE standard for binary oating point arithmetic, ACM SIGPLAN Notices, vol.22, issue.2, p.925, 1987.

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

D. M. Russino, A mechanically checked proof of IEEE compliance of the AMD-K7 oating point multiplication, division, and square root instructions, LMS Journal of Computation and Mathematics, vol.1, p.148200, 1998.

J. Harrison, A machine-checked theory of oating-point arithmetic, Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics, p.113130, 1999.

M. Daumas, L. Rideau, and L. Théry, A generic library of oating-point numbers and its application to exact computing, Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics, p.169184, 2001.

A. Ziv, Fast evaluation of elementary mathematical functions with correctly rounded last bit, ACM Transactions on Mathematical Software, vol.17, issue.3, p.410423, 1991.
DOI : 10.1145/114697.116813

J. Muller, Elementary Functions, Algorithms and Implementation, 1997.
URL : https://hal.archives-ouvertes.fr/ensl-00000008

C. Muñoz and D. Lester, Real number calculations and theorem proving, Proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics, 2005.

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

P. P. Tang, Table-driven implementation of the logarithm function in IEEE oating-point arithmetic, ACM Transactions on Mathematical Software, vol.16, issue.378400, 1990.