{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T21:28:14Z","timestamp":1767994094065,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642033582","type":"print"},{"value":"9783642033599","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-03359-9_4","type":"book-chapter","created":{"date-parts":[[2009,8,20]],"date-time":"2009-08-20T01:46:12Z","timestamp":1250732772000},"page":"60-66","source":"Crossref","is-referenced-by-count":116,"title":["HOL Light: An Overview"],"prefix":"10.1007","author":[{"given":"John","family":"Harrison","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","volume-title":"An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof","author":"P.B. Andrews","year":"1986","unstructured":"Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press, London (1986)"},{"key":"4_CR2","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Church, A.: A formulation of the Simple Theory of Types. Journal of Symbolic Logic\u00a05, 56\u201368 (1940)","journal-title":"Journal of Symbolic Logic"},{"key":"4_CR3","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1090\/S0002-9939-1975-0373893-X","volume":"51","author":"R. Diaconescu","year":"1975","unstructured":"Diaconescu, R.: Axiom of choice and complementation. Proceedings of the American Mathematical Society\u00a051, 176\u2013178 (1975)","journal-title":"Proceedings of the American Mathematical Society"},{"key":"4_CR4","first-page":"163","volume-title":"Tools and notions for program construction: an advanced course","author":"M.J.C. Gordon","year":"1982","unstructured":"Gordon, M.J.C.: Representing a logic in the LCF metalanguage. In: N\u00e9el, D. (ed.) Tools and notions for program construction: an advanced course, pp. 163\u2013185. Cambridge University Press, Cambridge (1982)"},{"key":"4_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":"4_CR6","series-title":"Lecture Notes in Computer Science","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":"Gordon, M.J.C., Milner, R., Wadsworth, C.P.: Edinburgh LCF. LNCS, vol.\u00a078. Springer, Heidelberg (1979)"},{"key":"4_CR7","series-title":"Dagstuhl Seminar Proceedings","volume-title":"Mathematics, Algorithms, Proofs","author":"T.C. Hales","year":"2006","unstructured":"Hales, T.C.: Introduction to the Flyspeck project. In: Coquand, T., Lombardi, H., Roy, M.-F. (eds.) Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, vol.\u00a005021. Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany (2006)"},{"key":"4_CR8","doi-asserted-by":"crossref","first-page":"882","DOI":"10.1080\/00029890.2007.11920481","volume":"114","author":"T.C. Hales","year":"2007","unstructured":"Hales, T.C.: The Jordan curve theorem, formally and informally. The American Mathematical Monthly\u00a0114, 882\u2013894 (2007)","journal-title":"The American Mathematical Monthly"},{"key":"4_CR9","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., Paulin-Mohring, C. (eds.) TYPES 1996. LNCS, vol.\u00a01512, pp. 154\u2013172. Springer, Heidelberg (1998)"},{"key":"4_CR10","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-1591-5","volume-title":"Theorem Proving with the Real Numbers","author":"J. Harrison","year":"1998","unstructured":"Harrison, J.: Theorem Proving with the Real Numbers. Springer, Heidelberg (1998); Revised version of author\u2019s PhD thesis"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/11757283_8","volume-title":"Formal Methods for Hardware Verification","author":"J. Harrison","year":"2006","unstructured":"Harrison, J.: Floating-point verification using theorem proving. In: Bernardo, M., Cimatti, A. (eds.) SFM 2006. LNCS, vol.\u00a03965, pp. 211\u2013242. Springer, Heidelberg (2006)"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-540-74591-4_9","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"2007","unstructured":"Harrison, J.: Verifying nonlinear real formulas via sums of squares. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 102\u2013118. Springer, Heidelberg (2007)"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Formalizing an analytic proof of the Prime Number Theorem (dedicated to Mike Gordon on the occasion of his 60th birthday). Journal of Automated Reasoning (to appear, 2009)","DOI":"10.1007\/s10817-009-9145-6"},{"key":"4_CR14","series-title":"Cambridge studies in advanced mathematics","volume-title":"Introduction to higher order categorical logic","author":"J. Lambek","year":"1986","unstructured":"Lambek, J., Scott, P.J.: Introduction to higher order categorical logic. Cambridge studies in advanced mathematics, vol.\u00a07. Cambridge University Press, Cambridge (1986)"},{"key":"4_CR15","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/321450.321456","volume":"15","author":"D.W. Loveland","year":"1968","unstructured":"Loveland, D.W.: Mechanical theorem-proving by model elimination. Journal of the ACM\u00a015, 236\u2013251 (1968)","journal-title":"Journal of the ACM"},{"key":"4_CR16","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1016\/0304-3975(93)90095-B","volume":"121","author":"D. Scott","year":"1993","unstructured":"Scott, D.: A type-theoretical alternative to ISWIM, CUCH, OWHY. Theoretical Computer Science\u00a0121, 411\u2013440 (1993); Annotated version of a 1969 manuscript","journal-title":"Theoretical Computer Science"},{"key":"4_CR17","unstructured":"Solovay, R.M., Arthan, R., Harrison, J.: Some new results on decidability for elementary algebra and geometry. ArXiV preprint 0904.3482 (2009); submitted to Annals of Pure and Applied Logic, \n                    \n                      http:\/\/arxiv.org\/PS_cache\/arxiv\/pdf\/0904\/0904.3482v1.pdf"}],"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\/978-3-642-03359-9_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,9]],"date-time":"2019-03-09T13:29:46Z","timestamp":1552138186000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03359-9_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642033582","9783642033599"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03359-9_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}