@inproceedings{a8009daf8ff54c15bb2ed8750ce962b4,
title = "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 formalization 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.",
author = "Bartzia, \{Evmorfia Iro\} and Strub, \{Pierre Yves\}",
year = "2014",
month = jan,
day = "1",
doi = "10.1007/978-3-319-08970-6\_6",
language = "English",
isbn = "9783319089690",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "77--92",
booktitle = "Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings",
note = "5th International Conference on Interactive Theorem Proving, ITP 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014 ; Conference date: 14-07-2014 Through 17-07-2014",
}