G. Barrett, Formal methods applied to a floating-point number system, IEEE Transactions on Software Engineering, vol.15, issue.5, pp.611-621, 1989.
DOI : 10.1109/32.24710

V. A. Carreño and P. S. Miner, Specification of the IEEE-854 floatingpoint standard in HOL and PVS, Proceedings of the International Workshop on Higher Order Logic Theorem Proving and its Applications, 1995.

P. Loiseleur, Formalisation en Coq de la norme IEEE-754 sur l'arithmétiquè a virgule flottante, 1997.

J. S. Moore, T. W. Lynch, and M. Kaufmann, A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program, IEEE Transactions on Computers, vol.47, issue.9, pp.913-926, 1998.
DOI : 10.1109/12.713311

D. M. Russinoff, A Case Study in Formal Verification of Register-Transfer Logic with ACL2: The Floating Point Adder of the AMD Athlon TM Processor, Proceedings of the 3rd International Conference on Formal Methods in Computer-Aided Design, ser. Lecture Notes in Computer Science, pp.3-36, 2000.
DOI : 10.1007/3-540-40922-X_3

R. Kaivola and K. Kohatsu, Proof engineering in the large: formal verification of Pentium???4 floating-point divider, International Journal on Software Tools for Technology Transfer (STTT), vol.4, issue.3, pp.323-334, 2003.
DOI : 10.1007/s10009-002-0081-6

C. Jacobi and C. Berg, Formal Verification of the VAMP Floating Point Unit, Formal Methods in System Design, pp.227-266, 2005.
DOI : 10.1007/s10703-005-1613-y

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

]. M. Daumas, L. Rideau, and L. Théry, A generic library of floatingpoint numbers and its application to exact computing, Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics, pp.169-184, 2001.

S. Boldo, Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms, Proceedings of the 3rd International Joint Conference on Automated Reasoning, ser. Lecture Notes in Computer Science, pp.52-66, 2006.
DOI : 10.1007/11814771_6

G. Melquiond, Floating-point arithmetic in the Coq system, Proceedings of the 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

M. Daumas and G. Melquiond, Certification of bounds on expressions involving rounded operators, ACM Transactions on Mathematical Software, vol.37, issue.1, pp.1-20, 2010.
DOI : 10.1145/1644001.1644003
URL : https://hal.archives-ouvertes.fr/hal-00127769

S. Boldo, J. Filliâtre, and G. Melquiond, Combining Coq and Gappa for Certifying Floating-Point Programs, Proceedings of the 16th Calculemus Symposium, pp.59-74, 2009.
DOI : 10.1109/TC.2008.200
URL : https://hal.archives-ouvertes.fr/inria-00432726

S. Boldo and M. Daumas, Representable correcting terms for possibly underflowing floating point operations, 16th IEEE Symposium on Computer Arithmetic, 2003. Proceedings., pp.79-86, 2003.
DOI : 10.1109/ARITH.2003.1207663

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

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

D. M. Priest, Algorithms for arbitrary precision floating point arithmetic, [1991] Proceedings 10th IEEE Symposium on Computer Arithmetic, pp.132-145, 1991.
DOI : 10.1109/ARITH.1991.145549

J. Harrison, Formal Verification of Square Root Algorithms, Formal Methods in System Design, vol.22, issue.2, pp.143-153, 2003.
DOI : 10.1023/A:1022973506233

P. H. Sterbenz, Floating-Point Computation, 1974.

N. J. Higham, Accuracy and Stability of Numerical Algorithms, SIAM, 1996.
DOI : 10.1137/1.9780898718027

D. Knuth, The Art of Computer Programming, 1998.

T. Ogita, S. M. Rump, and S. Oishi, Accurate Sum and Dot Product, SIAM Journal on Scientific Computing, vol.26, issue.6, 2005.
DOI : 10.1137/030601818
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.2.1547

S. Boldo and J. Filliâtre, Formal Verification of Floating-Point Programs, 18th IEEE Symposium on Computer Arithmetic (ARITH '07), pp.187-194, 2007.
DOI : 10.1109/ARITH.2007.20
URL : https://hal.archives-ouvertes.fr/hal-01174892

X. Leroy, A Formally Verified Compiler Back-end, Journal of Automated Reasoning, vol.27, issue.1, pp.363-446, 2009.
DOI : 10.1007/s10817-009-9155-4
URL : https://hal.archives-ouvertes.fr/inria-00360768