{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T17:33:10Z","timestamp":1725471190068},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540371878"},{"type":"electronic","value":"9783540371885"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11814771_27","type":"book-chapter","created":{"date-parts":[[2006,10,5]],"date-time":"2006-10-05T15:44:21Z","timestamp":1160063061000},"page":"298-302","source":"Crossref","is-referenced-by-count":35,"title":["Importing HOL into Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"Steven","family":"Obua","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sebastian","family":"Skalberg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"27_CR1","series-title":"Lecture Notes in Computer Science","volume-title":"Theorem Proving in Higher Order Logics","year":"1996","unstructured":"von Wright, J., Harrison, J., Grundy, J. (eds.): TPHOLs 1996. LNCS, vol.\u00a01125. Springer, Heidelberg (1996)"},{"key":"27_CR2","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C. Sch\u00fcrmann","year":"2005","unstructured":"Sch\u00fcrmann, C., Stehr, M.: An Executable Formalization of the HOL\/Nuprl Connection in the Metalogical Framework Twelf. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, Springer, Heidelberg (2005)"},{"key":"27_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44755-5_23","volume-title":"Theorem Proving in Higher Order Logics","author":"P. Naumov","year":"2001","unstructured":"Naumov, P., Stehr, M., Meseguer, J.: The HOL\/NuPRL Proof Translator: A Practical Approach to Formal Interoperability. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol.\u00a02152, Springer, Heidelberg (2001)"},{"key":"27_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"Theorem Proving in Higher Order Logics","author":"P. Naumov","year":"1999","unstructured":"Naumov, P.: Importing Isabelle Formal Mathematics into NuPRL. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, Springer, Heidelberg (1999)"},{"key":"27_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44659-1_8","volume-title":"Theorem Proving in Higher Order Logics","author":"E. Denney","year":"2000","unstructured":"Denney, E.: A Prototype Proof Translator from HOL to Coq. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol.\u00a01869, Springer, Heidelberg (2000)"},{"key":"27_CR6","unstructured":"Wiedijk, F.: Encoding the HOL Light logic in Coq. Unpublished notes"},{"key":"27_CR7","unstructured":"McLaughlin, S.: An interpretation of Isabelle\/HOL in HOL Light (submitted)"},{"key":"27_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44659-1_3","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Berghofer","year":"2000","unstructured":"Berghofer, S., Nipkow, T.: Proof terms for simply typed higher order logic. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol.\u00a01869, Springer, Heidelberg (2000)"},{"key":"27_CR9","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002)"},{"key":"27_CR10","unstructured":"The HOL System Description, \n                    \n                      http:\/\/hol.sourceforge.net"},{"key":"27_CR11","unstructured":"Harrison, J.: The HOL Light manual, \n                    \n                      http:\/\/www.cl.cam.ac.uk\/users\/jrh\/hol-light\/manual-1.1.pdf"},{"key":"27_CR12","unstructured":"Obua, S.:\n                    \n                      http:\/\/www4.in.tum.de\/~obua\/importer"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11814771_27.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:27:35Z","timestamp":1619508455000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11814771_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540371878","9783540371885"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/11814771_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}