{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,5]],"date-time":"2026-10-05T16:52:58Z","timestamp":1791219178265,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540425250","type":"print"},{"value":"9783540447559","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44755-5_23","type":"book-chapter","created":{"date-parts":[[2007,8,10]],"date-time":"2007-08-10T06:03:32Z","timestamp":1186725812000},"page":"329-345","source":"Crossref","is-referenced-by-count":26,"title":["The HOL\/NuPRL Proof Translator"],"prefix":"10.1007","author":[{"given":"Pavel","family":"Naumov","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mark-Oliver","family":"Stehr","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2001,8,24]]},"reference":[{"key":"23_CR1","unstructured":"B. Barras et al. The Coq Proof Assistant Reference Manual: Version 6.1. Technical Report RT-0203, INRIA, May 1997."},{"key":"23_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/3-540-44659-1_3","volume-title":"13th International Conference on Theorem Proving in Higher Order Logics","author":"S. Berghofer","year":"2000","unstructured":"S. Berghofer and T. Nipkow. Proof terms for simply typed higher order logic. In M. Aagaard and J. Harrison, editors, 13th International Conference on Theorem Proving in Higher Order Logics, volume 1869 of Lecture Notes in Computer Science, pages 38\u201352, Portland, Oregon, August 2000. Springer."},{"key":"23_CR3","unstructured":"R.L. Constable et al. Implementing Mathematics with Nuprl Proof Development System. Prentice Hall, 1986."},{"issue":"2\/3","key":"23_CR4","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"T. Coquand and G. Huet. The calculus of constructions. Information and Computation, 76(2\/3):95\u2013120, 1988.","journal-title":"Information and Computation"},{"key":"23_CR5","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N.G. Bruijn de","year":"1972","unstructured":"N.G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indag. Math., 34:381\u2013392, 1972.","journal-title":"Indag. Math."},{"key":"23_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-44659-1_8","volume-title":"The 13th International Conference on Theorem Proving in Higher Order Logics","author":"E. Denney","year":"2000","unstructured":"E. Denney. A Prototype Proof Translator from HOL to Coq. In M. Aagaard and J. Harrison, editors, The 13th International Conference on Theorem Proving in Higher Order Logics, volume 1869 of Lecture Notes in Computer Science, pages 108\u2013125, Portland, Oregon, August 2000. Springer-Verlag."},{"key":"23_CR7","doi-asserted-by":"crossref","unstructured":"A.P. Felty and D.J. Howe. Hybrid interactive theorem proving using Nuprl and HOL. In W. McCune, editor, Automated Deduction-CADE-14, volume 1249 of Lecture Notes in Artificial Intelligence, pages 351\u2013365, Berlin, 1997. Springer-Verlag.","DOI":"10.1007\/3-540-63104-6_34"},{"issue":"1","key":"23_CR8","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1145\/147508.147524","volume":"39","author":"J. Goguen","year":"1992","unstructured":"J. Goguen and R. Burstall. Institutions: Abstract model theory for specification and programming. Journal of the ACM, 39(1):95\u2013146, 1992.","journal-title":"Journal of the ACM"},{"key":"23_CR9","unstructured":"M.J.C. Gordon and T.F. Melham. Introduction to HOL-A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993."},{"key":"23_CR10","unstructured":"D. J. Howe. A classical set-theoretic model of polymorphic extensional type theory. Manuscript."},{"key":"23_CR11","series-title":"Lect Notes Comput Sci","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":"D.J. Howe. Importing mathematics from HOL into Nuprl. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics, volume 1125 of Lecture Notes in Computer Science, pages 267\u2013282, Berlin, 1996. Springer-Verlag."},{"key":"23_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/BFb0014309","volume-title":"Algebraic Methodology and Software Technology","author":"D.J. Howe","year":"1996","unstructured":"D.J Howe. Semantics foundation for embedding HOL in Nuprl. In M. Wirsing and A. Nivat, editors, Algebraic Methodology and Software Technology, volume 1101 of Lecture Notes in Computer Science, pages 85\u2013101, Berlin, 1996. Springer-Verlag."},{"key":"23_CR13","unstructured":"P. Martin-L\u00f6f. Intuitionistic Type Theory. Bibliopolis, Napoli, 1984."},{"key":"23_CR14","doi-asserted-by":"crossref","unstructured":"J. Meseguer. General logics. In H.-D. Ebbinghaus et al., editor, Logical Colloquium, 1987, pages 275\u2013329. North-Holland, 1989.","DOI":"10.1016\/S0049-237X(08)70132-0"},{"key":"23_CR15","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2319.001.0001","volume-title":"The Definition of Standard ML (Revised)","author":"R. Milner","year":"1997","unstructured":"R. Milner, M. Tofte, R.M. Harper, and D.B. MacQueen. The Definition of Standard ML (Revised). MIT Press, Cambridge, 1997."},{"key":"23_CR16","unstructured":"G. Mints. A Short Introduction to Intuitionistic Logic. Kluwer Academic\/Plenum Publishers, 2000."},{"key":"23_CR17","unstructured":"P. Naumov. Importing Isabelle Formal Mathematics into NuPRL. In Supplemental proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics, Nice, France, September 1999."},{"key":"23_CR18","unstructured":"P. Naumov. Formalization of Isabelle Meta Logic in NuPRL. In Supplemental proceedings of the 13th International Conference on Theorem Proving in Higher Order Logics, pages 141\u2013156, Portland, OR, August 2000."},{"key":"23_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle-A Generic Theorem Prover","author":"L.C. Paulson","year":"1994","unstructured":"L.C. Paulson. Isabelle-A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1994."},{"key":"23_CR20","series-title":"International Series of Monographs on Computer Science","volume-title":"Programming in Martin-L\u00f6f\u2019s Type Theory. An Introduction","author":"K. Petersson","year":"1990","unstructured":"K. Petersson, J. Smith, and B. Nordstroem. Programming in Martin-L\u00f6f\u2019s Type Theory. An Introduction. International Series of Monographs on Computer Science. Oxford: Clarendon Press, 1990."},{"key":"23_CR21","unstructured":"M.-O. Stehr, P. Naumov, and J. Meseguer. A proof-theoretic approach to HOL-Nuprl connection with applications to proof translation (full version). \n                    http:\/\/cs.hbg.psu.edu\/~naumov\/Papers\/holnuprl.ps\n                    \n                  , March 2000."},{"key":"23_CR22","unstructured":"M.-O. Stehr, P. Naumov, and J. Meseguer. A proof-theoretic approach to HOL-Nuprl connection with applications to proof translation. In 15th International Workshop on Algebraic Development Techniques, Genova, Italy, April 2001. To appear. See [21] for the full version."},{"issue":"2","key":"23_CR23","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1023\/A:1008643803725","volume":"14","author":"W. Wong","year":"1999","unstructured":"W. Wong. Validation of HOL proofs by proof checking. Formal Methods in System Design: An International Journal, 14(2):193\u2013212, 1999.","journal-title":"Formal Methods in System Design: An International Journal"}],"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-44755-5_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,21]],"date-time":"2019-02-21T02:22:18Z","timestamp":1550715738000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44755-5_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540425250","9783540447559"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-44755-5_23","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2001]]}}}