A Coq Library on Floating-Point Arithmetic

This library was first designed by Laurent Théry and Laurence Rideau. Contributors now include Laurent Fousse, Guillaume Melquiond and Sylvie Boldo (maintainer).

All the versions of the library: using Coq V7.4, V8.0, V8.1 or V8.2 are downloadable on this page.
Click here to access the library via various indexes (by module, definition, lemma...)
The last developments are:
- the AlgoPredSucc file: an algorithm to compute the predecessor and the successor using rounding to nearest (see the article).
- the FmaEmul file: results on a software emulation of the FMA using rounding to odd (see the DblRndOdd file).
- the discriminant, discriminant2 and discriminant3 files: a property about a program computating the discriminant by Pr W. Kahan.
- the FArgReduct2, FArgReduct3, FArgReduct4 files: proved algorithms for argument reductions.
To go back to the main page of the project.

The following graph, made using dot, describes the dependences between all the files of the library. All the nodes are clickable to access directly the file.
The colors refer to the directory where the file lie and to the subject matter: beige for the initial library, green for the expansions, violet for the two's complement, blue for the elementary functions evaluation and red for the other files.