Skip to Main content Skip to Navigation
New interface
Conference papers

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.
Complete list of metadata

Cited literature [25 references]  Display  Hide  Download
Contributor : Guillaume Hanrot Connect in order to contact the contributor
Submitted on : Monday, April 9, 2007 - 7:50:19 AM
Last modification on : Saturday, June 25, 2022 - 10:57:50 PM
Long-term archiving on: : Tuesday, September 21, 2010 - 1:20:27 PM


Files produced by the author(s)


  • HAL Id : inria-00138382, version 2



Laurent Théry, Guillaume Hanrot. Primality Proving with Elliptic Curves. TPHOL 2007, Sep 2007, Kaiserslautern, Germany. pp.319-333. ⟨inria-00138382v2⟩



Record views


Files downloads