{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:50:04Z","timestamp":1725475804679},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540676645"},{"type":"electronic","value":"9783540451013"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10721959_1","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T16:12:31Z","timestamp":1167408751000},"page":"1-6","source":"Crossref","is-referenced-by-count":0,"title":["High-Level Verification Using Theorem Proving and Formalized Mathematics"],"prefix":"10.1007","author":[{"given":"John","family":"Harrison","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","doi-asserted-by":"publisher","first-page":"903","DOI":"10.1090\/S0025-5718-97-00856-9","volume":"66","author":"D. Bailey","year":"1997","unstructured":"Bailey, D., Borwein, P., Plouffe, S.: On the rapid computation of various poly- logarithmic constants. Mathematics of Computation\u00a066, 903\u2013913 (1997)","journal-title":"Mathematics of Computation"},{"key":"1_CR2","series-title":"Lecture Notes in Computer Science","first-page":"83","volume-title":"Theorem Proving in Higher Order Logics","year":"1999","unstructured":"Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.): TPHOLs 1999. LNCS, vol.\u00a01690, p. 83. Springer, Heidelberg (1999)"},{"key":"1_CR3","unstructured":"Boulton, R.J.: Effciency in a fully-expansive theorem prover. Technical Report 337, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge, CB2 3QG, UK, Author\u2019s PhD thesis (1993)"},{"key":"1_CR4","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139173018","volume-title":"The Functional Approach to Programming","author":"G. Cousineau","year":"1998","unstructured":"Cousineau, G., Mauny, M.: The Functional Approach to Programming. Cambridge University Press, Cambridge (1998)"},{"key":"1_CR5","volume-title":"Introduction to HOL: a theorem proving environment for higher order logic","author":"M.J.C. Gordon","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F.: Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, Cambridge (1993)"},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF","author":"M.J.C. Gordon","year":"1979","unstructured":"Gordon, M.J.C., Milner, R., Wadsworth, C.P.: Edinburgh LCF. LNCS, vol.\u00a078. Springer, Heidelberg (1979)"},{"key":"1_CR7","unstructured":"Harrison, J.: Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-053, SRI Cambridge, Millers Yard, Cambridge, UK (1995), Available on the Web as, http:\/\/www.cl.cam.ac.uk\/users\/jrh\/papers\/reflect.dvi.gz"},{"key":"1_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"Formal Methods in Computer-Aided Design","author":"J. Harrison","year":"1996","unstructured":"Harrison, J.: HOL Light: A tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 265\u2013269. Springer, Heidelberg (1996)"},{"key":"1_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1007\/BFb0105406","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"1996","unstructured":"Harrison, J.: A Mizar mode for HOL. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol.\u00a01125, pp. 203\u2013220. Springer, Heidelberg (1996)"},{"key":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/BFb0097791","volume-title":"Types for Proofs and Programs","author":"J. Harrison","year":"1998","unstructured":"Harrison, J.: Proof style. In: Gim\u00e9nez, E. (ed.) TYPES 1996. LNCS, vol.\u00a01512, pp. 154\u2013172. Springer, Heidelberg (1998)"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Harrison, J.: 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":"1_CR12","doi-asserted-by":"crossref","unstructured":"Harrison, J.: A machine-checked theory of floating point arithmetic. In: Bertot et al. [2], pp. 113\u2013130","DOI":"10.1007\/3-540-48256-3_9"},{"key":"1_CR13","unstructured":"IEEE. Standard for binary floating point arithmetic. ANSI\/IEEE Standard 754- 1985, The Institute of Electrical and Electronic Engineers, Inc., 345 East 47th Street, New York, NY 10017, USA (1985)"},{"key":"1_CR14","unstructured":"Knopp, K.: Theory and Application of Infinite Series, 2nd edn. Blackie and Son Ltd. (1951)"},{"key":"1_CR15","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1109\/HOL.1991.596284","volume-title":"Proceedings of the 1991 International Workshop on the HOL theorem proving system and its Applications","author":"R. Kumar","year":"1991","unstructured":"Kumar, R., Kropf, T., Schneider, K.: Integrating a first-order automatic prover in the HOL environment. In: Archer, M., Joyce, J.J., Levitt, K.N. (eds.) Proceedings of the 1991 International Workshop on the HOL theorem proving system and its Applications, University of California at Davis, Davis CA, USA, pp. 170\u2013176. IEEE Computer Society Press, Los Alamitos (1991)"},{"key":"1_CR16","doi-asserted-by":"publisher","first-page":"913","DOI":"10.1109\/12.713311","volume":"47","author":"J.S. Moore","year":"1998","unstructured":"Moore, J.S., Lynch, T., Kaufmann, M.: A mechanically checked proof of the correctness of the kernel of the AMD5K86 floating-point division program. IEEE Transactions on Computers\u00a047, 913\u2013926 (1998)","journal-title":"IEEE Transactions on Computers"},{"key":"1_CR17","unstructured":"O\u2019Leary, J., Zhao, X., Gerth, R., Seger, C.-J.H.: Formally verifying IEEE compliance of floating-point hardware. Intel Technology Journal\u00a01999-Q1, 1\u201314 (1999), Available on the Web as http:\/\/developer.intel.com\/technology\/itj\/q11999\/articles\/art_5.htm."},{"key":"1_CR18","unstructured":"Rudnicki, P.: An overview of the MIZAR project. Available on the Web as http:\/\/web.cs.ualberta.ca\/~piotr\/Mizar\/MizarOverview.ps (1992)"},{"key":"1_CR19","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1112\/S1461157000000176","volume":"1","author":"D. Rusinoff","year":"1998","unstructured":"Rusinoff, D.: A mechanically checked proof of IEEE compliance of a register-transfer-level specification of the AMD-K7 floating-point multiplication, division, and square root instructions. LMS Journal of Computation and Mathematics\u00a01, 148\u2013200 (1998), Available on the Web via http:\/\/www.onr.com\/user\/russ\/david\/k7-div-sqrt.html","journal-title":"LMS Journal of Com- putation and Mathematics"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Russell, B.: The autobiography of Bertrand Russell. Allen & Unwin (1968)","DOI":"10.2307\/2218050"},{"key":"1_CR21","doi-asserted-by":"crossref","unstructured":"Syme, D.: Three tactic theorem proving. In: Bertot et al. [2], pp. 203\u2013220","DOI":"10.1007\/3-540-48256-3_14"},{"key":"1_CR22","first-page":"136","volume":"6","author":"A. Trybulec","year":"1978","unstructured":"Trybulec, A.: The Mizar-QC\/6000 logic information language. ALLC Bulletin (Association for Literary and Linguistic Computing)\u00a06, 136\u2013140 (1978)","journal-title":"ALLC Bulletin (Association for Literary and Linguistic Computing)"},{"key":"1_CR23","unstructured":"Weis, P., Leroy, X.: Le langage Caml. InterEditions (1993), See also the CAML Web page: http:\/\/pauillac.inria.fr\/caml\/"},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"Wenzel, M.: Isar - a generic intepretive approach to readable formal proof documents. In: Bertot et al. [2], pp. 167\u2013183","DOI":"10.1007\/3-540-48256-3_12"},{"key":"1_CR25","volume-title":"Principia Mathematica","author":"A.N. Whitehead","year":"1910","unstructured":"Whitehead, A.N., Russell, B.: Principia Mathematica, vol.\u00a03. Cambridge University Press, Cambridge (1910)"},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"Zammit, V.: On the implementation of an extensible declarative proof language. In: Bertot et al. [2],pp. 185\u2013202","DOI":"10.1007\/3-540-48256-3_13"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-17"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10721959_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,23]],"date-time":"2019-04-23T07:42:52Z","timestamp":1556005372000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10721959_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676645","9783540451013"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/10721959_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}