Floating point verification in HOL Light: the exponential function

. Since they often embody compact but mathematically sophisticated algorithms, operations for computing the common transcendental functions in floating point arithmetic seem good targets for formal verification using a mechanical theorem prover. We discuss some of the general issues that arise in verifications of this class, and then present a machine-checked verification of an algorithm for computing the exponential function in IEEE-754 standard binary floating point arithmetic. We confirm (indeed strengthen) the main result of a previously published error analysis, though we uncover a minor error in the hand proof and are forced to confront several subtle issues that might easily be overlooked informally. 1 Introduction Algorithms for performing floating point operations are often rather complex. It is difficult to make sure they are correct --- for example, a bug in the floatingpoint division instruction of the Intel Pentium gained widespread publicity quite recently (Pratt 1995). W..