{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T01:55:34Z","timestamp":1778291734101,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540371878","type":"print"},{"value":"9783540371885","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11814771_17","type":"book-chapter","created":{"date-parts":[[2006,10,5]],"date-time":"2006-10-05T15:44:21Z","timestamp":1160063061000},"page":"177-191","source":"Crossref","is-referenced-by-count":45,"title":["Towards Self-verification of HOL Light"],"prefix":"10.1007","author":[{"given":"John","family":"Harrison","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"17_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":"17_CR2","doi-asserted-by":"publisher","first-page":"181","DOI":"10.2307\/421013","volume":"3","author":"H. Barendregt","year":"1997","unstructured":"Barendregt, H.: The impact of the lambda calculus on logic and computer science. Bulletin of Symbolic Logic\u00a03, 181\u2013215 (1997)","journal-title":"Bulletin of Symbolic Logic"},{"key":"17_CR3","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":"17_CR4","doi-asserted-by":"publisher","first-page":"252","DOI":"10.2307\/2316620","volume":"79","author":"P.J. Davis","year":"1972","unstructured":"Davis, P.J.: Fidelity in mathematical discourse: Is one and one really two? The American Mathematical Monthly\u00a079, 252\u2013263 (1972)","journal-title":"The American Mathematical Monthly"},{"key":"17_CR5","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":"17_CR6","first-page":"205","volume-title":"Selected Writings on Computing: A Personal Perspective","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: Formal techniques and sizeable programs (EWD563). In: Dijkstra, E.W. (ed.) Selected Writings on Computing: A Personal Perspective, pp. 205\u2013214. Springer, Heidelberg (1976); (Paper prepared for Symposium on the Mathematical Foundations of Computing Science, Gdansk 1976)"},{"key":"17_CR7","series-title":"Advances in Logic","doi-asserted-by":"publisher","DOI":"10.1142\/9789812795038","volume-title":"Reasoning about theoretical entities","author":"T. Forster","year":"2003","unstructured":"Forster, T.: Reasoning about theoretical entities. Advances in Logic, vol.\u00a03. World Scientific, Singapore (2003)"},{"key":"17_CR8","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":"17_CR9","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":"17_CR10","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":"17_CR11","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":"17_CR12","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":"17_CR13","unstructured":"Lecat, M.: Erreurs de Math\u00e9maticiens. Brussels (1935)"},{"key":"17_CR14","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/978-1-4757-3188-0_16","volume-title":"Computer-Aided Reasoning: ACL2 Case Studies","author":"W. McCune","year":"2000","unstructured":"McCune, W., Shumsky, O.: Ivy: A preprocessor and proof checker for first-order logic. In: Kaufmann, M., Manolios, P., Moore, J.S. (eds.) Computer-Aided Reasoning: ACL2 Case Studies, pp. 265\u2013281. Kluwer, Dordrecht (2000)"},{"key":"17_CR15","series-title":"IFIP Transactions A: Computer Science and Technology","first-page":"3","volume-title":"Proceedings of the IFIP TC10\/WG10.2 International Workshop on Higher Order Logic Theorem Proving and its Applications","author":"T.F. Melham","year":"1992","unstructured":"Melham, T.F.: The HOL logic extended with quantification over type variables. In: Claesen, L.J.M., Gordon, M.J.C. (eds.) Proceedings of the IFIP TC10\/WG10.2 International Workshop on Higher Order Logic Theorem Proving and its Applications, IMEC, Leuven, Belgium. IFIP Transactions A: Computer Science and Technology, vol.\u00a0A-20, pp. 3\u201318. North-Holland, Amsterdam (1992)"},{"key":"17_CR16","volume-title":"Twenty-Five Years of Constructive Type Theory","author":"R. Pollack","year":"1998","unstructured":"Pollack, R.: How to believe a machine-checked proof. In: Sambin, G., Smith, J. (eds.) Twenty-Five Years of Constructive Type Theory, Oxford University Press, Oxford (1998), also available on the Web as http:\/\/www.brics.dk\/~pollack\/export\/believing.ps.gz"},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"Ridge, T.: A mechanically verified, efficient, sound and complete theorem prover for first order logic (2005), available via http:\/\/homepages.inf.ed.ac.uk\/s0128214\/","DOI":"10.1007\/11541868_19"},{"key":"17_CR18","unstructured":"Rudnicki, P.: An overview of the MIZAR project (1992), available on the Web as http:\/\/web.cs.ualberta.ca\/~piotr\/Mizar\/MizarOverview.ps"},{"key":"17_CR19","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":"17_CR20","unstructured":"Slind, K.: Reasoning about terminating functional programs. PhD thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen (1999), available from http:\/\/tumb1.biblio.tu-muenchen.de\/publ\/diss\/in\/1999\/slind.html"},{"key":"17_CR21","series-title":"Oxford Logic Guides","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780195046724.001.0001","volume-title":"G\u00f6del\u2019s Incompleteness Theorems","author":"R.M. Smullyan","year":"1992","unstructured":"Smullyan, R.M.: G\u00f6del\u2019s Incompleteness Theorems. Oxford Logic Guides, vol.\u00a019. Oxford University Press, Oxford (1992)"},{"key":"17_CR22","unstructured":"Wong, W.: Recording HOL proofs. Technical Report 306, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge, CB2 3QG, UK (1993)"},{"key":"17_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"456","DOI":"10.1007\/3-540-58450-1_60","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"J. Wright von","year":"1994","unstructured":"von Wright, J.: Representing higher-order logic proofs in HOL. In: Melham, T.F., Camilleri, J. (eds.) HUG 1994. LNCS, vol.\u00a0859, pp. 456\u2013470. Springer, Heidelberg (1994)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11814771_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,1]],"date-time":"2021-08-01T22:01:30Z","timestamp":1627855290000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11814771_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540371878","9783540371885"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/11814771_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}