Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations - Archive ouverte HAL Access content directly
Conference Papers Year : 2015

Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations

(1)
1
Yves Bertot

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.
Fichier principal
Vignette du fichier
main (1).pdf (264.32 Ko) Télécharger le fichier
Vignette du fichier
agm.v (4.1 Ko) Télécharger le fichier
Vignette du fichier
computing.v (239 B) Télécharger le fichier
Vignette du fichier
coq_files.zip (41.35 Ko) Télécharger le fichier
Vignette du fichier
ln_2_10.v (6.1 Ko) Télécharger le fichier
Vignette du fichier
log2.v (47.92 Ko) Télécharger le fichier
Vignette du fichier
README (1.52 Ko) Télécharger le fichier
Vignette du fichier
rounding_big.v (2.16 Ko) Télécharger le fichier
Vignette du fichier
rounding_correct.v (129.87 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Origin : Files produced by the author(s)
Origin : Files produced by the author(s)
Origin : Files produced by the author(s)
Origin : Files produced by the author(s)
Origin : Files produced by the author(s)
Origin : Files produced by the author(s)
Origin : Files produced by the author(s)
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01074927 , version 1 (10-12-2014)

Identifiers

Cite

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⟩
227 View
275 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More