{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,25]],"date-time":"2026-01-25T04:40:46Z","timestamp":1769316046780,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540664635","type":"print"},{"value":"9783540482567","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48256-3_9","type":"book-chapter","created":{"date-parts":[[2007,8,3]],"date-time":"2007-08-03T20:15:22Z","timestamp":1186172122000},"page":"113-130","source":"Crossref","is-referenced-by-count":68,"title":["A Machine-Checked Theory of Floating Point Arithmetic"],"prefix":"10.1007","author":[{"given":"John","family":"Harrison","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,9,17]]},"reference":[{"key":"9_CR1","doi-asserted-by":"publisher","first-page":"611","DOI":"10.1109\/32.24710","volume":"15","author":"M. Barratt","year":"1989","unstructured":"M. Barratt. Formal methods applied to a floating-point system. IEEE Transactions on Software Engineering, 15:611\u2013621, 1989.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"-Q2","key":"9_CR2","first-page":"1","volume":"1998","author":"M. Cornea-Hasegan","year":"1998","unstructured":"M. Cornea-Hasegan. Proving the IEEE correctness of iterative floating-point square root, divide and remainder algorithms. Intel Technology Journal, 1998-Q2:1\u201311, 1998. Available on the Web as http:\/\/developer.intel.com\/technology\/itj\/q21998\/articles\/art_3.htm .","journal-title":"Intel Technology Journal"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"M. A. Cornea-Hasegan, R. A. Golliver, and P. Markstein. Correctness proofs outline for Newton-Raphson based floating-point divide and square root algorithms. In Koren and Kornerup P. Kornerup, editors. Proceedings, 14th IEEE symposium on on computer arithmetic [10], pages 96\u2013105.","DOI":"10.1109\/ARITH.1999.762834"},{"key":"9_CR4","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1109\/2.689674","volume":"647","author":"C. Dulong","year":"1998","unstructured":"C. Dulong. The IA-64 architecture at work. IEEE Computer, 64(7):24\u201332, July 1998.","journal-title":"IEEE Computer"},{"key":"9_CR5","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1145\/103162.103163","volume":"23","author":"D. Goldberg","year":"1991","unstructured":"D. Goldberg. What every computer scientist should know about floating point arithmetic. ACM Computing Surveys, 23:5\u201348, 1991.","journal-title":"ACM Computing Surveys"},{"key":"9_CR6","unstructured":"M. J. C. Gordon and T. F. Melham. Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, 1993."},{"key":"9_CR7","volume-title":"Technical Report 428","author":"J. Harrison","year":"1997","unstructured":"J. Harrison. Floating point verification in HOL Light: The exponential function. Technical Report 428, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge, CB2 3QG, UK, 1997."},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"J. Harrison. Theorem Proving with the Real Numbers. Springer-Verlag, 1998. Revised version of author\u2019s PhD thesis.","DOI":"10.1007\/978-1-4471-1591-5"},{"key":"9_CR9","volume-title":"ANSI\/IEEE Standard 754-1985","author":"IEEE.","year":"1985","unstructured":"IEEE. Standard for binary floating point arithmetic. ANSI\/IEEE Standard 754-1985, The Institute of Electrical and Electronic Engineers, Inc., 345 East 47th Street, New York, NY 10017, USA, 1985."},{"key":"9_CR10","unstructured":"I. Koren and P. Kornerup, editors. Proceedings, 14th IEEE symposium on on computer arithmetic, Adelaide, Australia, 1999. IEEE Computer Society."},{"key":"9_CR11","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1147\/rd.341.0111","volume":"34","author":"P. W. Markstein","year":"1990","unstructured":"P. W. Markstein. Computation of elementary functions on the IBM RISC System\/6000 processor. IBM Journal of Research and Development, 34:111\u2013119, 1990.","journal-title":"IBM Journal of Research and Development"},{"key":"9_CR12","volume-title":"Technical memorandum 110167","author":"P. S. Miner","year":"1995","unstructured":"P. S. Miner. Defining the IEEE-854 floating-point standard in PVS. Technical memorandum 110167, NASA Langley Research Center, Hampton, VA 23681-0001, USA, 1995."},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"J-M. Muller. Elementary functions: Algorithms and Implementation. Birkh\u00e4user, 1997.","DOI":"10.1007\/978-1-4757-2646-6"},{"issue":"-vnQ1","key":"9_CR14","first-page":"1","volume":"1999","author":"J. O\u2019Leary","year":"1999","unstructured":"J. O\u2019Leary, X. Zhao, R. Gerth, and C-J. H. Seger. Formally verifying IEEE compliance of floating-point hardware. Intel Technology Journal, 1999-vnQ1:1\u201314, 1999. Available on the Web as http:\/\/developer.intel.com\/technology\/itj\/q11999\/articles\/art_5.htm .","journal-title":"Intel Technology Journal"},{"key":"9_CR15","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/0167-6423(83)90008-4","volume":"3","author":"L. C. Paulson","year":"1983","unstructured":"L. C. Paulson. A higher-order implementation of rewriting. Science of Computer Programming, 3:119\u2013149, 1983.","journal-title":"Science of Computer Programming"},{"key":"9_CR16","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1112\/S1461157000000176","volume":"1","author":"D. Rusinoff","year":"1998","unstructured":"D. Rusinoff. A mechanically checked proof of IEEE compliance of a registertransfer-level specification of the AMD-K7 floating-point multiplication, division, and square root instructions. LMS Journal of Computation and Mathematics, 1:148\u2013200, 1998. Available on the Web via http:\/\/www.onr.com\/user\/russ\/david\/k7-div-sqrt.html .","journal-title":"LMS Journal of Computation and Mathematics"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"S. Story and P. T. P. Tang. New algorithms for improved transcendental functions on IA-64. In Koren and Kornerup P. Kornerup, editors. Proceedings, 14th IEEE symposium on on computer arithmetic, Adelaide, Australia, 1999 [10], pages 4\u201311.","DOI":"10.1109\/ARITH.1999.762822"}],"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\/3-540-48256-3_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T03:45:58Z","timestamp":1737344758000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48256-3_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664635","9783540482567"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-48256-3_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1999]]}}}