2 citations · 2 across the 5 of their papers we have counts for
4 papers · 1 filter
Formally Verified Argument Reduction with a Fused-Multiply-Add
Sylvie Boldo, Marc Daumas, Ren Cang Li
Cody & Waite argument reduction technique works perfectly for reasonably large arguments but as the input grows there are no bit left to approximate the constant with enough accura…
Verified Real Number Calculations: A Library for Interval Arithmetic
Marc Daumas, David Lester, César Muñoz
Real number calculations on elementary functions are remarkably difficult to handle in mechanical proofs. In this paper, we show how these calculations can be performed within a th…
Certification of bounds on expressions involving rounded operators
Marc Daumas, Guillaume Melquiond
Gappa uses interval arithmetic to certify bounds on mathematical expressions that involve rounded as well as exact operators. Gappa generates a theorem with its proof for each boun…
Computer validated proofs of a toolset for adaptable arithmetic
Sylvie Boldo, Marc Daumas, Claire Moreau-Finot +1
Most existing implementations of multiple precision arithmetic demand that the user sets the precision {\em a priori}. Some libraries are said adaptable in the sense that they dyna…