Primality Proving with Elliptic Curves

Laurent Théry 1 Guillaume Hanrot 2
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
2 CACAO - Curves, Algebra, Computer Arithmetic, and so On
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Elliptic curves are fascinating mathematical objects. In this paper, we present the way they have been represented inside the {\sc Coq} system, and how we have proved that the classical composition law on the points is internal and gives them a group structure. We then describe how having elliptic curves inside a prover makes it possible to derive a checker for proving the primality of natural numbers.
Type de document :
Communication dans un congrès
Klaus Schneider and Jens Brandt. TPHOL 2007, Sep 2007, Kaiserslautern, Germany. Springer-Verlag, 4732, pp.319-333, 2007, LNCS; Theorem Proving in Higher Order Logics
Liste complète des métadonnées

https://hal.inria.fr/inria-00138382
Contributeur : Guillaume Hanrot <>
Soumis le : lundi 9 avril 2007 - 07:50:19
Dernière modification le : mardi 25 octobre 2016 - 16:57:56
Document(s) archivé(s) le : mardi 21 septembre 2010 - 13:20:27

Fichier

paper.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00138382, version 2

Collections

Citation

Laurent Théry, Guillaume Hanrot. Primality Proving with Elliptic Curves. Klaus Schneider and Jens Brandt. TPHOL 2007, Sep 2007, Kaiserslautern, Germany. Springer-Verlag, 4732, pp.319-333, 2007, LNCS; Theorem Proving in Higher Order Logics. <inria-00138382v2>

Partager

Métriques

Consultations de
la notice

1298

Téléchargements du document

297