Distant Decimals of $$\pi $$ π : Formal Proofs of Some Algorithms Computing Them and Guarantees of Exact Computation

Autor: Yves Bertot, Laurent Théry, Laurence Rideau

Publikováno v: Journal of Automated Reasoning. 61:33-71

We describe how to compute very far decimals of $$\pi $$ and how to provide formal guarantees that the decimals we compute are correct. In particular, we report on an experiment where 1 million decimals of $$\pi $$ and the billionth hexadecimal (with

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::e386d2de14a80fa109335551749622e7
https://doi.org/10.1007/s10817-017-9444-2

A Machine-Checked Proof of the Odd Order Theorem

Autor: Alexey Solovyev, Jeremy Avigad, Andrea Asperti, Georges Gonthier, Stéphane Le Roux, Sidi Ould Biha, Ioana Pasca, Assia Mahboubi, Russell O'Connor, Enrico Tassi, François Garillot, Laurence Rideau, Cyril Cohen, Laurent Théry, Yves Bertot

Publikováno v: Interactive Theorem Proving ISBN: 9783642396335
ITP
ITP 2013, 4th Conference on Interactive Theorem Proving
ITP 2013, 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.163-179, ⟨10.1007/978-3-642-39634-2_14⟩

International audience; This paper reports on a six-year collaborative effort that cul- minated in a complete formalization of a proof of the Feit-Thompson Odd Order Theorem in the Coq proof assistant. The formalized proof is constructive, and relies

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8edf5c2f030660500c9cd44d945cff0e
http://hdl.handle.net/11585/185912

Rigorous Polynomial Approximation using Taylor Models in Coq

Autor: Micaela Mayero, Nicolas Brisebarre, Laurence Rideau, Mioara Joldes, Jean-Michel Muller, Ioana Pasca, Laurent Théry, Érik Martin-Dorel

Publikováno v: NASA Formal Methods 4th International Symposium, NFM 2012
Fourth NASA Formal Methods Symposium
Fourth NASA Formal Methods Symposium, NASA, Apr 2012, Norfolk, Virginia, United States. pp.15
Lecture Notes in Computer Science ISBN: 9783642288906
NASA Formal Methods

International audience; One of the most common and practical ways of representing a real function on machines is by using a polynomial approximation. It is then important to properly handle the error introduced by such an approximation. The purpose o

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::a2c3015ee8fc4578d9ab96a7e829277b
https://hal-ens-lyon.archives-ouvertes.fr/ensl-00653460v2/file/NFM2012_Brisebarre_et_al.pdf

Packaging Mathematical Structures

Autor: Georges Gonthier, Laurence Rideau, Assia Mahboubi, François Garillot

Publikováno v: Lecture Notes in Computer Science ISBN: 9783642033582
TPHOLs
Theorem Proving in Higher Order Logics
Theorem Proving in Higher Order Logics, 2009, Munich, Germany

International audience; This paper proposes generic design patterns to define and combine algebraic structures, using dependent records, coercions and type inference, inside the Coq system. This alternative to telescopes in particular allows multiple

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8ad5f3569898cb1d5314b9f33e3f616b
https://doi.org/10.1007/978-3-642-03359-9_23

Intelligent Computer Mathematics : 10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010, and 9th International Conference, MKM 2010, Paris, France, July 5-10, 2010. Proceedings

Autor: Serge Autexier, Jacques Calmet, David Delahaye, P.D.F. Ion, Laurence Rideau, Renaud Rioboo, Alan Sexton