| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
A Formal Library for Elliptic Curves in the Coq Proof Assistant
Abstract : A preliminary step towards the verification of elliptic curve cryptographic algorithms is the development of formal libraries with the corresponding mathematical theory. In this paper we present a formaliza-tion of elliptic curves theory, in the SSReflect extension of the Coq proof assistant. Our central contribution is a library containing many of the objects and core properties related to elliptic curve theory. We demonstrate the applicability of our library by formally proving a non-trivial property of elliptic curves: the existence of an isomorphism between a curve and its Picard group of divisors.
Cited literature [18 references]
https://hal.inria.fr/hal-01102288
Contributor : Bruno Blanchet <>
Submitted on : Sunday, October 4, 2015 - 11:48:29 PM
Last modification on : Friday, May 25, 2018 - 12:02:06 PM
Long-term archiving on: : Tuesday, January 5, 2016 - 10:19:13 AM
Contributor : Bruno Blanchet <>
Submitted on : Sunday, October 4, 2015 - 11:48:29 PM
Last modification on : Friday, May 25, 2018 - 12:02:06 PM
Long-term archiving on: : Tuesday, January 5, 2016 - 10:19:13 AM
File
A-Formal-Library-for-Elliptic-...
Files produced by the author(s)