{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:10Z","timestamp":1761611170981},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540638889"},{"type":"electronic","value":"9783540696612"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/bfb0000475","type":"book-chapter","created":{"date-parts":[[2005,10,5]],"date-time":"2005-10-05T10:30:36Z","timestamp":1128508236000},"page":"246-260","source":"Crossref","is-referenced-by-count":32,"title":["Floating point verification in HOL light: The exponential function"],"prefix":"10.1007","author":[{"given":"John","family":"Harrison","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,9,7]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","first-page":"611","DOI":"10.1109\/32.24710","volume":"15","author":"M. Barratt","year":"1989","unstructured":"Barratt, M. (1989) Formal methods applied to a floating-point system. IEEE Transactions on Software Engineering, 15, 611\u2013621.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"17_CR2","volume-title":"Real algebraic and semi-algebraic sets","author":"R. Benedetti","year":"1990","unstructured":"Benedetti, R. and Risler, J.-J. (1990) Real algebraic and semi-algebraic sets. Hermann, Paris."},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Brock, B., Kaufmann, M., and Moore, J. S. (1996) ACL2 theorems about commercial microprocessors. See Srivas and Camilleri (1996), pp. 275\u2013293.","DOI":"10.1007\/BFb0031816"},{"key":"17_CR4","series-title":"Volume 1125 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1007\/BFb0105402","volume-title":"Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs'96","author":"B. Dutertre","year":"1996","unstructured":"Dutertre, B. (1996) Elements of mathematical analysis in PVS. See von Wright, Grundy, and Harrison (1996).(1996), pp. 141\u2013156."},{"key":"17_CR5","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1145\/103162.103163","volume":"23","author":"D. Goldberg","year":"1991","unstructured":"Goldberg, D. (1991) What every computer scientist should know about floating point arithmetic. ACM Computing Surveys, 23, 5\u201348.","journal-title":"ACM Computing Surveys"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Gordon, M. J. C. (1989) Mechanizing programming logics in higher order logic. In Birtwistle, G. and Subrahmanyam, P. A. (eds.), Current Trends in Hardware Verification and Automated Theorem Proving, pp. 387\u2013439. Springer-Verlag.","DOI":"10.1007\/978-1-4612-3658-0_10"},{"key":"17_CR7","unstructured":"Gordon, M. J. C. and Melham, T. F. (1993) Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press."},{"key":"17_CR8","unstructured":"Harrison, J. (1996a) HOL light: A tutorial introduction. See Srivas and Camilleri (1996), pp. 265\u2013269."},{"key":"17_CR9","unstructured":"Harrison, J. (1996b) Theorem proving with the real numbers. Technical Report 408, University of Cambridge Computer Laboratory."},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Harrison, J. (1997a) Floating point verification in HOL Light: The exponential function. Technical Report 428, University of Cambridge Computer Laboratory.","DOI":"10.1007\/BFb0000475"},{"key":"17_CR11","series-title":"Volume 1275 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/BFb0028391","volume-title":"Theorem Proving in Higher Order Logics: 10th International Conference, TPHOLs'97","author":"J. Harrison","year":"1997","unstructured":"Harrison, J. (1997b) Verifying the accuracy of polynomial approximations in HOL. In Gunter, E. L. and Felty, A. (eds.), Theorem Proving in Higher Order Logics: 10th International Conference, TPHOLs'97, Volume 1275 of Lecture Notes in Computer Science, Murray Hill, NJ, pp. 137\u2013152. Springer-Verlag."},{"key":"17_CR12","volume-title":"Technical memorandum 110167","author":"P. S. Miner","year":"1995","unstructured":"Miner, P. S. (1995) Defining the IEEE-854 floating-point standard in PVS. Technical memorandum 110167, NASA Langley Research Center, Hampton, VA 23681-0001, USA."},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"Miner, P. S. and Leathrum, J. F. (1996) Verification of IEEE compliant subtractive division algorithms. See Srivas and Camilleri (1996), pp. 64\u201378.","DOI":"10.1007\/BFb0031800"},{"key":"17_CR14","unstructured":"Moore, J. S., Lynch, T., and Kaufmann, M. (1996) A mechanically checked proof of the correctness of the kernel of the AMD5K86 floating-point division algorithm. Unpublished; available on the Web as http:\/\/devil.ece.utexas.edu:80\/\u223clynch\/divide\/divide.html."},{"key":"17_CR15","first-page":"97","volume-title":"Volume 915 of Lecture Notes in Computer Science","author":"V. R. Pratt","year":"1995","unstructured":"Pratt, V. R. (1995) Anatomy of the Pentium bug. In Mosses, P. D., Nielsen, M., and Schwartzbach, M. I. (eds.), 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, Aarhus, Denmark, pp. 97\u2013107. Springer-Verlag."},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Srivas, M. and Camilleri, A. (eds.) (1996) Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (FMCAD'96), Volume 1166 of Lecture Notes in Computer Science. Springer-Verlag.","DOI":"10.1007\/BFb0031795"},{"key":"17_CR17","doi-asserted-by":"crossref","first-page":"144","DOI":"10.1145\/63522.214389","volume":"15","author":"P. T. P. Tang","year":"1989","unstructured":"Tang, P. T. P. (1989) Table-driven implementation of the exponential function in IEEE floating-point arithmetic. ACM Transactions on Mathematical Software, 15, 144\u2013157.","journal-title":"ACM Transactions on Mathematical Software"},{"key":"17_CR18","series-title":"Volume 1125 of Lecture Notes in Computer Science","volume-title":"Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs'96","author":"J. Wright von","year":"1996","unstructured":"von Wright, J., Grundy, J., and Harrison, J. (eds.) (1996) Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs'96, Volume 1125 of Lecture Notes in Computer Science, Turku, Finland. Springer-Verlag."}],"container-title":["Lecture Notes in Computer Science","Algebraic Methodology and Software Technology"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0000475","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,10]],"date-time":"2020-04-10T02:21:40Z","timestamp":1586485300000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0000475"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540638889","9783540696612"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/bfb0000475","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}