{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:37:10Z","timestamp":1725557830642},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540406648"},{"type":"electronic","value":"9783540451303"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/10930755_20","type":"book-chapter","created":{"date-parts":[[2006,6,19]],"date-time":"2006-06-19T11:27:09Z","timestamp":1150716429000},"page":"304-318","source":"Crossref","is-referenced-by-count":3,"title":["Proving Pearl: Knuth\u2019s Algorithm for Prime Numbers"],"prefix":"10.1007","author":[{"given":"Laurent","family":"Th\u00e9ry","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","unstructured":"Agrawal, M., Kayal, N., Saxena, N.: PRIMES is in P. Preprint (2002), Available at http:\/\/www.cse.iit.ac.in\/primality.pdf"},{"key":"20_CR2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-22343-7","volume-title":"Proofs from THE BOOK","author":"M. Aigner","year":"1998","unstructured":"Aigner, M., Ziegler, G.M.: Proofs from THE BOOK. Springer, Heidelberg (1998)"},{"key":"20_CR3","unstructured":"Almeida, J.C., Th\u00e9ry, L.: Correctness of the RSA algorithm. Coq contribution (1999), Available at http:\/\/coq.inria.fr\/contribs\/summary.html"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Magaud, N., Zimmermann, P.: A GMP program computing square roots and its proof within Coq. Journal of Automated Reasoning\u00a029(3-4) (2002)","DOI":"10.1023\/A:1021987403425"},{"issue":"1","key":"20_CR5","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), 55\u201370 (2001)","journal-title":"Journal of Symbolic Computation"},{"key":"20_CR6","first-page":"194","volume":"5","author":"P. Erd\u00f6s","year":"1932","unstructured":"Erd\u00f6s, P.: Beweis eines Satzes von Tschebyschef. Acta Scientifica Mathematica\u00a05, 194\u2013198 (1932)","journal-title":"Acta Scientifica Mathematica"},{"key":"20_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/3-540-48167-2_6","volume-title":"Types for Proofs and Programs","author":"J.-C. Filli\u00e2tre","year":"1999","unstructured":"Filli\u00e2tre, J.-C.: Proof of Imperative Programs in Type Theory. In: Altenkirch, T., Naraschewski, W., Reus, B. (eds.) TYPES 1998. LNCS, vol.\u00a01657, p. 78. Springer, Heidelberg (1999)"},{"key":"20_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"186","DOI":"10.1007\/3-540-60275-5_65","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"J. Harrison","year":"1995","unstructured":"Harrison, J.: Floating Point Verification in HOL. In: Schubert, E.T., Alves-Foss, J., Windley, P. (eds.) HUG 1995. LNCS, vol.\u00a0971, pp. 186\u2013199. Springer, Heidelberg (1995)"},{"issue":"3","key":"20_CR9","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. Journal of Automated Reasoning\u00a021(3), 279\u2013294 (1998)","journal-title":"Journal of Automated Reasoning"},{"issue":"10","key":"20_CR10","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An Axiomatic Basis for Computer Programming. Communication of the ACM\u00a012(10), 576\u2013580, 583 (1969)","journal-title":"Communication of the ACM"},{"key":"20_CR11","unstructured":"Hurd, J.: Formal Verification of Probabilistic Algorithms. Phd Thesis, University of Cambridge (2002)"},{"key":"20_CR12","first-page":"147","volume-title":"The Art of Computer Programming: Fundamental Algorithms","author":"D.E. Knuth","year":"1997","unstructured":"Knuth, D.E.: The Art of Computer Programming: Fundamental Algorithms, pp. 147\u2013149. Addison-Wesley, Reading (1997)"},{"key":"20_CR13","unstructured":"PCoq. A Graphical User-interface to Coq, Available at http:\/\/www-sop.inria.fr\/lemme\/pcoq\/"},{"key":"20_CR14","series-title":"Automated reasoning series","volume-title":"Automated development of fundamental mathematical theories","author":"A. Quaife","year":"1992","unstructured":"Quaife, A.: Automated development of fundamental mathematical theories. Automated reasoning series, vol.\u00a02. Kluwer, Dordrecht (1992)"},{"key":"20_CR15","unstructured":"Slinko, A.: Number Theory. Tutorial 5: Bertrand\u2019s Postulate, Available at http:\/\/matholymp.com\/tutorials\/bertrand.pdf"},{"key":"20_CR16","unstructured":"Th\u00e9ry, L.: A Tour of Formal Verification with Coq: Knuth\u2019s Algorithm for Prime Numbers. Research Report 4600, INRIA (2002)"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10930755_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,19]],"date-time":"2019-04-19T08:24:01Z","timestamp":1555662241000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10930755_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540406648","9783540451303"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/10930755_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}