{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,8]],"date-time":"2025-05-08T23:04:20Z","timestamp":1746745460101},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540745907"},{"type":"electronic","value":"9783540745914"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74591-4_24","type":"book-chapter","created":{"date-parts":[[2007,8,22]],"date-time":"2007-08-22T10:49:52Z","timestamp":1187779792000},"page":"319-333","source":"Crossref","is-referenced-by-count":12,"title":["Primality Proving with Elliptic Curves"],"prefix":"10.1007","author":[{"given":"Laurent","family":"Th\u00e9ry","sequence":"first","affiliation":[]},{"given":"Guillaume","family":"Hanrot","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/BFb0014565","volume-title":"Theoretical Aspects of Computer Software","author":"S. Boutin","year":"1997","unstructured":"Boutin, S.: Using Reflection to Build Efficient and Certified Decision Procedures. In: Ito, T., Abadi, M. (eds.) TACS 1997. LNCS, vol.\u00a01281, pp. 515\u2013529. Springer, Heidelberg (1997)"},{"key":"24_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1007\/3-540-44566-8","volume-title":"Practical Aspects of Declarative Languages","author":"R.S. Boyer","year":"2001","unstructured":"Boyer, R.S., Moore, J.S.: Single-threaded objects in ACL2. In: Ramakrishnan, I.V. (ed.) PADL 2001. LNCS, vol.\u00a01990, pp. 9\u201327. Springer, Heidelberg (2001)"},{"key":"24_CR3","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1017\/CBO9780511565847.003","volume-title":"Gr\u00f6bner Bases and Applications","author":"B. Buchberger","year":"1998","unstructured":"Buchberger, B.: Introduction to Gr\u00f6bner Bases. In: Buchberger, B., Winkler, F. (eds.) Gr\u00f6bner Bases and Applications, pp. 3\u201331. Cambridge University Press, Cambridge (1998)"},{"key":"24_CR4","unstructured":"Capani, A., Niesi, G., Robbiano, L.: Cocoa: Computations in commutative algebra, available at http:\/\/cocoa.dima.unige.it\/"},{"key":"24_CR5","doi-asserted-by":"crossref","unstructured":"Cohen, H., Frey, G.: Handbook of Elliptic and Hyperelliptic Curve Cryptography. Discrete Mathematics and Its Applications. Chapman & Hall \/ CRC (2005)","DOI":"10.1201\/9781420034981"},{"key":"24_CR6","unstructured":"Cr\u00e9ci, J., Pottier, L.: Gb: une proc\u00e9dure de d\u00e9cision pour le syst\u00e8me Coq. In: JFLA 2004, pp. 83\u201390 (2004)"},{"key":"24_CR7","unstructured":"Friedl, S.: An elementary proof of the group law for elliptic curves. Excerpt from undergraduate thesis, Regensburg (1998), available at http:\/\/www.labmath.uqam.ca\/~friedl\/papers\/AAELLIPTIC.PDF"},{"key":"24_CR8","doi-asserted-by":"crossref","unstructured":"Goldwasser, S., Kilian, J.: Almost all primes can be quickly certified. In: Proceedings of the 18th STOC, pp. 316\u2013329 (1986)","DOI":"10.1145\/12130.12162"},{"key":"24_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/11814771_36","volume-title":"Automated Reasoning","author":"B. Gr\u00e9goire","year":"2006","unstructured":"Gr\u00e9goire, B., Th\u00e9ry, L.: A Purely Functional Library for Modular Arithmetic and its Application to Certifying Large Prime Numbers. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 423\u2013437. Springer, Heidelberg (2006)"},{"key":"24_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/11737414_8","volume-title":"Functional and Logic Programming","author":"B. Gr\u00e9goire","year":"2006","unstructured":"Gr\u00e9goire, B., Th\u00e9ry, L., Werner, B.: A Computational Approach to Pocklington Certificates in Type Theory. In: Hagiya, M., Wadler, P. (eds.) FLOPS 2006. LNCS, vol.\u00a03945, pp. 97\u2013113. Springer, Heidelberg (2006)"},{"key":"24_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1007\/11541868_7","volume-title":"Theorem Proving in Higher Order Logics","author":"B. Gr\u00e9goire","year":"2005","unstructured":"Gr\u00e9goire, B., Mahboubi, A.: Proving ring equalities done right in Coq. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 98\u2013113. Springer, Heidelberg (2005)"},{"key":"24_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"Formal Methods in Computer-Aided Design","author":"J. Harrison","year":"1996","unstructured":"Harrison, J.: HOL light: A tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 265\u2013269. Springer, Heidelberg (1996)"},{"key":"24_CR13","series-title":"Lecture Notes in Computer Science","first-page":"159","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"2001","unstructured":"Harrison, J.: Complex quantifier elimination in HOL. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol.\u00a02152, pp. 159\u2013174. Springer, Heidelberg (2001)"},{"key":"24_CR14","unstructured":"Hurd, J.: Formalized elliptic curve cryptography, available at http:\/\/www.cl.cam.ac.uk\/~jeh1004\/research\/talks\/elliptic-talk.pdf"},{"key":"24_CR15","doi-asserted-by":"publisher","first-page":"649","DOI":"10.2307\/1971363","volume":"126","author":"H.W. Lenstra Jr.","year":"1987","unstructured":"Lenstra Jr., H.W.: Factoring integers with elliptic curves. Ann. Math.\u00a0126, 649\u2013673 (1987)","journal-title":"Ann. Math."},{"key":"24_CR16","unstructured":"Leroy, X.: Objective Caml (1997), available at http:\/\/pauillac.inria.fr\/ocaml\/"},{"key":"24_CR17","unstructured":"Martin, M.: PRIMO - primality proving, available at http:\/\/www.ellipsa.net\/"},{"key":"24_CR18","unstructured":"Morain, F.: Certificate for (((((((((23\u2009+\u20093)3\u2009+\u200930)3\u2009+\u20096)3\u2009+\u200980)3\u2009+\u200912)3\u2009+\u2009450)3\u2009+\u2009894)3\u2009+\u20093636)3\u2009+\u200970756)3\u2009+\u200997220, available at http:\/\/www.lix.polytechnique.fr\/Labo\/Francois.Morain"},{"key":"24_CR19","unstructured":"Morain, F.: La primalit\u00e9 en temps polynomial, d\u2019apr\u00e8s Adleman, Huang; Agrawal, Kayal, Saxena. S\u00e9minaire Bourbaki, 3(55) (2002)"},{"key":"24_CR20","unstructured":"M\u00e9nissier-Morain, V.: The CAML Numbers Reference Manual. Technical Report 141, INRIA (1992)"},{"key":"24_CR21","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-1920-8","volume-title":"The Arithmetic of Elliptic Curves","author":"J.H. Silverman","year":"1986","unstructured":"Silverman, J.H.: The Arithmetic of Elliptic Curves. Springer, Heidelberg (1986)"},{"key":"24_CR22","unstructured":"The COQ development team: The Coq Proof Assistant Reference Manual v7.2. Technical Report 255, INRIA (2002), available at http:\/\/coq.inria.fr\/doc"},{"key":"24_CR23","unstructured":"Th\u00e9ry, L.: Proving the group law for elliptic curves formally. Technical Report 330, INRIA (2007)"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74591-4_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:28:10Z","timestamp":1619504890000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74591-4_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540745907","9783540745914"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74591-4_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}