Published September 2007
| Version v1
Conference paper
Primality Proving with Elliptic Curves
Creators
Contributors
Others:
- Mathematical, Reasoning and Software (MARELLE) ; Centre Inria d'Université Côte d'Azur (CRISAM) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)
- Curves, Algebra, Computer Arithmetic, and so On (CACAO) ; INRIA Lorraine ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)
- Klaus Schneider and Jens Brandt
Description
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.
Abstract
International audienceAdditional details
Identifiers
- URL
- https://inria.hal.science/inria-00138382
- URN
- urn:oai:HAL:inria-00138382v2
Origin repository
- Origin repository
- UNICA