S. Boutin, Using reflection to build efficient and certified decision procedures, TACS'97, pp.515-529, 1997.
DOI : 10.1007/BFb0014565

S. Robert, J. Boyer, and . Strother-moore, Single-threaded objects in ACL2, PADL'2001, pp.9-27, 2001.

B. Buchberger, Introduction to Groebner Bases, Gröbner Bases and Applications, pp.3-31, 1998.
DOI : 10.1007/978-3-642-59048-1_2

A. Capani, G. Niesi, and L. Robbiano, Cocoa: Computations in commutative algebra

H. Cohen and G. Frey, Handbook of Elliptic and Hyperelliptic Curve Cryptography . Discrete Mathematics and Its Applications, 2005.

J. Créci and L. Pottier, Gb: une procédure de décision pour le système Coq, JFLA'2004, pp.83-90, 2004.

S. Friedl, An elementary proof of the group law for elliptic curves Excerpt from undergraduate thesis, 1998.

S. Goldwasser and J. Kilian, Almost all primes can be quickly certified, Proceedings of the eighteenth annual ACM symposium on Theory of computing , STOC '86, pp.316-329, 1986.
DOI : 10.1145/12130.12162

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

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

B. Grégoire and A. Mahboubi, Proving Equalities in a Commutative Ring Done Right in Coq, TPHOLS'05, pp.98-113
DOI : 10.1007/11541868_7

J. Harrison, HOL Light: A tutorial introduction, FMCAD'96, pp.265-269, 1996.
DOI : 10.1007/BFb0031814

J. Harrison, Complex quantifier elimination in HOL, TPHOLs 2001: Supplemental Proceedings, pp.159-174, 2001.

J. Hurd, Formalized elliptic curve cryptography

W. Hendrik and . Lenstra-jr, Factoring integers with elliptic curves, Ann. Math, vol.126, pp.649-673, 1987.

X. Leroy, Objective Caml Available at http://pauillac.inria.fr/ocaml, 1997.

M. Martin, PRIMO -primality proving

F. Morain, La primalité en temps polynomial, d'après Adleman, Huang, 2002.

V. Ménissier-morain, The CAML Numbers Reference Manual, 1992.

J. H. Silverman, The Arithmetic of Elliptic Curves, 1986.

C. The and . Team, The Coq Proof Assistant Reference Manual v7.2, 2002.

L. Théry, Proving the group law for elliptic curves formally, 2007.

I. Unité-de-recherche-inria-sophia and . Antipolis, route des Lucioles -BP 93 -06902 Sophia Antipolis Cedex (France) Unité de recherche INRIA Futurs : Parc Club Orsay Université -ZAC des Vignes 4, 2004.

I. Unité-de-recherche and . Lorraine, Technopôle de Nancy-Brabois -Campus scientifique 615, rue du Jardin Botanique -BP 101 -54602 Villers-lès-Nancy Cedex (France) Unité de recherche INRIA Rennes : IRISA, Campus universitaire de Beaulieu -35042 Rennes Cedex (France) Unité de recherche INRIA Rhône-Alpes : 655, avenue de l'Europe -38334 Montbonnot Saint-Ismier (France) Unité de recherche INRIA Rocquencourt, Domaine de Voluceau -Rocquencourt -BP 105 -78153 Le Chesnay Cedex

I. De-voluceau-rocquencourt, BP 105 -78153 Le Chesnay Cedex (France) http://www.inria.fr ISSN, pp.249-6399