package coq-pi-agm

  1. Overview
  2. No Docs
Computing thousands or millions of digits of PI with arithmetic-geometric means

Install

Dune Dependency

www-sop.inria.fr Edit opam file Versions (12)

Authors

  1. Y
    Yves Bertot <yves.bertot@inria.fr>

Maintainers

  1. Y
    yves.bertot@inria.fr

Sources

pi-agm-1.2.6.tgz
sha256=65f6f470c5942d04b0185c7d9350c6c32dcae1fb05112091f4696edc59e1ea79

Description

This is a proof of correctness for two algorithms to compute PI to high precision using arithmetic-geometric means. A first file contains the calculus-based proofs for an abstract view of the algorithm, where all numbers are real numbers. A second file describes how to approximate all computations using large integers. Other files describe the second algorithm which is close to the one used in mpfr, for instance.

The whole development can be used to produce mathematically proved and formally verified approximations of PI.

Tags

keyword:real analysis keyword:pi category:Mathematics/Real Calculus and Topology logpath:agm date:2020-06-23

Published: 27 Jul 2020

Dependencies (4)

  1. coq-interval >= "4"
  2. coq-coquelicot >= "3" & < "4~"
  3. coq >= "8.12" & < "8.13~"
  4. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None