6 papers
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…
Graphic processors to speed-up simulations for the design of high performance solar receptors
Sylvain Collange, Marc Daumas, David Defour
Graphics Processing Units (GPUs) are now powerful and flexible systems adapted and used for other purposes than graphics calculations (General Purpose computation on GPU -- GPGPU).…
Formal proof for delayed finite field arithmetic using floating point operators
Sylvie Boldo, Marc Daumas, Pascal Giorgi
Formal proof checkers such as Coq are capable of validating proofs of correction of algorithms for finite field arithmetics but they require extensive training from potential users…
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…