Home
Submit
Login
Register
Browse
By domain
News
By writing year
By publication type
By collection
ArXiv
News in HAL
Search
Simple search
Advanced search
Search by id
Help
Help
Bib2Hal
Information
Services
Subscribe
Export a publication list
Export raweb
Find your project / laboratory
HalTools : Bib2Hal
HalTools : Create your web page
HalTools : Manage your identities
version française
english version
inria-00138382, version 2
See detailed view
BibTeX
EndNote
TEI
RefWorks
%% inria-00138382, version 2 %% http://hal.inria.fr/inria-00138382/en/ @inproceedings{THERY:2007:INRIA-00138382:2, title = { {P}rimality {P}roving with {E}lliptic {C}urves}, author = {{T}h{\'e}ry, {L}aurent and {H}anrot, {G}uillaume}, abstract = {{E}lliptic curves are fascinating mathematical objects. {I}n this paper, we present the way they have been represented inside the {\sc {C}oq} system, and how we have proved that the classical composition law on the points is internal and gives them a group structure. {W}e then describe how having elliptic curves inside a prover makes it possible to derive a checker for proving the primality of natural numbers.}, language = {{E}nglish}, affiliation = {{MARELLE} - {INRIA} {S}ophia {A}ntipolis - {INRIA} - {CACAO} ({C}ourbes, {A}lg{\`e}bre, {C}alculs, {A}rithm{\'e}tique des {O}rdinateurs) - {INRIA} {L}orraine - {LORIA} - {CNRS} : {UMR}7503 - {INRIA} - {U}niversit{\'e} {H}enri {P}oincar{\'e} - {N}ancy {I} - {U}niversit{\'e} {N}ancy {II} - {I}nstitut {N}ational {P}olytechnique de {L}orraine }, booktitle = {{TPHOL} 2007 {T}heorem {P}roving in {H}igher {O}rder {L}ogics }, publisher = {{S}pringer-{V}erlag }, pages = {319-333 }, address = {{K}aiserslautern {G}ermany }, volume = {4732 }, editor = {{K}laus {S}chneider and {J}ens {B}randt }, series = {{LNCS} }, note = {}, audience = {international }, year = {2007}, URL = {http://hal.inria.fr/inria-00138382/en/}, URL = {http://hal.inria.fr/inria-00138382/PDF/paper.pdf}, }
%F inria-00138382, version 2 %0 Conference Proceedings %U http://hal.inria.fr/inria-00138382/en/ %2 INFO:INFO_CR;INFO:INFO_LO %T Primality Proving with Elliptic Curves %A Théry, Laurent %A Hanrot, Guillaume %A Théry, L. %A Hanrot, G. %A Théry L. et al %+ MARELLE - INRIA Sophia Antipolis - INRIA - CACAO (Courbes, Algèbre, Calculs, Arithmétique des Ordinateurs) - INRIA Lorraine - LORIA - CNRS : UMR7503 - INRIA - Université Henri Poincaré - Nancy I - Université Nancy II - Institut National Polytechnique de Lorraine %X 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. %G English %8 2007 %2 international %B TPHOL 2007 %2 Kaiserslautern %2 Germany %8 2007-09 %E Klaus Schneider and Jens Brandt %I Springer-Verlag %2 Theorem Proving in Higher Order Logics %V 4732 %N LNCS %P 319-333 %2 RR-6155
<?xml version="1.0" encoding="UTF-8"?> <listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML"> <listBibl type="inproceedings"><head>Peer-reviewed conferences/proceedings</head> <biblStruct type="inproceedings" xml:id="inria-00138382"><analytic> <author><persName><forename>Laurent</forename><surname>Théry</surname></persName> <affiliation> <orgName type="laboratory">INRIA Sophia Antipolis</orgName> <orgName type="team">MARELLE</orgName> <country>FR</country> <orgName type="institution">INRIA</orgName> </affiliation> </author> <author><persName><forename>Guillaume</forename><surname>Hanrot</surname></persName> <affiliation> <orgName type="laboratory">INRIA Lorraine - LORIA</orgName> <orgName type="team">CACAO (Courbes, Algèbre, Calculs, Arithmétique des Ordinateurs)</orgName> <country>FR</country> <orgName type="institution">CNRS : UMR7503</orgName> <orgName type="institution">INRIA</orgName> <orgName type="institution">Université Henri Poincaré - Nancy I</orgName> <orgName type="institution">Université Nancy II</orgName> <orgName type="institution">Institut National Polytechnique de Lorraine</orgName> </affiliation> </author> <title type="main" level="a">Primality Proving with Elliptic Curves</title></analytic><monogr><meeting>TPHOL 2007</meeting><imprint><publisher>Springer-Verlag</publisher><pubPlace><settlement>Kaiserslautern</settlement><country>Germany</country></pubPlace><biblScope type="publicationDate">2007</biblScope><biblScope type="vol">4732</biblScope><biblScope type="pp">319-333</biblScope></imprint></monogr><idno type="HALid">http://hal.inria.fr/inria-00138382/en/</idno><idno type="HALFile">http://hal.inria.fr/inria-00138382/PDF/paper.pdf</idno></biblStruct> </listBibl> </listBibl>
Application Error:
Database fatal error
Contact us
BibTeX EndNote TEI RefWorks