{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,30]],"date-time":"2026-07-30T14:27:16Z","timestamp":1785421636202,"version":"3.56.0"},"reference-count":13,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2002,9,1]],"date-time":"2002-09-01T00:00:00Z","timestamp":1030838400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,9,1]],"date-time":"2002-09-01T00:00:00Z","timestamp":1030838400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[2002,9]]},"DOI":"10.1023\/a:1021987403425","type":"journal-article","created":{"date-parts":[[2003,3,21]],"date-time":"2003-03-21T23:56:29Z","timestamp":1048290989000},"page":"225-252","source":"Crossref","is-referenced-by-count":17,"title":["A Proof of GMP Square Root"],"prefix":"10.1007","volume":"29","author":[{"given":"Yves","family":"Bertot","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nicolas","family":"Magaud","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Paul","family":"Zimmermann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"5109775_CR1","unstructured":"Bondyfalat, D.: Certification d'un algorithme de division pour les grands entiers, Unpublished, 2002."},{"key":"5109775_CR2","unstructured":"Coq development team, INRIA and LRI: The Coq Proof Assistant ReferenceManual, 2002. Available from http:\/\/coq.inria.fr\/doc\/main.html."},{"key":"5109775_CR3","doi-asserted-by":"crossref","unstructured":"Daumas, M., Rideau, L. and Th\u00e9ry, L.: A generic library for floating-point numbers and its application to exact computing, in Theorem Proving in Higher Order Logics: 14th International Conference, LNCS 2152, Springer-Verlag, September 2001.","DOI":"10.1007\/3-540-44755-5_13"},{"key":"5109775_CR4","unstructured":"Filli\u00e2tre, J.-C.: Preuve de programmes imp\u00e9ratifs en th\u00e9orie des types, Ph.D. thesis, Universit\u00e9 Paris-Sud, July 1999."},{"key":"5109775_CR5","unstructured":"Filli\u00e2tre, J.-C.: Verification of non-functional programs using interpretations in type theory, J. Funct. Programming (2001). English translation of (Filli\u00e2tre, 1999). To appear."},{"key":"5109775_CR6","unstructured":"Granlund, T.: The GNU Multiple Precision Arithmetic Library, 2002. Edition 4.0.1."},{"key":"5109775_CR7","doi-asserted-by":"crossref","unstructured":"Harrison, J.: A machine-checked theory of floating point arithmetic, in Theorem Proving in Higher Order Logics: 12th International Conference, LNCS 1690, Springer-Verlag, September 1999.","DOI":"10.1007\/3-540-48256-3_9"},{"key":"5109775_CR8","series-title":"Informatics Research Report","volume-title":"TPHOLs 2001: Supplemental Proceedings","author":"C. Jacobi","year":"2001","unstructured":"Jacobi, C.: Formal verification of a theory of IEEE rounding, in R. J. Boulton and P. B. Jackson (eds), TPHOLs 2001: Supplemental Proceedings, 2001. Informatics Research Report EDI-INFRR-0046, Univ. Edinburgh, UK."},{"key":"5109775_CR9","series-title":"NASA Technical Memorandum","volume-title":"Defining the IEEE-854 floating-point standard in PVS","author":"P. S. Miner","year":"1995","unstructured":"Miner, P. S.: Defining the IEEE-854 floating-point standard in PVS, NASA Technical Memorandum 110167, NASA Langley Research Center, Hampton, Virginia, June 1995."},{"key":"5109775_CR10","unstructured":"Paulin-Mohring, C.: Inductive definitions in the system Coq \u2013 rules and properties, in M. Bezem and J.-F. Groote (eds), Proceedings of the Conference Typed Lambda Calculi and Applications, Lecture Notes in Comput. Sci. 664, 1993. LIP Research Report 92-49."},{"issue":"1","key":"5109775_CR11","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1023\/A:1008669628911","volume":"14","author":"D. M. Russinoff","year":"1999","unstructured":"Russinoff, D. M.: A mechanically checked proof of IEEE compliance of AMD K5 floating point square-root microcode, Formal Methods in System Design\n14(1) (January 1999), 75\u2013125.","journal-title":"Formal Methods in System Design"},{"key":"5109775_CR12","unstructured":"Zimmermann, P.: Karatsuba square root, Technical Report 3805, INRIA, November 1999."},{"issue":"8","key":"5109775_CR13","doi-asserted-by":"crossref","first-page":"899","DOI":"10.1109\/12.295852","volume":"43","author":"D. Zuras","year":"1994","unstructured":"Zuras, D.: More on squaring and multiplying large integers, IEEE Trans. on Computers\n43(8) (1994), 899\u2013908.","journal-title":"IEEE Trans. on Computers"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1021987403425.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1021987403425\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1021987403425.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:36:31Z","timestamp":1749123391000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1021987403425"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,9]]},"references-count":13,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2002,9]]}},"alternative-id":["5109775"],"URL":"https:\/\/doi.org\/10.1023\/a:1021987403425","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2002,9]]}}}