coq-pi-agm

Computing thousands or millions of digits of PI with arithmetic-geometric means This is a proof of correctness for an algorithm to compute PI to high precision using an algorithm based on 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. The whole development can be used to produce mathematically proved and formally verified approximations of PI.

opam install coq-pi-agm.1.0.0
homepage
http://www-sop.inria.fr/members/Yves.Bertot/
license
CeCILL-B
bugs tracker
yves.bertot@inria.fr
dependencies
coq (>= 8.4pl4 & < 8.5~) & coq-ssreflect = 1.5.0 & coq-coquelicot = 2.0.1
source
http://www.inria.fr/sophia/members/Yves.Bertot/proofs/pi_agm_1_0_0.tar.gz
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-pi-agm/coq-pi-agm.1.0.0