A. Avizienis, Signed-digit number representations for fast parallel arithmetic, IRE Transactions on Electronic Computers, vol.10, p.389400, 1961.

S. Boldo and G. Melquiond, Flocq: A unied library for proving oating-point algorithms in coq, 20th IEEE Symposium on Computer Arithmetic (ARITH), p.243252, 2011.

R. Brent, C. Percival, and P. Zimmermann, Error bounds on complex oating-point multiplication, Mathematics of Computation, vol.76, p.14691481, 2007.

M. Daumas, L. Rideau, and L. Théry, A generic library for oating-point numbers and its application to exact computing, 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'01), p.169184, 2001.

G. Everest, A. Van-der-poorten, I. Shparlinski, and T. Ward, Recurrence Sequences , volume 104 of Mathematical Surveys and Monographs, 2003.

J. Harrison, A machine-checked theory of oating point arithmetic, 12th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'99), p.130, 1999.

C. Jeannerod, N. Louvet, and J. Muller, Further analysis of Kahan???s algorithm for the accurate computation of $2\times 2$ determinants, Mathematics of Computation, vol.82, issue.284, p.22452264, 2013.
DOI : 10.1090/S0025-5718-2013-02679-8

C. Jeannerod, N. Louvet, and J. Muller, On the componentwise accuracy of complex oating-point division with an FMA, 21st IEEE Symposium on Computer Arithmetic (ARITH), p.8390, 2013.

G. Melquiond, Floating-point arithmetic in the Coq system, Information and Computation, vol.216, p.1423, 2012.
DOI : 10.1016/j.ic.2011.09.005
URL : https://hal.archives-ouvertes.fr/hal-00797913

J. Muller, On the error of computing ab+cd using Cornea, Harrison and Tang's method, ACM Transactions on Mathematical Software, vol.41, issue.2, pp.7-17