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

Yves Bertot

Software Year :

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

(1)

1

Yves Bertot

Function : Author
PersonId : 21022
IdHAL : yves-bertot
ORCID : 0000-0001-5052-3019
IdRef : 060348313

Mathematical, Reasoning and Software

Domains

Computer Science [cs] Logic in Computer Science [cs.LO] Computer Science [cs] Computer Arithmetic Computer Science [cs] Data Structures and Algorithms [cs.DS]

Yves Bertot : Connect in order to contact the contributor

https://hal.inria.fr/hal-01767263

Submitted on : Monday, April 16, 2018-9:18:15 AM

Last modification on : Saturday, June 25, 2022-11:29:55 PM

Dates and versions

hal-01767263 , version 1 (16-04-2018)

Identifiers

HAL Id : hal-01767263 , version 1
SWHID : swh:1:dir:47d41cb06472ccf913aba4be5b08aeb725a8888d;origin=https://hal.archives-ouvertes.fr/hal-01767263;visit=swh:1:snp:cd55c2657ac70c9b15ae4384b6af1ae6ce8df512;anchor=swh:1:rev:b1e197c030e66d588987087a193fc3a88d8bd5ed;path=/

version :
Software License : MIT License
Code Repository :

Cite

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⟩

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

Domains

Dates and versions

Identifiers

Metadata

Cite

Export

Collections

Share