Using reflection to build efficient and certified decision procedures, TACS'97, pp.515-529, 1997. ,
DOI : 10.1007/BFb0014565
Single-threaded objects in ACL2, PADL'2001, pp.9-27, 2001. ,
Introduction to Groebner Bases, Gröbner Bases and Applications, pp.3-31, 1998. ,
DOI : 10.1007/978-3-642-59048-1_2
Cocoa: Computations in commutative algebra ,
Handbook of Elliptic and Hyperelliptic Curve Cryptography . Discrete Mathematics and Its Applications, 2005. ,
Gb: une procédure de décision pour le système Coq, JFLA'2004, pp.83-90, 2004. ,
An elementary proof of the group law for elliptic curves Excerpt from undergraduate thesis, 1998. ,
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
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
A Computational Approach to Pocklington Certificates in Type Theory, FLOPS, pp.97-113, 2006. ,
DOI : 10.1007/11737414_8
Proving Equalities in a Commutative Ring Done Right in Coq, TPHOLS'05, pp.98-113 ,
DOI : 10.1007/11541868_7
HOL Light: A tutorial introduction, FMCAD'96, pp.265-269, 1996. ,
DOI : 10.1007/BFb0031814
Complex quantifier elimination in HOL, TPHOLs 2001: Supplemental Proceedings, pp.159-174, 2001. ,
Formalized elliptic curve cryptography ,
Factoring integers with elliptic curves, Ann. Math, vol.126, pp.649-673, 1987. ,
Objective Caml Available at http://pauillac.inria.fr/ocaml, 1997. ,
PRIMO -primality proving ,
La primalité en temps polynomial, d'après Adleman, Huang, 2002. ,
The CAML Numbers Reference Manual, 1992. ,
The Arithmetic of Elliptic Curves, 1986. ,
The Coq Proof Assistant Reference Manual v7.2, 2002. ,
Proving the group law for elliptic curves formally, 2007. ,
route des Lucioles -BP 93 -06902 Sophia Antipolis Cedex (France) Unité de recherche INRIA Futurs : Parc Club Orsay Université -ZAC des Vignes 4, 2004. ,
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 ,
BP 105 -78153 Le Chesnay Cedex (France) http://www.inria.fr ISSN, pp.249-6399 ,