Y. Bertot and P. Casteran, Coq'Art : the Calculus of Inductive Constructions. Texts in Theoretical Computer Science, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

S. Boldo, Preuves formelles en arithmétiquesarithmétiques`arithmétiquesà virgule flottante, 2004.

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

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

D. Stevenson, A proposed standard for binary floating point arithmetic, IEEE Computer, vol.14, issue.3, pp.51-62, 1981.
DOI : 10.1109/c-m.1981.220377

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