{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,8]],"date-time":"2025-05-08T23:04:13Z","timestamp":1746745453376},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540371878"},{"type":"electronic","value":"9783540371885"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11814771_36","type":"book-chapter","created":{"date-parts":[[2006,10,5]],"date-time":"2006-10-05T15:44:21Z","timestamp":1160063061000},"page":"423-437","source":"Crossref","is-referenced-by-count":13,"title":["A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers"],"prefix":"10.1007","author":[{"given":"Benjamin","family":"Gr\u00e9goire","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laurent","family":"Th\u00e9ry","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"36_CR1","unstructured":"GNU Multiple Precision Arithmetic Library, \n                    \n                      http:\/\/www.swox.com\/gmp\/"},{"issue":"3","key":"36_CR2","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1023\/A:1015761529444","volume":"28","author":"H. Barendregt","year":"2002","unstructured":"Barendregt, H., Barendsen, E.: Autarkic computations in formal proofs. J. Autom. Reasoning\u00a028(3), 321\u2013336 (2002)","journal-title":"J. Autom. Reasoning"},{"issue":"3-4","key":"36_CR3","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1023\/A:1021987403425","volume":"29","author":"Y. Bertot","year":"2002","unstructured":"Bertot, Y., Magaud, N., Zimmermann, P.: A proof of GMP square root. Journal of Automated Reasoning\u00a029(3-4), 225\u2013252 (2002)","journal-title":"Journal of Automated Reasoning"},{"key":"36_CR4","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":"36_CR5","first-page":"620","volume":"29","author":"J. Brillhart","year":"1975","unstructured":"Brillhart, J., Lehmer, D.H., Selfridge, J.L.: New primality criteria and factorizations of 2\n                    m\n                   \u00b11. Mathematics of Computation\u00a029, 620\u2013647 (1975)","journal-title":"Mathematics of Computation"},{"key":"36_CR6","unstructured":"Burnikel, C., Ziegler, J.: Fast recursive division. Technical Report MPI-I-98-1-022, Max-Planck-Institut (1998)"},{"issue":"1\/2","key":"36_CR7","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1006\/jsco.2001.0457","volume":"32","author":"O. Caprotti","year":"2001","unstructured":"Caprotti, O., Oostdijk, M.: Formal and efficient primality proofs by use of computer algebra oracles. Journal of Symbolic Computation\u00a032(1\/2), 55\u201370 (2001)","journal-title":"Journal of Symbolic Computation"},{"key":"36_CR8","doi-asserted-by":"crossref","unstructured":"Crandall, R., Fagin, B.: Discrete weighted transforms and large-integer arithmetic. \u00a062(205), 305\u2013324 (1994)","DOI":"10.2307\/2153411"},{"key":"36_CR9","unstructured":"Gonthier, G.: A computer-checked proof of the Four Colour Theorem. Technical report, available at \n                    \n                      http:\/\/research.microsoft.com\/~gonthier\/4colproof.pdf"},{"key":"36_CR10","first-page":"235","volume-title":"International Conference on Functional Programming 2002","author":"B. Gr\u00e9goire","year":"2002","unstructured":"Gr\u00e9goire, B., Leroy, X.: A compiled implementation of strong reduction. In: International Conference on Functional Programming 2002, pp. 235\u2013246. ACM Press, New York (2002)"},{"key":"36_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"36_CR12","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)"},{"issue":"3","key":"36_CR13","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1023\/A:1006023127567","volume":"21","author":"J. Harrison","year":"1998","unstructured":"Harrison, J., Th\u00e9ry, L.: A skeptic\u2019s approach to combining HOL and Maple. J. Autom. Reasoning\u00a021(3), 279\u2013294 (1998)","journal-title":"J. Autom. Reasoning"},{"key":"36_CR14","first-page":"595","volume":"7","author":"A.A. Karatsuba","year":"1963","unstructured":"Karatsuba, A.A., Ofman, Y.: Multiplication of Many-Digital Numbers by Automatic Computers. Soviet Physics-Doklad\u00a07, 595\u2013596 (1963)","journal-title":"Soviet Physics-Doklad"},{"key":"36_CR15","unstructured":"Leroy, X.: Objective Caml (1997), available at \n                    \n                      http:\/\/pauillac.inria.fr\/ocaml\/"},{"key":"36_CR16","unstructured":"M\u00e9nissier-Morain, V.: The CAML Numbers Reference Manual. Technical Report 141, INRIA (1992)"},{"key":"36_CR17","unstructured":"Nipkow, T., Bauer, G., Schultz, P.: Flyspeck I: Tame Graphs. Technical report, available at \n                    \n                      http:\/\/www.in.tum.de\/nipkow\/pubs\/Flyspeck\/"},{"key":"36_CR18","unstructured":"The Coq development team. The Coq Proof Assistant Reference Manual v7.2. Technical Report 255, INRIA (2002), available at \n                    \n                      http:\/\/coq.inria.fr\/doc"},{"key":"36_CR19","unstructured":"Zimmermann, P.: Karatsuba square root. Research Report 3805, INRIA (1999)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11814771_36","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T23:33:11Z","timestamp":1558308791000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11814771_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540371878","9783540371885"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/11814771_36","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}