Distant decimals of : formal proofs of some algorithms computing them and guarantees of exact computation
DOI10.1007/S10817-017-9444-2zbMATH Open1448.68455OpenAlexW2780997459WikidataQ113901245 ScholiaQ113901245MaRDI QIDQ1663216FDOQ1663216
Yves Bertot, Laurent Théry, Laurence Rideau
Publication date: 21 August 2018
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-017-9444-2
Coq proof assistantPIarithmetic geometric meansBailey-Borwein-Plouffe formulaBBPformal proofs in real analysis
Evaluation of number-theoretic constants (11Y60) Numerical approximation and computational geometry (primarily algorithms) (65D99) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Why3 — Where Programs Meet Provers
- Coquelicot: a user-friendly library of real analysis for Coq
- Isabelle/HOL. A proof assistant for higher-order logic
- Fast multiplication of large numbers
- MPFR
- Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
- A Refinement-Based Approach to Computational Algebra in Coq
- Fast Multiple-Precision Evaluation of Elementary Functions
- Refinements for Free!
- Proving tight bounds on univariate expressions with elementary functions in Coq
- On the rapid computation of various polylogarithmic constants
- Certified Exact Transcendental Real Number Computation in Coq
- Type classes for efficient exact real arithmetic in Coq
- A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers
- A proof of GMP square root
- Computation of π Using Arithmetic-Geometric Mean
- Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
- Views of Pi: definition and computation
- Extending Coq with Imperative Features and Its Application to SAT Verification
Cited In (5)
- Parallel implementation of multiple-precision arithmetic and 2,576,980,370,000 decimal digits of \(\pi \) calculation
- Title not available (Why is that?)
- Quantitative continuity and Computable Analysis in Coq
- What is the point of computers? A question for pure mathematicians
- New proofs of Borwein-type algorithms for Pi
Uses Software
This page was built for publication: Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1663216)
