{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:09Z","timestamp":1774837809346,"version":"3.50.1"},"publisher-location":"Berlin\/Heidelberg","reference-count":14,"publisher":"Springer-Verlag","isbn-type":[{"value":"354019343X","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0012835","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T06:12:39Z","timestamp":1132726359000},"page":"238-257","source":"Crossref","is-referenced-by-count":24,"title":["Computational metatheory in Nuprl"],"prefix":"10.1007","author":[{"given":"Douglas J.","family":"Howe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"16_CR1","volume-title":"Foundations of Constructive Analysis","author":"E. Bishop","year":"1967","unstructured":"Errett Bishop. Foundations of Constructive Analysis. McGraw-Hill, New York, 1967."},{"key":"16_CR2","unstructured":"R. S. Boyer and J Strother Moore. Metafunctions: proving them correct and using them efficiently as new proof procedures. In R. S. Boyer and J Strother Moore, editors, The Correctness Problem in Computer Science, chapter 3, Academic Press, 1981."},{"key":"16_CR3","unstructured":"Robert L. Constable and Scott F. Smith. Partial objects in constructive type theory. In Proceedings of the Second Annual Symposium on Logic in Computer Science, IEEE, 1987."},{"key":"16_CR4","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"R. L. Constable","year":"1986","unstructured":"Robert L. Constable, et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs, New Jersey, 1986."},{"key":"16_CR5","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0898-1221(79)90044-0","volume":"5","author":"M. Davis","year":"1979","unstructured":"Martin Davis and Jacob T. Schwartz. Metamathematical extensibility for theorem verifiers and proof-checkers. Computers and Mathematics with Applications, 5:217\u2013230, 1979.","journal-title":"Computers and Mathematics with Applications"},{"key":"16_CR6","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1007\/BFb0060623","volume-title":"Symposium on Automatic Demonstration","author":"N.G. Bruijn de","year":"1970","unstructured":"N.G. de Bruijn. The mathematical language AUTOMATH, its usage and some of its extensions. In Symposium on Automatic Demonstration, Lecture Notes in Mathematics vol. 125, pages 29\u201361, Springer-Verlag, New York, 1970."},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Michael J. Gordon, Robin Milner, and Christopher P. Wadsworth. Edinburgh LCF: A Mechanized Logic of Computation. Volume 78 of Lecture Notes in Computer Science, Springer-Verlag, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"16_CR8","unstructured":"Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. In The Second Annual Symposium on Logic in Computer Science, IEEE, 1987."},{"key":"16_CR9","unstructured":"Douglas J. Howe. Automating Reasoning in an Implementation of Constructive Type Theory. PhD thesis, Cornell University, 1988."},{"key":"16_CR10","unstructured":"Todd B. Knoblock. Metamathematical Extensibility in Type Theory. PhD thesis, Cornell University, 1987."},{"key":"16_CR11","unstructured":"Todd B. Knoblock and Robert L. Constable. Formalized metareasoning in type theory. In Proceedings of the First Annual Symposium on Logic in Computer Science, IEEE, 1986."},{"key":"16_CR12","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1016\/S0049-237X(09)70189-2","volume-title":"Sixth International Congress for Logic, Methodology, and Philosophy of Science","author":"P. Martin-L\u00f6f","year":"1982","unstructured":"Per Martin-L\u00f6f. Constructive mathematics and computer programming. In Sixth International Congress for Logic, Methodology, and Philosophy of Science, pages 153\u2013175, North Holland, Amsterdam, 1982."},{"key":"16_CR13","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/0167-6423(83)90008-4","volume":"3","author":"L. C. Paulson","year":"1983","unstructured":"Lawrence C. Paulson. A higher-order implementation of rewriting. Science of Computer Programming, 3:119\u2013149, 1983.","journal-title":"Science of Computer Programming"},{"key":"16_CR14","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/0004-3702(80)90015-6","volume":"13","author":"R. W. Weyhrauch","year":"1980","unstructured":"Richard W. Weyhrauch. Prolegomena to a theory of formal reasoning. Artificial Intelligence, 13:133\u2013170, 1980.","journal-title":"Artificial Intelligence"}],"container-title":["Lecture Notes in Computer Science","9th International Conference on Automated Deduction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0012835.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,7]],"date-time":"2020-12-07T15:06:39Z","timestamp":1607353599000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0012835"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354019343X"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/bfb0012835","relation":{},"subject":[]}}