Skip to Main content Skip to Navigation

Formal study in Coq of pi computations using arithmetic-geometric means

Yves Bertot 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Document type :
Software
Complete list of metadatas

Browse

Present sur SoftwareHeritage
swh:1:dir:47d41cb06472ccf913aba4be5b08aeb725a8888d;origin=https://hal.archives-ouvertes.fr/hal-01767263;visit=swh:1:snp:cd55c2657ac70c9b15ae4384b6af1ae6ce8df512;anchor=swh:1:rev:b1e197c030e66d588987087a193fc3a88d8bd5ed;path=/
 Browse
https://hal.inria.fr/hal-01767263
Contributor : Yves Bertot <>
Submitted on : Monday, April 16, 2018 - 9:18:15 AM
Last modification on : Thursday, January 7, 2021 - 3:40:10 PM

Metadata


Software License
MIT License

Collections

INRIA | UNIV-COTEDAZUR

Citation

Yves Bertot. Formal study in Coq of pi computations using arithmetic-geometric means. 2018, ⟨swh:1:dir:47d41cb06472ccf913aba4be5b08aeb725a8888d;origin=https://hal.archives-ouvertes.fr/hal-01767263;visit=swh:1:snp:cd55c2657ac70c9b15ae4384b6af1ae6ce8df512;anchor=swh:1:rev:b1e197c030e66d588987087a193fc3a88d8bd5ed;path=/⟩. ⟨hal-01767263⟩

Share

Metrics

Record views

779

Files downloads

144

 

Contact                    Legal Notice                    Personal Data