Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions, Theoretical Computer Science, 2004.
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/hal-00344237

J. Zur-gathen and J. Gerhard, Modern Computer Algebra, 2003.
DOI : 10.1017/CBO9781139856065

G. Gonthier, Formal Proof?The Four-Color Theorem. Notices of the, pp.1382-1393, 2008.

G. Gonthier and A. Mahboubi, A Small Scale Reflection Extension for the Coq system, INRIA, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00258384

G. Gonthier and S. L. Roux, An Ssreflect Tutorial, INRIA, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00407778

B. Grégoire and L. Théry, A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers
DOI : 10.1007/11814771_36

B. Grégoire, L. Théry, and B. Werner, A Computational Approach to Pocklington Certificates in Type Theory, Functional and Logic Programming, pp.97-113, 2006.
DOI : 10.1007/11737414_8

K. Hensel, Neue Grundlagen der Arithmetik Journal für die reine und angewandte Mathematik (Crelle's Journal), pp.51-84, 1904.

G. Huet, G. Kahn, and C. Paulin-mohring, The Coq proof assistant: a tutorial: version 8, 2010.

W. Kahan, A Test for Correctly Rounded SQRT, 1996.

V. Lefèvre and J. M. Muller, Worst cases for correct rounding of the elementary functions in double precision, Proceedings 15th IEEE Symposium on Computer Arithmetic. ARITH-15 2001, pp.111-118, 2001.
DOI : 10.1109/ARITH.2001.930110

A. K. Lenstra, J. Lenstra, H. W. Lovász, and L. , Factoring polynomials with rational coefficients, Mathematische Annalen, vol.32, issue.4, pp.515-534, 1982.
DOI : 10.1007/BF01457454
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.310.318

R. M. Mcconnell, K. Mehlhorn, S. Näher, and P. Schweitzer, Certifying algorithms, Computer Science Review, vol.5, issue.2, 2010.
DOI : 10.1016/j.cosrev.2010.09.009

J. M. Muller, Elementary Functions, Algorithms and Implementation, 2006.
URL : https://hal.archives-ouvertes.fr/ensl-00000008

M. Parks, Number-Theoretic Test Generation for Directed Rounding, 14th IEEE Symposium on Computer Arithmetic, pp.241-248, 1999.
DOI : 10.1109/12.863034
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.645.6373

D. Stehlé, Algorithmique de la réduction des réseaux et application à la recherche de pires cas pour l'arrondi des fonctions mathématiques, 2005.

D. Stehlé, On the Randomness of Bits Generated by Sufficiently Smooth Functions, 7th International Symposium, ANTS-VII, pp.257-274, 2006.
DOI : 10.1007/11792086_19

D. Stehlé, V. Lefèvre, and P. Zimmermann, Searching worst cases of a one-variable function using lattice reduction, IEEE Transactions on Computers, vol.54, issue.3, pp.340-346, 2005.
DOI : 10.1109/TC.2005.55

L. Théry and G. Hanrot, Primality Proving with Elliptic Curves, Theorem Proving in Higher Order Logics, pp.319-333, 2007.
DOI : 10.1007/978-3-540-74591-4_24