This is an unofficial reimagining of the Archive of Formal Proofs
A Formal Model of IEEE Floating Point Arithmeticby Lei Yu