{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:06:58Z","timestamp":1776305218569,"version":"3.50.1"},"reference-count":47,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2000,6,1]],"date-time":"2000-06-01T00:00:00Z","timestamp":959817600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2000,6,1]],"date-time":"2000-06-01T00:00:00Z","timestamp":959817600000},"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":["Formal Methods in System Design"],"published-print":{"date-parts":[[2000,6]]},"DOI":"10.1023\/a:1008712907154","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T11:37:32Z","timestamp":1040557052000},"page":"271-305","source":"Crossref","is-referenced-by-count":29,"title":["Floating Point Verification in HOL Light: The Exponential Function"],"prefix":"10.1007","volume":"16","author":[{"given":"John","family":"Harrison","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"260865_CR1","volume-title":"Correctness Preserving Program Transformations: Proof Theory and Applications","author":"R. Back","year":"1980","unstructured":"R. Back, Correctness Preserving Program Transformations: Proof Theory and Applications, Mathematical Centre Tracts, Vol. 131, Mathematical Centre, Amsterdam, 1980."},{"key":"260865_CR2","doi-asserted-by":"crossref","unstructured":"A. Baker, Transcendental Number Theory, Cambridge University Press, 1975.","DOI":"10.1017\/CBO9780511565977"},{"key":"260865_CR3","doi-asserted-by":"crossref","first-page":"611","DOI":"10.1109\/32.24710","volume":"15","author":"M. Barratt","year":"1989","unstructured":"M. Barratt, \u201cFormal methods applied to a floating-point system, \u201d IEEE Transactions on Software Engineering, Vol. 15, pp. 611\u2013621, 1989.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"260865_CR4","first-page":"844","volume":"7","author":"J. Barwise","year":"1989","unstructured":"J. Barwise, \u201cMathematical proofs of computer correctness, \u201d Notices of the American Mathematical Society, Vol. 7, pp. 844\u2013851, 1989.","journal-title":"Notices of the American Mathematical Society"},{"key":"260865_CR5","unstructured":"R. Benedetti and J.-J. Risler, Real Algebraic and Semi-Algebraic Sets, Hermann, Paris, 1990."},{"key":"260865_CR6","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/BFb0031816","volume":"1166","author":"B. Brock","year":"1996","unstructured":"B. Brock, M. Kaufmann, and J.S. Moore, \u201cACL2 theorems about commercial microprocessors, \u201d in [41], pp.275\u2013293.","journal-title":"Proceedings of the First International Conference on Formal Methodsin Computer-Aided Design (FMCAD'96)"},{"key":"260865_CR7","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1145\/62.322429","volume":"31","author":"C.W. Clenshaw","year":"1984","unstructured":"C.W. Clenshaw and F.W.J. Olver, \u201cBeyond floating point, \u201d Journal of the ACM, Vol. 31, pp. 319\u2013328, 1984.","journal-title":"Journal of the ACM"},{"key":"260865_CR8","doi-asserted-by":"crossref","unstructured":"G. Cousineau and M. Mauny, The Functional Approach to Programming, Cambridge University Press, 1998.","DOI":"10.1017\/CBO9781139173018"},{"key":"260865_CR9","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1145\/359104.359106","volume":"22","author":"R. DeMillo","year":"1979","unstructured":"R. DeMillo, R. Lipton, and A. Perlis, \u201cSocial processes and proofs of theorems and programs, \u201d Communications of the ACM, Vol. 22, pp. 271\u2013280, 1979.","journal-title":"Communications of the ACM"},{"key":"260865_CR10","unstructured":"E.W. Dijkstra,A Discipline of Programming, Prentice-Hall, 1976."},{"key":"260865_CR11","unstructured":"B. Dutertre, \u201cElements of mathematical analysis in PVS, \u201d Le langage Caml, InterEditions, 1993. See also the CAML Web page: http:\/\/ pauillac.inria.fr\/caml\/. in [46], pp. 141\u2013156, 1996."},{"key":"260865_CR12","doi-asserted-by":"crossref","unstructured":"S. Gal, \u201cComputing elementary functions: A new approach for achieving high accuracy and good performance, \u201d in W.L. Miranker and R.A. Toupin (Eds.), Accurate Scientific Computations, Lecture Notes in Computer Science, 1986, Vol. 235, pp. 1\u201316.","DOI":"10.1007\/3-540-16798-6_1"},{"key":"260865_CR13","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1145\/103162.103163","volume":"23","author":"D. Goldberg","year":"1991","unstructured":"D. Goldberg, \u201cWhat every computer scientist should know about floating point arithmetic, \u201d ACM Computing Surveys, Vol. 23, pp. 5\u201348, 1991.","journal-title":"ACM Computing Surveys"},{"key":"260865_CR14","doi-asserted-by":"crossref","unstructured":"M.J.C. Gordon, \u201cMechanizing programming logics in higher order logic, \u201d in G. Birtwistle and P.A. Subrahmanyam (Eds.), Current Trends in Hardware Verification and Automated Theorem Proving, pp. 387\u2013439, 1989.","DOI":"10.1007\/978-1-4612-3658-0_10"},{"key":"260865_CR15","doi-asserted-by":"crossref","unstructured":"M. Gordon, \u201cThe semantic challenge of Verilog HDL, \u201d in Proceedings of the Tenth Annual IEEE Symposium on Logic in Computer Science, San Diego, CA, USA, pp. 136\u2013145, 1995.","DOI":"10.1109\/LICS.1995.523251"},{"key":"260865_CR16","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":"260865_CR17","doi-asserted-by":"crossref","unstructured":"M.J.C. Gordon, R. Milner, and C.P. Wadsworth, Edinburgh LCF: A Mechanised Logic of Computation, Lecture Notes in Computer Science, Vol. 78, Springer-Verlag, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"260865_CR18","doi-asserted-by":"crossref","unstructured":"J. Harrison, \u201cFloating point verification in HOL, \u201d in P.J. Windley, T. Schubert, and J. Alves-Foss (Eds.), Higher Order Logic Theorem Proving and Its Applications: Proceedings of the 8th International Workshop, Aspen Grove, Utah. Lecture Notes in Computer Science, Vol. 971, pp. 186\u2013199, 1995.","DOI":"10.1007\/3-540-60275-5_65"},{"key":"260865_CR19","first-page":"265","volume":"1166","author":"J. Harrison","year":"1996","unstructured":"J. Harrison, \u201cHOL Light: A tutorial introduction, \u201d see [41], pp. 265\u2013269.","journal-title":"Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (FMCAD'96)"},{"key":"260865_CR20","unstructured":"J. Harrison, \u201cA Mizar mode for HOL, \u201d Le langage Caml, InterEditions, 1993. See also the CAML Web page: http:\/\/pauillac.inria.fr\/caml\/. in [46] pp. 203\u2013220."},{"key":"260865_CR21","doi-asserted-by":"crossref","unstructured":"J. Harrison, \u201cTheorem proving with the real numbers, \u201d Springer-Verlag. Revised version of author's Ph.D. thesis, 1998.","DOI":"10.1007\/978-1-4471-1591-5"},{"key":"260865_CR22","doi-asserted-by":"crossref","unstructured":"J. Harrison, \u201cVerifying the accuracy of polynomial approximations in HOL, \u201d in E.L. Gunter and A. Felty (Eds.), Theorem Proving in Higher Order Logics: 10th International Conference, TPHOLs'97, Murray Hill, NJ. Lecture Notes in Computer Science, Vol. 1275, 1997, pp. 137\u2013152.","DOI":"10.1007\/BFb0028391"},{"key":"260865_CR23","doi-asserted-by":"crossref","unstructured":"J. Harrison, \u201cA machine-checked theory of floating point arithmetic, \u201d in Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Th\u00b4ery (Eds.), Theorem Proving in Higher Order Logics: 12th International Conference, TPHOLs'97, Vol. 1690, Lecture Notes in Computer Science. Nice, France, 1999, pp. 113\u2013130.","DOI":"10.1007\/3-540-48256-3_9"},{"key":"260865_CR24","volume-title":"Standard for binary floating point arithmetic","author":"IEEE","year":"1985","unstructured":"IEEE, \u201cStandard for binary floating point arithmetic, \u201d ANSI\/IEEE Standard 754-1985, The Institute of Electrical and Electronic Engineers, Inc., 345 East 47th Street, New York, NY 10017, USA, 1985."},{"key":"260865_CR25","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/BF01446522","volume":"120","author":"F. Lindemann","year":"1882","unstructured":"F. Lindemann, \u201c \u00d1ber die Zahl \u03c0, \u201d Mathematische Annalen, Vol. 120, pp. 213\u2013225, 1882.","journal-title":"Mathematische Annalen"},{"key":"260865_CR26","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1145\/321450.321456","volume":"15","author":"D.W. Loveland","year":"1968","unstructured":"D.W. Loveland, \u201cMechanical theorem-proving by model elimination, \u201d Journal of the ACM, Vol. 15, pp. 236\u2013251, 1968.","journal-title":"Journal of the ACM"},{"key":"260865_CR27","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1098\/rsta.1953.0001","volume":"245","author":"K. Mahler","year":"1953","unstructured":"K. Mahler, \u201cOn the approximation of logarithms of algebraic numbers, \u201d Philosophical Transactions of the Royal Society of London, Series A, Vol. 245, pp. 371\u2013398, 1953.","journal-title":"Philosophical Transactions of the Royal Society of London, Series A"},{"key":"260865_CR28","series-title":"Technical Memorandum","volume-title":"Defining the IEEE-854 Floating-point standard in PVS","author":"P.S. Miner","year":"1995","unstructured":"P.S. Miner, \u201cDefining the IEEE-854 Floating-point standard in PVS, \u201d Technical Memorandum 110167, NASA Langley Research Center, Hampton, VA 23681-0001, USA, 1995."},{"key":"260865_CR29","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1007\/BFb0031800","volume":"1166","author":"P.S. Miner","year":"1996","unstructured":"P.S. Miner and J.F. Leathrum, \u201cVerification of IEEE compliant subtractive division algorithms, \u201d see [41], pp. 64\u201378.","journal-title":"Proceedings of the First International Conference on Formal Methodsin Computer-Aided Design (FMCAD'96)"},{"key":"260865_CR30","doi-asserted-by":"crossref","first-page":"913","DOI":"10.1109\/12.713311","volume":"47","author":"J.S. Moore","year":"1998","unstructured":"J.S. Moore, T. Lynch, and M. Kaufmann, \u201cA mechanically checked proof of the correctness of the kernel of the AMD5K 86 floating-point division algorithm, \u201d IEEE Transactions on Computers, Vol. 47, pp. 913\u2013926, 1998. Available on the Web as http:\/\/devil.ece.utexas.edu:80\/lynch\/divide\/divide.html, 1996.","journal-title":"IEEE Transactions on Computers"},{"key":"260865_CR31","unstructured":"K.C. Ng, \u201cArgument reduction for huge arguments: Good to the last bit, \u201d Unpublished draft, available from the author (kwok.ng@eng.sun.com), 1992."},{"key":"260865_CR32","doi-asserted-by":"crossref","unstructured":"T. Nipkow, \u201cWinskel is (almost) right: Towards a mechanized semantics textbook, \u201d in V. Chandru and V. Vinay (Eds.), in Foundations of Software Technology and Theoretical Computer Science, 16th Conference, Proceedings. pp. 180\u2013192, 1996.","DOI":"10.1007\/3-540-62034-6_48"},{"key":"260865_CR33","series-title":"Technical Report","volume-title":"C formalized in HOL","author":"M. Norrish","year":"1998","unstructured":"M. Norrish, \u201cC formalized in HOL, \u201d Technical Report 453, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge, CB2 3QG, UK. Author's Ph.D. thesis, 1998."},{"key":"260865_CR34","first-page":"1","volume":"1999-Q1","author":"J. O'Leary","year":"1999","unstructured":"J. O'Leary, X. Zhao, R. Gerth, and C.-J.H. Seger, \u201cFormally verifying IEEE compliance of floating-point hardware, \u201d Intel Technology Journal, Vol. 1999-Q1, pp. 1\u201314. Available on theWeb as http:\/\/developer. intel.com\/technology\/itj\/q11999\/articles\/art 5.htm, 1999.","journal-title":"Intel Technology Journal"},{"key":"260865_CR35","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1007\/BF00936948","volume":"12","author":"I. Page","year":"1996","unstructured":"I. Page, \u201cConstructing hardware-software systems from a single description, \u201d Journal of VLSI Signal Processing, Vol. 12, pp. 87\u2013107, 1996.","journal-title":"Journal of VLSI Signal Processing"},{"key":"260865_CR36","doi-asserted-by":"crossref","unstructured":"L.C. Paulson, Logic and Computation: Interactive Proof with Cambridge LCF, Cambridge Tracts in Theoretical Computer Science, Vol. 2, Cambridge University Press, 1987.","DOI":"10.1017\/CBO9780511526602"},{"issue":"1","key":"260865_CR37","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1145\/1057600.1057602","volume":"18","author":"M. Payne","year":"1983","unstructured":"M. Payne and R. Hanek, \u201cRadian reduction for trigonometric functions, \u201d SIGNUM Newsletter, Vol. 18, No. 1, pp. 19\u201324, 1983.","journal-title":"SIGNUM Newsletter"},{"key":"260865_CR38","doi-asserted-by":"crossref","unstructured":"R. Pollack, \u201cHow to believe a machine-checked proof, \u201d in G. Sambin and J. Smith (Eds.), Twenty-Five Years of Constructive Type Theory, Also available on the Web as http:\/\/www.brics.dk\/pollack\/export\/ believing.ps.gz, 1998.","DOI":"10.1093\/oso\/9780198501275.003.0013"},{"key":"260865_CR39","doi-asserted-by":"crossref","unstructured":"V.R. Pratt, \u201cAnatomy of the Pentium bug, \u201d in P.D. Mosses, M. Nielsen, and M.I. Schwartzbach (Eds.), Proceedings of the 5th International Joint Conference on the Theory and Practice of Software Development (TAPSOFT'95), Aarhus, Denmark. Lecture Notes in Computer Science, Vol. 915, 1995, pp. 97\u2013107.","DOI":"10.1007\/3-540-59293-8_189"},{"key":"260865_CR40","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1112\/S1461157000000176","volume":"1","author":"D. Rusinoff","year":"1998","unstructured":"D. Rusinoff, \u201cAmechanically checked proof of IEEE compliance of a register-transfer-level specification of the AMD-K7 floating-point multiplication, division, and square root instructions, \u201d LMS Journal of Computation and Mathematics, Vol. 1, pp. 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":"260865_CR41","doi-asserted-by":"crossref","unstructured":"M. Srivas and A. Camilleri (Eds.), in Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (FMCAD'96). Lecture Notes in Computer Science, Vol. 1166, Springer-Verlag, 1996.","DOI":"10.1007\/BFb0031795"},{"key":"260865_CR42","doi-asserted-by":"crossref","first-page":"144","DOI":"10.1145\/63522.214389","volume":"15","author":"P.T.P. Tang","year":"1989","unstructured":"P.T.P. Tang, \u201cTable-driven implementation of the exponential function in IEEE floating-point arithmetic, \u201d ACM Transactions on Mathematical Software, Vol. 15, pp. 144\u2013157, 1989.","journal-title":"ACM Transactions on Mathematical Software"},{"key":"260865_CR43","first-page":"136","volume":"6","author":"A. Trybulec","year":"1978","unstructured":"A. Trybulec, \u201cThe Mizar-QC\/6000 logic information language, \u201d ALLC Bulletin (Association for Literary and Linguistic Computing), Vol. 6, pp. 136\u2013140, 1978.","journal-title":"ALLC Bulletin (Association for Literary and Linguistic Computing)"},{"key":"260865_CR44","unstructured":"J. von Wright, J. Grundy, and J. Harrison (Eds.), in Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs'96, Turku, Finland. Lecture Notes in Computer Science, Vol. 1175, Springer-Verlag, 1996."},{"key":"260865_CR45","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/BF01383984","volume":"3","author":"J. von Wright","year":"1993","unstructured":"J. von Wright, J. Hekanaho, P. Luostarinen, and T. L\u00e5ngbacka, \u201cMechanizing some advanced refinement concepts, \u201d Formal Methods in System Design, Vol. 3, pp. 49\u201382, 1993.","journal-title":"Formal Methods in System Design"},{"key":"260865_CR46","unstructured":"P. Weis and X. Leroy, Le langage Caml, InterEditions, 1993. See also the CAML Web page: http:\/\/ pauillac.inria.fr\/caml\/."},{"key":"260865_CR47","volume-title":"Rounding Errors in Algebraic Processes","author":"J.H. Wilkinson","year":"1963","unstructured":"J.H. Wilkinson, Rounding Errors in Algebraic Processes, National Physical Laboratory Notes on Applied Science, Vol. 32, Her Majesty's Stationery Office (HMSO), London, 1963."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008712907154.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1008712907154\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008712907154.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T04:55:23Z","timestamp":1754369723000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1008712907154"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,6]]},"references-count":47,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2000,6]]}},"alternative-id":["260865"],"URL":"https:\/\/doi.org\/10.1023\/a:1008712907154","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2000,6]]}}}