A Formal Model of IEEE Floating Point Arithmetic.
Lei Yu · 2013
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 arith-metic, 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 pro-gramming languages. The definitions of the IEEE standard in Isabelle is ported from HOL Light [1].