Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations

Yves Bertot 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : We describe two approaches for the computation of mathematical constant approximations inside interactive theorem provers. These two approaches share the same basis of fixed point computation and differ only in the way the proofs of correctness of the approximations are described. The first approach performs interval computations, while the second approach relies on bounding errors, for example with the help of derivatives. As an illustration, we show how to describe good approximations of the logarithm function and we compute π to a precision of a million decimals inside the proof system, with a guarantee that all digits up to the millionth decimal are correct. All these experiments are performed with the Coq system, but most of the steps should apply to any interactive theorem prover.
Type de document :
Communication dans un congrès
Certified Programs and Proofs (CPP'15), Jan 2015, Mumbai, India. ACM, 2015, <10.1145/2676724.2693172>
Liste complète des métadonnées


https://hal.inria.fr/hal-01074927
Contributeur : Yves Bertot <>
Soumis le : mercredi 10 décembre 2014 - 15:54:17
Dernière modification le : lundi 5 octobre 2015 - 17:01:28
Document(s) archivé(s) le : mercredi 11 mars 2015 - 11:27:24

Identifiants

Collections

Citation

Yves Bertot. Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations. Certified Programs and Proofs (CPP'15), Jan 2015, Mumbai, India. ACM, 2015, <10.1145/2676724.2693172>. <hal-01074927>

Partager

Métriques

Consultations de
la notice

174

Téléchargements du document

376