{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T18:12:49Z","timestamp":1781892769813,"version":"3.54.5"},"publisher-location":"Berlin, Heidelberg","reference-count":8,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540633792","type":"print"},{"value":"9783540695264","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/bfb0028391","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T01:50:11Z","timestamp":1132624211000},"page":"137-152","source":"Crossref","is-referenced-by-count":19,"title":["Verifying the accuracy of polynomial approximations in HOL"],"prefix":"10.1007","author":[{"given":"John","family":"Harrison","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2005,6,17]]},"reference":[{"key":"10_CR1","unstructured":"Benedetti, R. and Risler, J.-J. (1990) Real algebraic and semi-algebraic sets. Hermann, Paris."},{"key":"10_CR2","unstructured":"Boyer, R. S. and Moore, J S. (1979) A Computational Logic. ACM Monograph Series. Academic Press."},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Harrison, J. (1997) Floating point verification in HOL Light: The exponential function. Unpublished draft, to appear.","DOI":"10.1007\/BFb0000475"},{"key":"10_CR4","unstructured":"Harrison, J. (1996) Theorem proving with the real numbers. Technical Report 408, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge, CB2 3QG, UK. Author's PhD thesis."},{"key":"10_CR5","unstructured":"Pour-El, M. B. and Richards, J. L (1980) Computability in Analysis and Physics. Perspectives in Mathematical Logic. Springer-Verlag."},{"key":"10_CR6","first-page":"337","volume":"199","author":"M. E. Remes","year":"1934","unstructured":"Remes, M. E. (1934) 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.","journal-title":"Comptes Rendus Hebdomadaires des S\u00e9ances de l'Acad\u00e9mie des Sciences"},{"key":"10_CR7","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1007\/BF01386330","volume":"4","author":"T. J. Rivlin","year":"1962","unstructured":"Rivlin, T. J. (1962) Polynomials of but uniform approximation to certain rational functions. Numerische Mathematik, 4, 345\u2013349","journal-title":"Numerische Mathematik"},{"key":"10_CR8","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"}],"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\/BFb0028391","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,10]],"date-time":"2020-04-10T22:49:04Z","timestamp":1586558944000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0028391"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540633792","9783540695264"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/bfb0028391","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1997]]}}}