MULLER , Jean-Michel

Recently, a complete set of algorithms for manipulating double-word numbers (some classical, some new) was analyzed [15]. We have formally proven all the theorems given in that paper, using the Coq proof assistant. The formal proof work led us to: i) locate mistakes in some of the original paper proofs (mistakes that, however, do not hinder the...

We present a full Coq formalisation of the correctness of some comparison algorithms between binary64 and decimal64 floating-point numbers.

We consider the computation of the Euclidean (or L2) norm of an n-dimensional vector in floating-point arithmetic. We review the classical solutions used to avoid spurious overflow or underflow and/or to obtain very accurate results. We modify a recently published algorithm (that uses double-word arithmetic) to allow for a very accurate...