{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T17:33:09Z","timestamp":1725471189817},"publisher-location":"Berlin, Heidelberg","reference-count":33,"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_18","type":"book-chapter","created":{"date-parts":[[2006,10,5]],"date-time":"2006-10-05T15:44:21Z","timestamp":1160063061000},"page":"192-204","source":"Crossref","is-referenced-by-count":8,"title":["An Interpretation of Isabelle\/HOL in HOL Light"],"prefix":"10.1007","author":[{"given":"Sean","family":"McLaughlin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"18_CR1","unstructured":"http:\/\/www.cs.cmu.edu\/~seanmcl\/projects\/logosphere\/isabelle-holl"},{"key":"18_CR2","unstructured":"Avigad, J., Donnelly, K., Gray, D., Raff, P.: A formally verified proof of the prime number theorem. To appear in the ACM Transactions on Computational Logic"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"Ballarin, C.: Locales and locale expressions in Isabelle\/Isar. In: B., S., et al. (eds.) Types for Proofs and Programs: International Workshop (2003)","DOI":"10.1007\/978-3-540-24849-1_3"},{"key":"18_CR4","volume-title":"Texts in Theoretical Computer Science","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Coq\u00c1rt: The Calculus of Inductive Constructions. In: Texts in Theoretical Computer Science, Springer, Heidelberg (2004)"},{"key":"18_CR5","first-page":"589","volume-title":"To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism","author":"N.G. Bruijn de","year":"1980","unstructured":"de Bruijn, N.G.: A survey of the project AUTOMATH. In: Seldin, J.P., Hindley, J.R. (eds.) To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism, pp. 589\u2013606. Academic Press, London (1980)"},{"key":"18_CR6","volume-title":"Implementing Mathematics with The Nuprl Proof Development System","author":"R. Constable","year":"1986","unstructured":"Constable, R.: Implementing Mathematics with The Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs (1986)"},{"key":"18_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1007\/BFb0105410","volume-title":"Theorem Proving in Higher Order Logics","author":"D.J. Howe","year":"1996","unstructured":"Howe, D.J.: Importing mathematics from HOL into Nuprl. In: Von Wright, J., Grundy, J., Harrison, J. (eds.) TPHOLs 1996. LNCS, vol.\u00a01125, pp. 267\u2013282. Springer, Heidelberg (1996)"},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1007\/3-540-63104-6_34","volume-title":"Fourteenth International Conference on Automated Deduction","author":"A.P. Felty","year":"1997","unstructured":"Felty, A.P., Howe, D.J.: Hybrid interactive theorem proving using Nuprl and HOL. In: WebDB 2000. LNCS, pp. 351\u2013365. Springer, Heidelberg (1997)"},{"key":"18_CR9","unstructured":"Gonthier, G.: A computer-checked proof of the four colour theorem (2005), Available on the Web via http:\/\/research.microsoft.com\/~gonthier\/"},{"key":"18_CR10","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":"18_CR11","unstructured":"Hales, T.: The Flyspeck Project fact sheet. Project description (2005), available at http:\/\/www.math.pitt.edu\/~thales\/flyspeck\/"},{"key":"18_CR12","unstructured":"Hales, T.: The Jordan Curve Theorem in HOL Light. Source code (2005), available at http:\/\/www.math.pitt.edu\/~thales\/"},{"key":"18_CR13","doi-asserted-by":"publisher","first-page":"1065","DOI":"10.4007\/annals.2005.162.1065","volume":"162","author":"T.C. Hales","year":"2005","unstructured":"Hales, T.C.: A proof of the the Kepler conjecture. Annals of Mathematics\u00a0162, 1065\u20131185 (2005)","journal-title":"Annals of Mathematics"},{"key":"18_CR14","first-page":"194","volume-title":"Proceedings of the Second Annual Symposium on Logic in Computer Science","author":"R. Harper","year":"1987","unstructured":"Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. In: Proceedings of the Second Annual Symposium on Logic in Computer Science, Ithaca, NY, pp. 194\u2013204. IEEE Computer Society Press, Los Alamitos (1987)"},{"key":"18_CR15","volume-title":"Advanced Topics in Types and Programming Languages","author":"R. Harper","year":"2005","unstructured":"Harper, R., Pierce, B.C.: Design issues in advanced module systems. In: Pierce, B.C. (ed.) Advanced Topics in Types and Programming Languages, MIT Press, Cambridge (2005)"},{"key":"18_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (FMCAD 1996)","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":"18_CR17","unstructured":"Landau, E.: Grundlagen der Analysis. Leipzig, 1930. English translation by F. Steinhardt: Foundations of analysis: the arithmetic of whole, rational, irrational, and complex numbers. A supplement to textbooks on the differential and integral calculus, published by Chelsea; 3rd edition (1966)"},{"key":"18_CR18","doi-asserted-by":"crossref","unstructured":"McLaughlin, S., Barrett, C., Ge, Y.: Cooperating theorem provers: A case study combining CVC Lite and HOL Light. In: Armando, A., Cimatti, A. (eds.) Proceedings of the Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning, vol.\u00a0144, pp. 43\u201351 (2005)","DOI":"10.1016\/j.entcs.2005.12.005"},{"key":"18_CR19","volume-title":"The Definition of Standard ML","author":"R. Milner","year":"1990","unstructured":"Milner, R., Tofte, M., Harper, R.: The Definition of Standard ML. MIT Press, Cambridge (1990)"},{"key":"18_CR20","unstructured":"Naumov, P.: Importing Isabelle formal mathematics into Nuprl. Technical Report TR99-1734, Cornell University, 26 (1999)"},{"key":"18_CR21","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.-O., 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":"18_CR22","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Bauer, G., Schultz, P.: Flyspeck I: Tame Graphs. Technical report, Institut f\u00fcr Informatik, TU M\u00fcnchen (January 2006)","DOI":"10.1007\/11814771_4"},{"key":"18_CR23","doi-asserted-by":"crossref","unstructured":"Obua, S., Skalberg, S.: Importing HOL into Isabelle\/HOL (submitted, 2006)","DOI":"10.1007\/11814771_27"},{"key":"18_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"18_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: a generic theorem prover","author":"L.C. Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle. LNCS, vol.\u00a0828. Springer, Heidelberg (1994)"},{"key":"18_CR26","doi-asserted-by":"publisher","first-page":"1063","DOI":"10.1016\/B978-044450813-3\/50019-9","volume-title":"Handbook of Automated Reasoning","author":"F. Pfenning","year":"2001","unstructured":"Pfenning, F.: Logical frameworks. In: Handbook of Automated Reasoning, pp. 1063\u20131147. MIT Press, Cambridge (2001)"},{"key":"18_CR27","doi-asserted-by":"crossref","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: Twelf - a meta-logical framweork for deductive systems. In: Ganzinger, H. (ed.) Proceedings of the 16th International Conference on Automated Deduction, pp. 202\u2013206 (1999)","DOI":"10.1007\/3-540-48660-7_14"},{"key":"18_CR28","unstructured":"Pfenning, F., Sch\u00fcrmann, C., Kohlhase, M., Shankar, N., Owre, S.: The Logosphere Project (2005), Project description available at http:\/\/www.logosphere.org"},{"key":"18_CR29","doi-asserted-by":"crossref","unstructured":"Sch\u00fcrmann, C., Stehr, M.-O.: An Executable Formalization of the HOL\/NuPRL Connection in Twelf. In: 11th International Conference on Logic for Programming Artificial Intelligence and Reasoning (2005)","DOI":"10.1007\/11916277_11"},{"key":"18_CR30","unstructured":"Stehr, M.-O., Naumov, P., Meseguer, J.: A proof-theoretic approach to the HOL-NuPRL connection with applications to proof-translation. In: WADT\/CoFI (2001)"},{"key":"18_CR31","unstructured":"Weis, P., Leroy, X.: Le langage Caml. InterEditions (1993), see also the CAML Web page: http:\/\/pauillac.inria.fr\/caml\/"},{"key":"18_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/BFb0028402","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Wenzel","year":"1997","unstructured":"Wenzel, M.: Type Classes and Overloading in Higher-Order Logic. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol.\u00a01275, pp. 307\u2013322. Springer, Heidelberg (1997)"},{"key":"18_CR33","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)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11814771_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:14:31Z","timestamp":1605644071000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11814771_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540371878","9783540371885"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/11814771_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}