The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

Hi,

there is the floqc library

http://flocq.gforge.inria.fr/

I have been given a course on how to use this library, the lectures are
here:

ftp://ftp-sop.inria.fr/marelle/Laurent.Thery/FloatingPoint/index.html

It is not covering completely your specific question on using floating
point to perform effective computation. Guillaume Melquiond
(guillaume.melquiond AT inria.fr)
 is the right person to contact.

--
Laurent