D. Stevenson, A Proposed Standard for Binary Floating-Point Arithmetic, Computer, vol.14, issue.3, pp.51-62, 1981.
DOI : 10.1109/C-M.1981.220377

G. Melquiond and S. Pion, Formally certified floating-point filters for homogeneous geometric predicates, Theoretical Informatics and Applications, pp.57-70, 2007.
DOI : 10.1051/ita:2007005
URL : https://hal.archives-ouvertes.fr/inria-00071232

S. A. Figueroa, When is double rounding innocuous?, ACM SIGNUM Newsletter, vol.30, issue.3, pp.21-26, 1995.
DOI : 10.1145/221332.221334

J. Neumann, First Draft of a Report on the EDVAC, IEEE Annals of the History of Computing, vol.15, issue.4, pp.27-75, 1993.
DOI : 10.1007/978-3-642-61812-3_30

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

C. Lee, Multistep gradual rounding, IEEE Transactions on Computers, vol.38, issue.4, pp.595-600, 1989.
DOI : 10.1109/12.21152

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

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

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

S. Boldo, G. J. Melquiond13-]-t, and . Dekker, When double rounding is odd A floating point technique for extending the available precision, Proceedings of the 17th IMACS World Congress on Computational and Applied Mathematics, pp.224-242, 1971.

D. E. Knuth, The Art of Computer Programming: Seminumerical Algorithms, 1969.

S. Boldo, Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms, Third International Joint Conference on Automated Reasoning, 2006.
DOI : 10.1007/11814771_6

N. J. Higham, Accuracy and stability of numerical algorithms, SIAM, 1996.
DOI : 10.1137/1.9780898718027

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

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

D. M. Priest, Algorithms for arbitrary precision floating point arithmetic, [1991] Proceedings 10th IEEE Symposium on Computer Arithmetic, pp.132-144, 1991.
DOI : 10.1109/ARITH.1991.145549
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.55.3546

M. Daumas, Multiplications of floating point expansions, Proceedings 14th IEEE Symposium on Computer Arithmetic (Cat. No.99CB36336), pp.250-257, 1999.
DOI : 10.1109/ARITH.1999.762851

F. De-dinechin, C. Q. Lauter, and J. Muller, Fast and correctly rounded logarithms in double-precision, Theoretical Informatics and Applications, pp.85-102, 2007.
DOI : 10.1051/ita:2007003
URL : https://hal.archives-ouvertes.fr/inria-00070331

C. Q. Lauter, Basic building blocks for a triple-double intermediate format, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00070314

V. Lefèvre and J. Muller, Worst cases for correct rounding of the elementary functions in double precision, Proceedings 15th IEEE Symposium on Computer Arithmetic. ARITH-15 2001, pp.111-118, 2001.
DOI : 10.1109/ARITH.2001.930110