{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,4]],"date-time":"2023-09-04T21:17:18Z","timestamp":1693862238767},"reference-count":13,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2004,7,1]],"date-time":"2004-07-01T00:00:00Z","timestamp":1088640000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2004,7]]},"DOI":"10.1007\/s10817-004-3997-6","type":"journal-article","created":{"date-parts":[[2005,3,2]],"date-time":"2005-03-02T13:28:22Z","timestamp":1109770102000},"page":"29-49","source":"Crossref","is-referenced-by-count":14,"title":["Organizing Numerical Theories Using Axiomatic Type Classes"],"prefix":"10.1007","volume":"33","author":[{"given":"Lawrence C.","family":"Paulson","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"CR1","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/BF00881906","volume":"11","author":"W. M. Farmer","year":"1993","unstructured":"Farmer, W. M., Guttman, J. D. and Thayer, F. J.: IMPS: An interactive mathematical proof system, J. Automated Reasoning 11(2) (1993), 213?248.","journal-title":"J. Automated Reasoning"},{"key":"CR2","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1112\/S1461157000000267","volume":"3","author":"J. D. Fleuriot","year":"2000","unstructured":"Fleuriot, J. D. and Paulson, L. C.: Mechanizing nonstandard real analysis, LMS J. Comput. Math. 3 (2000), 140?190, http:\/\/www.lms.ac.uk\/jcm\/3\/lms1999-027\/.","journal-title":"LMS J. Comput. Math."},{"issue":"4","key":"CR3","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1006\/jsco.2002.0552","volume":"34","author":"H. Geuvers","year":"2002","unstructured":"Geuvers, H., Pollack, R., Wiedijk, F. and Zwanenburg, J.: A constructive algebraic hierarchy in Coq, J. Symbolic Comput. 34(4) (2002), 271?286.","journal-title":"J. Symbolic Comput."},{"key":"CR4","unstructured":"Gordon, M. J. C. and Melham, T. F.: Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, Cambridge University Press, 1993."},{"key":"CR5","doi-asserted-by":"crossref","unstructured":"Hudak, P.: The Haskell School of Expression, Cambridge University Press, 2000.","DOI":"10.1017\/CBO9780511818073"},{"key":"CR6","doi-asserted-by":"crossref","first-page":"583","DOI":"10.1016\/S0304-3975(02)00869-1","volume":"298","author":"G. Klein","year":"2003","unstructured":"Klein, G. and Nipkow, T.: Verified bytecode verifiers, Theoret. Comput. Sci. 298 (2003), 583?626.","journal-title":"Theoret. Comput. Sci."},{"key":"CR7","unstructured":"Nipkow, T.: Order-sorted polymorphism in Isabelle, in G. Huet and G. Plotkin (eds.), Logical Environments, Cambridge University Press, 1993, pp. 164?188."},{"key":"CR8","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L. C. and Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, LNCS 2283, Springer, 2002.","DOI":"10.1007\/3-540-45949-9"},{"key":"CR9","doi-asserted-by":"crossref","unstructured":"Paulson, L. C.: ML for the Working Programmer, 2nd edn, Cambridge University Press, 1996.","DOI":"10.1017\/CBO9780511811326"},{"issue":"3","key":"CR10","doi-asserted-by":"crossref","first-page":"332","DOI":"10.1145\/322510.322530","volume":"2","author":"L. C. Paulson","year":"1999","unstructured":"Paulson, L. C.: Inductive analysis of the Internet protocol TLS, ACM Transactions on Information and System Security 2(3) (1999), 332?351.","journal-title":"ACM Transactions on Information and System Security"},{"key":"CR11","unstructured":"The PVS standard prelude, http:\/\/pvs.csl.sri.com\/doc\/prelude.html, 2003."},{"key":"CR12","doi-asserted-by":"crossref","unstructured":"Wadler, P. and Blott, S.: How to make ad-hoc polymorphism less ad hoc, in 16th Annual Symposium on Principles of Programming Languages, ACM Press, 1989, pp. 60?76.","DOI":"10.1145\/75277.75283"},{"key":"CR13","doi-asserted-by":"crossref","unstructured":"Wenzel, M.: Type classes and overloading in higher-order logic, in E. L. Gunter and A. Felty (eds.), Theorem Proving in Higher Order Logics: TPHOLs ?97, LNCS 1275, Springer, 1997, pp. 307?322.","DOI":"10.1007\/BFb0028402"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-004-3997-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-004-3997-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-004-3997-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T02:23:16Z","timestamp":1586139796000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-004-3997-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,7]]},"references-count":13,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2004,7]]}},"alternative-id":["5383997"],"URL":"https:\/\/doi.org\/10.1007\/s10817-004-3997-6","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,7]]}}}