Mechanizing Olver's Error Arithmetic

Max Fan, Ariel E. Kellison, Samuel D. Pollard

We mechanize the fundamental properties of a rounding error model for floating-point arithmetic based on relative precision, a measure of error proposed as a substitute for relativ…