{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:43:10Z","timestamp":1767926590937,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540334385","type":"print"},{"value":"9783540334392","type":"electronic"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"unspecified","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\/11737414_8","type":"book-chapter","created":{"date-parts":[[2006,3,15]],"date-time":"2006-03-15T11:54:37Z","timestamp":1142423677000},"page":"97-113","source":"Crossref","is-referenced-by-count":11,"title":["A Computational Approach to Pocklington Certificates in Type Theory"],"prefix":"10.1007","author":[{"given":"Benjamin","family":"Gr\u00e9goire","sequence":"first","affiliation":[]},{"given":"Laurent","family":"Th\u00e9ry","sequence":"additional","affiliation":[]},{"given":"Benjamin","family":"Werner","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","unstructured":"Elliptic Curve Method Library, \n                      \n                        http:\/\/www.loria.fr\/~zimmerma\/records\/ecmnet.html"},{"key":"8_CR2","unstructured":"GNU Multiple Precision Arithmetic Library, \n                      \n                        http:\/\/www.swox.com\/gmp\/"},{"issue":"3","key":"8_CR3","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1023\/A:1015761529444","volume":"28","author":"H. Barendregt","year":"2002","unstructured":"Barendregt, H., Barendsen, E.: A Computational Approach to Pocklington Certificates 113. Autarkic computations in formal proofs. J. Autom. Reasoning\u00a028(3), 321\u2013336 (2002)","journal-title":"J. Autom. Reasoning"},{"key":"8_CR4","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 2m \u00b1 1. Mathematics of Computation\u00a029, 620\u2013647 (1975)","journal-title":"Mathematics of Computation"},{"key":"8_CR5","unstructured":"Brillhart, J., Lehmer, D.H., Selfridge, J.L., Tuckerman, B., Wagstaff Jr., S.S.: Factorizations of bn \u00b1 1. In: Contemporary Mathematics, vol.\u00a022. American Mathematical Society, Providence (1983); b = 2, 3, 5, 6, 7, 10, 11, 12 up to high powers"},{"issue":"1\/2","key":"8_CR6","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":"8_CR7","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)"},{"issue":"3","key":"8_CR8","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":"8_CR9","series-title":"Graduate Texts in Mathematics","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-0041-0","volume-title":"Algebra","author":"S. Lang","year":"2002","unstructured":"Lang, S.: Algebra, 3rd edn. Graduate Texts in Mathematics, vol.\u00a0211. Springer, New York (2002)","edition":"3"},{"key":"8_CR10","unstructured":"Pocklington, H.C.: The determination of the prime or composite nature of large numbers by Fermat\u2019s theorem\u00a018, 29\u201330 (1914)"}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11737414_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,12]],"date-time":"2019-03-12T03:44:22Z","timestamp":1552362262000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11737414_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540334385","9783540334392"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/11737414_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}