{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:00:41Z","timestamp":1725559241642},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642140518"},{"type":"electronic","value":"9783642140525"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14052-5_22","type":"book-chapter","created":{"date-parts":[[2010,7,12]],"date-time":"2010-07-12T10:23:14Z","timestamp":1278930194000},"page":"307-322","source":"Crossref","is-referenced-by-count":27,"title":["Importing HOL Light into Coq"],"prefix":"10.1007","author":[{"given":"Chantal","family":"Keller","sequence":"first","affiliation":[]},{"given":"Benjamin","family":"Werner","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","unstructured":"Our implementation, http:\/\/perso.ens-lyon.fr\/chantal.keller\/Recherche\/hollightcoq.html"},{"key":"22_CR2","unstructured":"Dedukti, a universal proof checker, http:\/\/www.lix.polytechnique.fr\/dedukti"},{"key":"22_CR3","unstructured":"The Flyspeck project, http:\/\/www.flyspeck-blog.blogspot.com"},{"key":"22_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"Theorem Proving in Higher Order Logics","year":"2000","unstructured":"Aagaard, M., Harrison, J. (eds.): TPHOLs 2000. LNCS, vol.\u00a01869. Springer, Heidelberg (2000)"},{"key":"22_CR5","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1145\/1328438.1328443","volume-title":"POPL","author":"B. Aydemir","year":"2008","unstructured":"Aydemir, B., Chargu\u00e9raud, A., Pierce, B., Pollack, R., Weirich, S.: Engineering formal metatheory. In: Necula, G., Wadler, P. (eds.) POPL, pp. 3\u201315. ACM, New York (2008)"},{"key":"22_CR6","unstructured":"Barras, B., Boutin, S., Cornes, C., Courant, J., Filliatre, J., Gimenez, E., Herbelin, H., Huet, G., Munoz, C., Murthy, C., et al.: The Coq proof assistant: reference manual. Rapport technique - INRIA (2000)"},{"key":"22_CR7","first-page":"203","volume-title":"LICS","author":"U. Berger","year":"1991","unstructured":"Berger, U., Schwichtenberg, H.: An inverse of the evaluation functional for typed lambda-calculus. In: LICS, pp. 203\u2013211. IEEE Computer Society, Los Alamitos (1991)"},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"Berghofer, S., Nipkow, T.: Proof terms for simply typed higher order logic. In: Aagaard, Harrison: [4], pp. 38\u201352","DOI":"10.1007\/3-540-44659-1_3"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Denney, E.: A prototype proof translator from hol to coq. In: Aagaard, Harrison: [4], pp. 108\u2013125","DOI":"10.1007\/3-540-44659-1_8"},{"key":"22_CR10","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/1159876.1159880","volume-title":"ML","author":"J.C. Filli\u00e2tre","year":"2006","unstructured":"Filli\u00e2tre, J.C., Conchon, S.: Type-safe modular hash-consing. In: Kennedy, A., Pottier, F. (eds.) ML, pp. 12\u201319. ACM, New York (2006)"},{"key":"22_CR11","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Reasoning","year":"2006","unstructured":"Furbach, U., Shankar, N. (eds.): IJCAR 2006. LNCS (LNAI), vol.\u00a04130. Springer, Heidelberg (2006)"},{"key":"22_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-540-74591-4_27","volume-title":"Theorem Proving in Higher Order Logics","author":"F. Garillot","year":"2007","unstructured":"Garillot, F., Werner, B.: Simple types in type theory: Deep and shallow encodings. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 368\u2013382. Springer, Heidelberg (2007)"},{"key":"22_CR13","unstructured":"Gonthier, G., Mahboubi, A.: A Small Scale Reflection Extension for the Coq system. Tech. rep., INRIA (2007)"},{"key":"22_CR14","volume-title":"Introduction to HOL: A theorem proving environment for higher order logic","author":"M. Gordon","year":"1993","unstructured":"Gordon, M., Melham, T.: Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, New York (1993)"},{"key":"22_CR15","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":"22_CR16","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1007\/11814771_17","volume-title":"Automated Reasoning","author":"John Harrison","year":"2006","unstructured":"Harrison, J.: Towards self-verification of HOL Light. In: Furbach, Shankar: [11], pp. 177\u2013191"},{"key":"22_CR17","unstructured":"Hurd, J.: OpenTheory: Package Management for Higher Order Logic Theories. In: PLMMS\u201909, p. 31 (2009)"},{"key":"22_CR18","unstructured":"Leroy, X.: The OCaml Programming Language (1998)"},{"key":"22_CR19","doi-asserted-by":"crossref","unstructured":"Obua, S., Skalberg, S.: Importing HOL into Isabelle\/HOL. In: Furbach, Shankar: [11], pp. 298\u2013302","DOI":"10.1007\/11814771_27"},{"key":"22_CR20","unstructured":"Wiedijk, F.: Encoding the HOL Light logic in Coq. Unpublished notes (2007)"},{"key":"22_CR21","series-title":"Lecture Notes in Computer Science","first-page":"353","volume-title":"TPHOLs","author":"W. Wong","year":"1995","unstructured":"Wong, W.: Recording and checking HOL proofs. In: Schubert, E., Windley, P., Alves-Foss, J. (eds.) TPHOLs 1995. LNCS, vol.\u00a0971, pp. 353\u2013368. Springer, Heidelberg (1995)"},{"key":"22_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/BFb0028403","volume-title":"Theorem Proving in Higher Order Logics","author":"V. Zammit","year":"1997","unstructured":"Zammit, V.: A comparative study of Coq and HOL. In: Gunter, E., Felty, A. (eds.) TPHOLs 1997. LNCS, vol.\u00a01275, pp. 323\u2013337. Springer, Heidelberg (1997)"}],"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-14052-5_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,1]],"date-time":"2023-06-01T21:47:08Z","timestamp":1685656028000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14052-5_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642140518","9783642140525"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14052-5_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}