D. Goldberg, What every computer scientist should know about floating-point arithmetic, ACM Computing Surveys, vol.23, issue.1, pp.5-48, 1991.
DOI : 10.1145/103162.103163

V. A. Carreño and P. S. Miner, Specification of the IEEE-854 floating-point standard in HOL and PVS, HOL95: 8th International Workshop on Higher-Order Logic Theorem Proving and Its Applications, 1995.

D. M. Russinoff, Abstract, LMS Journal of Computation and Mathematics, vol.11, pp.148-200, 1998.
DOI : 10.1112/S1461157000000176

J. Harrison, Formal Verification of Floating Point Trigonometric Functions, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, pp.217-233, 2000.
DOI : 10.1007/3-540-40922-X_14
URL : http://www.cl.cam.ac.uk/~jrh13/papers/fmcad00.pdf

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

P. H. Sterbenz, Floating point computation, 1974.

S. Boldo, Formal Verification of Programs Computing the Floating-Point Average Available: https, 17th International Conference on Formal Engineering Methods, ser. Lecture Notes in Computer Science, pp.17-32, 2015.

F. Goualard, How do you compute the midpoint of an interval?, ACM Transactions on Mathematical Software, vol.40, issue.2, pp.1-11, 2014.
DOI : 10.1023/A:1022374804152
URL : https://hal.archives-ouvertes.fr/hal-00576641

P. Kornerup, V. Lefevre, N. Louvet, and J. Muller, On the Computation of Correctly Rounded Sums, IEEE Transactions on Computers, vol.61, issue.3, pp.289-298, 2012.
DOI : 10.1109/TC.2011.27
URL : https://hal.archives-ouvertes.fr/inria-00367584

T. J. Dekker, A floating-point technique for extending the available precision, Numerische Mathematik, vol.5, issue.3, pp.224-242, 1971.
DOI : 10.1007/BF01397083

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

M. Daumas, L. Rideau, and L. Thery, A Generic Library for Floating-Point Numbers and Its Application to Exact Computing, " in Theorem Proving in Higher Order Logics, ser. Lecture Notes in Computer Science Available: https, pp.169-184, 2001.

S. Boldo, S. Graillat, and J. Muller, On the robustness of the 2Sum and Fast2Sum algorithms Available: https, ACM Transactions on Mathematical Software, vol.44, issue.1, 2017.

U. W. Kulisch, Advanced Arithmetic for the Digital Computer, Design of Arithmetic Units, Electronic Notes in Theoretical Computer Science, vol.24, 2002.
DOI : 10.1016/S1571-0661(05)80622-X

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

S. Boldo, Deductive formal verification: How to make your floating-point programs behave Thèse d'habilitation, 2014.
DOI : 10.1109/arith.2007.20
URL : http://www.acsel-lab.com/arithmetic/arith18/papers/ARITH18_Boldo.pdf