{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,19]],"date-time":"2025-01-19T21:40:01Z","timestamp":1737322801799,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540678632"},{"type":"electronic","value":"9783540446590"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44659-1_8","type":"book-chapter","created":{"date-parts":[[2007,7,21]],"date-time":"2007-07-21T17:40:26Z","timestamp":1185039626000},"page":"108-125","source":"Crossref","is-referenced-by-count":9,"title":["A Prototype Proof Translator from HOL to Coq"],"prefix":"10.1007","author":[{"given":"Ewen","family":"Denney","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","unstructured":"[AHJ+OO]_A. Franke A, S.M. Hess, G.Ch. Jung, M. Kohlhase, and V. Sorge. Agent-oriented integration of distributed mathematical services. Journal of Universal Computer Science, 5, 2000."},{"key":"8_CR2","unstructured":"Henk Barendregt. The quest for correctness. Images of SMC research, pages 39\u201358, 1996. At ftp:\/\/ftp.cs.kun.nl\/pub\/CompMath.Found\/quest.ps.Z ."},{"key":"8_CR3","unstructured":"[BBC+97]_Bruno Barras, Samuel Boutin, Cristina Cornes, Jean-Christophe Filliatre, Eduardo Gim\u00e9nez, Hugo Herbelin, Gerard Huet, Cesar Mu\u00f1oz, Chetan Murthy, Catherine Parent, Christine Paulin-Mohring, Amokrane Saibi, and Benjamin Werner. The Coq Proof Assistant Reference Manual: Version 6.1. Technical Report RT-0203, Inria, May 1997."},{"key":"8_CR4","unstructured":"Robert S. Boyer and Gilles Dowek. Towards checking proof-checkers. In Workshop on Types for Proofs and Programs (Type\u2019 93), 1993."},{"key":"8_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/BFb0055131","volume-title":"Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics (TPHOLs\u201998)","author":"R. Boulton","year":"1998","unstructured":"R. Boulton, K. Slind, A. Bundy, and M. Gordon. An interface between CLAM and HOL. In J. Grundy and M. Newey, editors, Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics (TPHOLs\u201998), volume 1479 of Lecture Notes in Computer Science, pages 87\u2013104, Canberra, Australia, September\/October 1998. Springer-Verlag."},{"key":"8_CR6","unstructured":"O. Caprotti, D.P. Carlisle, and A.M. Cohen. Draft of the Open Math standard. The Open Math Society, 1999. http:\/\/www.nag.co.uk\/projects\/openmath\/omsoc\/ ."},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"A. P. Felty and D. J. Howe. Hybrid interactive theorem proving using Nuprl and HOL. In William McCune, editor, Proceedings of the 14th International Conference on Automated deduction, volume 1249 of LNAI, pages 351\u2013365, Berlin, July 13\u201317 1997. Springer-Verlag.","DOI":"10.1007\/3-540-63104-6_34"},{"key":"8_CR8","unstructured":"M. J. C. Gordon and Thomas F. Melham, editors. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993."},{"key":"8_CR9","unstructured":"Fausto Giunchiglia, Paolo Pecchiari, and Carolyn Talcott. Reasoning theories: Towards an architecture for open mechanized reasoning systems. Technical Note CS-TN-94-15, Stanford University, Department of Computer Science, December 1994."},{"key":"8_CR10","unstructured":"Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. In Symposium on Logic in Computer Science, Ithaca, NY, pages 194\u2013204. IEEE, June 1987."},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Necula and Lee. Efficient representation and validation of proofs. In LICS: IEEE Symposium on Logic in Computer Science, pages 93\u2013104, 1998.","DOI":"10.1109\/LICS.1998.705646"},{"issue":"2","key":"8_CR12","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1023\/A:1008643803725","volume":"14","author":"W. Wong","year":"1999","unstructured":"Wai Wong. Validation of HOL proofs by proof checking. Formal Methods in System Design: An International Journal, 14(2):193\u2013212, March 1999.","journal-title":"Formal Methods in System Design: An International Journal"},{"key":"8_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1007\/BFb0028403","volume-title":"Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics, TPHOLs\u201997, Murray Hill, NJ, USA","author":"V. Zammit","year":"1997","unstructured":"Vincent Zammit. A comparative study of Coq and HOL. In Elsa L. Gunter and Amy Felty, editors, Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics, TPHOLs\u201997, Murray Hill, NJ, USA, volume 1275 of Lecture Notes in Computer Science, pages 323\u2013337. Springer-Verlag, August 1997."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44659-1_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,19]],"date-time":"2025-01-19T21:22:29Z","timestamp":1737321749000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44659-1_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540678632","9783540446590"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-44659-1_8","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}