I am the maintainer and main contributor of a netlib library.
The "Formal Proofs on Floating Point" library (FP2) is a set of formal definitions and theorems (including proofs) to reason about floating point numbers. It is now stored in the "FP" section of NetLib for public use. It enables users to formally define types and operations of floating arithmetic and to deduce properties using a mechanized proof checker.
This library was first designed by
Marc
Daumas,
Laurent Théry* and
Laurence
Rideau*.
Contributors now include
Sylvie Boldo*,
Jean-Michel
Muller,
Laurent Fousse*,
Ren-Cang Li and
Guillaume
Melquiond*.
Contributors that were directly interacting with Coq are outlined by a
star.
There is also an official web page and a technical page for download and CVS access.
This library is the one used by the Caduceus and Why tools for program certification.
I wrote a tiny part of the NASA Langley PVS Libraries that deals with floating-point arithmetic.
The formalization is the same as the previous one (except it uses PVS features). It also contains links with the previous bit-level NASA formalization so that previous results can be transfered both ways.