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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [17 references]  Display  Hide  Download

https://hal.inria.fr/hal-01074927
Contributor : Yves Bertot <>
Submitted on : Wednesday, December 10, 2014 - 3:54:17 PM
Last modification on : Monday, September 3, 2018 - 10:56:07 AM
Long-term archiving on : Wednesday, March 11, 2015 - 11:27:24 AM

Identifiers

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. ⟨10.1145/2676724.2693172⟩. ⟨hal-01074927⟩

Share

Metrics

Record views

331

Files downloads

548