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

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

M. Daumas, L. Rideau, and L. Théry, A Generic Library for Floating-Point Numbers and Its Application to Exact Computing, Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics, pp.169-184, 2001.
DOI : 10.1007/3-540-44755-5_13
URL : https://hal.archives-ouvertes.fr/hal-00157285

M. D. Ercegovac and T. Lang, Digital Arithmetic, 2004.
URL : https://hal.archives-ouvertes.fr/ensl-00542215

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-00103655

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, pp.423-437, 2006.
DOI : 10.1007/11814771_36

J. Harrison, A Machine-Checked Theory of Floating Point Arithmetic, Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics, pp.113-130, 1999.
DOI : 10.1007/3-540-48256-3_9

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, pp.195-210, 2005.
DOI : 10.1007/11541868_13

D. Stevenson, An American national standard: IEEE standard for binary floating point arithmetic, ACM SIGPLAN Notices, vol.22, issue.2, pp.9-25, 1987.

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