TypiCal

When performing the certification of a piece of floating-point code, one usually has to prove properties about errors, which are mathematical expressions relating values from the program and values from the specification. These errors can be split in two categories: rounding errors and method errors, depending on their origin; and the methods for bounding them differ greatly.

I will present two Coq tactics dedicated to proving properties about numerical errors. The "gappa" tactic is an interface to the Gappa external tool; it queries the tool for properties on rounding errors. The "interval" tactic, on the other hand, is designed to deal with method errors, or more generally, differentiable expressions involving elementary functions.

A noteworthy point is that both tactics are themselves based on floating-point arithmetic. Indeed, the proofs they generate are checked by performing intensive numerical computations inside the formal system. For "gappa", these proofs are provided by an oracle, while they are fully reflexive for "interval". I will describe the arithmetic and some of the algorithms they use.