{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T09:24:15Z","timestamp":1766136255530,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642228629"},{"type":"electronic","value":"9783642228636"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-22863-6_20","type":"book-chapter","created":{"date-parts":[[2011,8,8]],"date-time":"2011-08-08T05:47:55Z","timestamp":1312782475000},"page":"265-280","source":"Crossref","is-referenced-by-count":13,"title":["A Verified Runtime for a Verified Theorem Prover"],"prefix":"10.1007","author":[{"given":"Magnus O.","family":"Myreen","sequence":"first","affiliation":[]},{"given":"Jared","family":"Davis","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","volume-title":"A Computational Logic Handbook","author":"R.S. Boyer","year":"1997","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic Handbook, 2nd edn. Academic Press, London (1997)","edition":"2"},{"key":"20_CR2","volume-title":"ACL2 2006","author":"R.S. Boyer","year":"2006","unstructured":"Boyer, R.S., Hunt Jr., W.A.: Function memoization and unique object representation for ACL2 functions. In: ACL2 2006. ACM, New York (2006)"},{"key":"20_CR3","volume-title":"POPL","author":"A.J. Chlipala","year":"2010","unstructured":"Chlipala, A.J.: A verified compiler for an impure functional language. In: Hermenegildo, M.V., Palsberg, J. (eds.) POPL. ACM, New York (2010)"},{"key":"20_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/978-3-540-75560-9_17","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"Z. Dargaye","year":"2007","unstructured":"Dargaye, Z., Leroy, X.: Mechanized verification of CPS transformations. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol.\u00a04790, pp. 211\u2013225. Springer, Heidelberg (2007)"},{"key":"20_CR5","unstructured":"Davis, J.C.: A Self-Verifying Theorem Prover. PhD thesis, University of Texas at Austin (December 2009)"},{"issue":"9","key":"20_CR6","doi-asserted-by":"publisher","first-page":"1048","DOI":"10.1145\/48529.48530","volume":"31","author":"J.H. Fetzer","year":"1988","unstructured":"Fetzer, J.H.: Program verification: The very idea. Communications of the ACM\u00a031(9), 1048\u20131063 (1988)","journal-title":"Communications of the ACM"},{"key":"20_CR7","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: A Mechanised Logic of Computation","author":"M.J. Gordon","year":"1979","unstructured":"Gordon, M.J., Milner, A.J., Wadsworth, C.P.: Edinburgh LCF: A Mechanised Logic of Computation. LNCS, vol.\u00a078. Springer, Heidelberg (1979)"},{"issue":"1\/2","key":"20_CR8","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/BF01128406","volume":"8","author":"J. Guttman","year":"1995","unstructured":"Guttman, J., Ramsdell, J., Wand, M.: VLISP: A verified implementation of Scheme. Lisp and Symbolic Computation\u00a08(1\/2), 5\u201332 (1995)","journal-title":"Lisp and Symbolic Computation"},{"key":"20_CR9","unstructured":"Harrison, J.: Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-053, SRI Cambridge, Cambridge, UK (1995)"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/BFb0055135","volume-title":"Theorem Proving in Higher Order Logics","author":"J.V. Harrison","year":"1998","unstructured":"Harrison, J.V.: Formalizing basic first order model theory. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol.\u00a01479, pp. 153\u2013170. Springer, Heidelberg (1998)"},{"key":"20_CR11","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/11814771_17","volume-title":"Automated Reasoning","author":"J. Harrison","year":"2006","unstructured":"Harrison, J.: Towards self-verification of HOL light. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 177\u2013191. Springer, Heidelberg (2006)"},{"key":"20_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-642-03359-9_4","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"2009","unstructured":"Harrison, J.: HOL light: An overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 60\u201366. Springer, Heidelberg (2009)"},{"key":"20_CR13","volume-title":"Computer-Aided Reasoning: An Approach","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"20_CR14","volume-title":"POPL","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: Morrisett, J.G., Jones, S.L.P. (eds.) POPL. ACM, New York (2006)"},{"issue":"4","key":"20_CR15","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1145\/367177.367199","volume":"3","author":"J. McCarthy","year":"1960","unstructured":"McCarthy, J.: Recursive functions of symbolic expressions and their computation by machine, part 1. Communications of the ACM\u00a03(4), 184\u2013195 (1960)","journal-title":"Communications of the ACM"},{"key":"20_CR16","volume-title":"ICFP","author":"A. McCreight","year":"2010","unstructured":"McCreight, A., Chevalier, T., Tolmach, A.P.: A certified framework for compiling and executing garbage-collected languages. In: Hudak, P., Weirich, S. (eds.) ICFP. ACM, New York (2010)"},{"key":"20_CR17","volume-title":"POPL","author":"M.O. Myreen","year":"2010","unstructured":"Myreen, M.O.: Verified just-in-time compiler on x86. In: Hermenegildo, M.V., Palsberg, J. (eds.) POPL. ACM, New York (2010)"},{"key":"20_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-642-03359-9_25","volume-title":"Theorem Proving in Higher Order Logics","author":"M.O. Myreen","year":"2009","unstructured":"Myreen, M.O., Gordon, M.J.C.: Verified LISP implementations on ARM,\u00a0x86\u00a0and\u00a0powerPC. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 359\u2013374. Springer, Heidelberg (2009)"},{"key":"20_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-00722-4_2","volume-title":"Compiler Construction","author":"M.O. Myreen","year":"2009","unstructured":"Myreen, M.O., Slind, K., Gordon, M.J.C.: Extensible proof-producing compilation. In: de Moor, O., Schwartzbach, M.I. (eds.) CC 2009. LNCS, vol.\u00a05501, pp. 2\u201316. Springer, Heidelberg (2009)"},{"key":"20_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/11541868_19","volume-title":"Theorem Proving in Higher Order Logics","author":"T. Ridge","year":"2005","unstructured":"Ridge, T., Margetson, J.: A mechanically verified, sound and complete theorem prover for first order logic. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 294\u2013309. Springer, Heidelberg (2005)"},{"key":"20_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-540-71067-7_6","volume-title":"Theorem Proving in Higher Order Logics","author":"K. Slind","year":"2008","unstructured":"Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 28\u201332. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22863-6_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,31]],"date-time":"2019-03-31T02:54:28Z","timestamp":1554000868000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22863-6_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642228629","9783642228636"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22863-6_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}