{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T16:27:04Z","timestamp":1780936024650,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540412199","type":"print"},{"value":"9783540409229","type":"electronic"}],"license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-40922-x_14","type":"book-chapter","created":{"date-parts":[[2007,11,29]],"date-time":"2007-11-29T09:41:36Z","timestamp":1196329296000},"page":"254-270","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":33,"title":["Formal Verification of Floating Point Trigonometric Functions"],"prefix":"10.1007","author":[{"given":"John","family":"Harrison","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2002,6,18]]},"reference":[{"key":"14_CR1","doi-asserted-by":"publisher","first-page":"903","DOI":"10.1090\/S0025-5718-97-00856-9","volume":"66","author":"D. Bailey","year":"1997","unstructured":"D. Bailey, P. Borwein, and S. Plouffe. On the rapid computation of various polylogarithmic constants. Mathematics of Computation, 66:903\u2013913, 1997.","journal-title":"Mathematics of Computation"},{"key":"14_CR2","unstructured":"A. Baker. A Consise Introduction to the Theory of Numbers. Cambridge University Press, 1985."},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"G. Cousineau and M. Mauny. The Functional Approach to Programming. Cam-bridge University Press, 1998.","DOI":"10.1017\/CBO9781139173018"},{"key":"14_CR4","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/BF01397083","volume":"18","author":"T. J. Dekker","year":"1971","unstructured":"T. J. Dekker. A floating-point technique for extending the available precision. Numerical Mathematics, 18:224\u2013242, 1971.","journal-title":"Numerical Mathematics"},{"key":"14_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: A Mechanised Logic of Computation","author":"M. J. C. Gordon","year":"1979","unstructured":"M. J. C. Gordon, R. Milner, and C. P. Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979."},{"key":"14_CR6","unstructured":"R. L. Graham, D. E. Knuth, and O. Patashnik. Concrete Mathematics: A Foun-dation for Computer Science. Addison-Wesley, 2nd edition, 1994."},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"J. Harrison. HOL Light: A tutorial introduction. In M. Srivas and A. Camilleri, editors, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201996), volume 1166 of Lecture Notes in mputerScience, pages 265\u2013269. Springer-Verlag, 1996.","DOI":"10.1007\/BFb0031814"},{"key":"14_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/BFb0028391","volume-title":"Verifying the accuracy of polynomial approximations in HOL","author":"J. Harrison","year":"1997","unstructured":"J. Harrison. Verifying the accuracy of polynomial approximations in HOL. In E. L. Gunter and A. Felty, editors, Theorem Proving in Higher Order Logics: 10th International Conference, TPHOLs\u201997, volume 1275 of Lecture Notes in Computer Science, pages 137\u2013152, Murray Hill, NJ, 1997. Springer-Verlag."},{"key":"14_CR9","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":"14_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/3-540-48256-3_9","volume-title":"A machine-checked theory of floating point arithmetic","author":"J. Harrison","year":"1999","unstructured":"J. Harrison. A machine-checked theory of floating point arithmetic. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Th\u00e9ry, editors, Theorem Proving in Higher Order Logics: 12th International Conference, TPHOLs\u201999, volume 1690 of Lecture Notes in Computer Science, pages 113\u2013130, Nice, France, 1999. Springer-Verlag."},{"key":"14_CR11","first-page":"1","volume":"1999-2Q4","author":"J. Harrison","year":"1999","unstructured":"J. Harrison, T. Kubaska, S. Story, and P. Tang. The computation of transcendental functions on the IA-64 architecture. Intel Technology Journal, 1999-2Q4:1\u20137, 1999. This paper is available on the Web as http:\/\/developer.intel.com\/technology\/itj\/q41999\/articles\/art_5.htm","journal-title":"Intel Technology Journal"},{"key":"14_CR12","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/BF01975722","volume":"5","author":"O. M\u00f8ller","year":"1965","unstructured":"O. M\u00f8ller. Quasi double-precision in floating-point addition. BIT, 5:37\u201350, 1965.","journal-title":"BIT"},{"key":"14_CR13","first-page":"337","volume":"199","author":"M. E. Remes","year":"1934","unstructured":"M. E. Remes. Sur le calcul effectif des polynomes d'approximation de Tchebichef. Comptes Rendus Hebdomadaires des S\u00e9ances de l'Acad\u00e9mie des Sciences, 199:337\u2013340, 1934.","journal-title":"Comptes Rendus Hebdomadaires des S\u00e9ances de l'Acad\u00e9mie des Sciences"},{"key":"14_CR14","unstructured":"P. H. Sterbenz. Floating-Point Computation. Prentice-Hall, 1974."},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"S. Story and P. T. P. Tang. New algorithms for improved transcendental functions on IA-64. In I. Koren and P. Kornerup, editors, Proceedings, 14th IEEE symposium on on computer arithmetic, pages 4\u201311, Adelaide, Australia, 1999. IEEE Computer Society.","DOI":"10.1109\/ARITH.1999.762822"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"P. T. P. Tang. Table-lookup algorithms for elementary functions and their error analysis. In Proceedings of the 10th Symposium on Computer Arithemtic, pages 232\u2013236, 1991.","DOI":"10.1109\/ARITH.1991.145565"},{"key":"14_CR17","unstructured":"P. Weis and X. Leroy. Le langage Caml. InterEditions, 1993. See also the CAML Web page: http:\/\/pauillac.inria.fr\/caml\/"}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-40922-X_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,23]],"date-time":"2025-01-23T00:23:11Z","timestamp":1737591791000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-40922-X_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540412199","9783540409229"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-40922-x_14","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2000]]},"assertion":[{"value":"18 June 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}