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

S. Boldo and M. Daumas, Properties of two???s complement floating point notations, International Journal on Software Tools for Technology Transfer, vol.22, issue.2-3, pp.2-3, 2004.
DOI : 10.1112/S1461157000000176

M. Daumas, L. Rideau, and L. Théry, A Generic Library for Floating-Point Numbers and Its Application to Exact Computing, 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

J. W. Demmel and Y. Hida, Fast and Accurate Floating Point Summation with Application to Computational Geometry, Proceedings of the 10th GAMM-IMACS International Symposium on Scientific Computing, Computer Arithmetic, and Validated Numerics, 2002.
DOI : 10.1023/B:NUMA.0000049458.99541.38

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
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.1.7712

N. J. Higham, Accuracy and stability of numerical algorithms, SIAM, 1996.

. Ste and D. Stevenson, A proposed standard for binary floating point arithmetic, IEEE Computer, vol.14, issue.3, pp.51-62, 1981.

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