{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:22:16Z","timestamp":1754482936311},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540602750"},{"type":"electronic","value":"9783540447849"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60275-5_65","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T18:05:41Z","timestamp":1330279541000},"page":"186-199","source":"Crossref","is-referenced-by-count":11,"title":["Floating point verification in HOL"],"prefix":"10.1007","author":[{"given":"John","family":"Harrison","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"Alan Baker. Transcendental Number Theory. Cambridge University Press, 1975.","DOI":"10.1017\/CBO9780511565977"},{"key":"13_CR2","unstructured":"C. T. Fike. Computer Evaluation of Mathematical Functions. Series in Automatic Computation. Prentice-Hall, 1968."},{"key":"13_CR3","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1145\/103162.103163","volume":"23","author":"D. Goldberg","year":"1991","unstructured":"David Goldberg. What every computer scientist should know about floating point arithmetic. ACM Computing Surveys, 23:5\u201348, 1991.","journal-title":"ACM Computing Surveys"},{"key":"13_CR4","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/BF01384233","volume":"5","author":"J. Harrison","year":"1994","unstructured":"John Harrison. Constructing the real numbers in HOL. Formal Methods in System Design, 5:35\u201359, 1994.","journal-title":"Formal Methods in System Design"},{"key":"13_CR5","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":"13_CR6","unstructured":"Tim Leonard. The HOL numeral library. Distributed with HOL system, 1993."},{"key":"13_CR7","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/BF01446522","volume":"120","author":"F. Lindemann","year":"1882","unstructured":"F. Lindemann. \u00fcber die Zahl \u03c0. Mathematische Annalen, 120:213\u2013225, 1882.","journal-title":"Mathematische Annalen"},{"key":"13_CR8","unstructured":"Val\u00e9rie M\u00e9nissier-Morain. Arithm\u00e9tique exacte, conception, algorithmique et performances d'une impl\u00e9mentation informatique en pr\u00e9cision arbitraire. Th\u00e8se, Universit\u00e9 Paris 7, December 1994."},{"key":"13_CR9","first-page":"52","volume-title":"volume 901 of Lecture Notes in Computer Science","author":"J. O'Leary","year":"1994","unstructured":"John O'Leary, Miriam Leeser, Jason Hickey, and Mark Aagaard. Non-restoring integer square root: A case study in design by principled optimization. In T. Kropf and R. Kumar, editors, Proceedings of the Second International Conference on Theorem Provers in Circuit Design (TPCD94): Theory, Practice and Experience, volume 901 of Lecture Notes in Computer Science, pages 52\u201371, Bad Herrenalb (Black Forest), Germany, 1994. Springer-Verlag."},{"key":"13_CR10","first-page":"97","volume-title":"volume 915 of Lecture Notes in Computer Science","author":"V. R. Pratt","year":"1995","unstructured":"Vaughan R. Pratt. Anatomy of the pentium bug. In ?, editor, Proceedings of the 5th International Joint Conference on the theory and practice of software development (TAPSOFT'95), volume 915 of Lecture Notes in Computer Science, pages 97\u2013107, Aarhus, Denmark, 1995. Springer-Verlag."},{"key":"13_CR11","unstructured":"E. Ya. Remez. Sur le calcul effectif des polynomes d'approximation. Comptes Rendus de l'Acad\u00e9mie des Sciences, pages 337\u2013340, 1934."},{"key":"13_CR12","first-page":"230","volume":"42","author":"A. M. Turing","year":"1936","unstructured":"A. M. Turing. On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society (2), 42:230\u2013265, 1936.","journal-title":"Proceedings of the London Mathematical Society (2)"},{"key":"13_CR13","doi-asserted-by":"crossref","first-page":"330","DOI":"10.1109\/TEC.1959.5222693","volume":"8","author":"J. Volder","year":"1959","unstructured":"J. Volder. The CORDIC trigonometric computing technique. IRE Transactions on Electronic Computers, 8:330\u2013334, 1959.","journal-title":"IRE Transactions on Electronic Computers"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"J. S. Walther. A unified algorithm for elementary functions. In Proceedings of the AFIPS Spring Joint Computer Conference, pages 379\u2013385, 1971.","DOI":"10.1145\/1478786.1478840"}],"container-title":["Lecture Notes in Computer Science","Higher Order Logic Theorem Proving and Its Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60275-5_65.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:57:19Z","timestamp":1605646639000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60275-5_65"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540602750","9783540447849"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-60275-5_65","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}