A Formal Model of IEEE Floating Point Arithmetic

Lei Yu 📧 with contributions from Fabian Hellauer 📧 and Fabian Immler 🌐

July 27, 2013

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


This development provides a formal model of IEEE-754 floating-point arithmetic. This formalization, including formal specification of the standard and proofs of important properties of floating-point arithmetic, forms the foundation for verifying programs with floating-point computation. There is also a code generation setup for floats so that we can execute programs using this formalization in functional programming languages.


BSD License


February 5, 2018
'Modernized' representation following the formalization in HOL4: former "float_format" and predicate "is_valid" is now encoded in a type "('e, 'f) float" where 'e and 'f encode the size of exponent and fraction.
September 25, 2017
Added conversions from and to software floating point numbers (by Fabian Hellauer and Fabian Immler).


Session IEEE_Floating_Point