{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T19:10:11Z","timestamp":1736536211465,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":9,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540649878"},{"type":"electronic","value":"9783540498018"}],"license":[{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0055138","type":"book-chapter","created":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T09:09:13Z","timestamp":1153991353000},"page":"207-224","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A type annotation scheme for Nuprl"],"prefix":"10.1007","author":[{"given":"Douglas J.","family":"Howe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,5,27]]},"reference":[{"key":"13_CR1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1007\/3-540-61042-1_48","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C.-T. Chou","year":"1996","unstructured":"C.-T. Chou and D. Peled. Verifying a model-checking algorithm. In Tools and Algorithms for the Construction and Analysis of Systems, number 1055 in LNCS, pages 241\u2013257, Passau, Germany, 1996. Springer-Verlag."},{"key":"13_CR2","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"R. L. Constable","year":"1986","unstructured":"R. L. Constable, et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs, New Jersey, 1986."},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"A. Felty, D. Howe, and F. Stomp. Protocol verification in nuprl. In CAV'98, Lecture Notes in Computer Science. Springer-Verlag, 1998.","DOI":"10.1007\/BFb0028764"},{"key":"13_CR4","volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher Order Logic","author":"M. J. C. Gordon","year":"1993","unstructured":"M. J. C. Gordon and T. F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge, UK, 1993."},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"D. J. Howe. On computational open-endedness in Martin-L\u00f6f's type theory. In Proceedings of the Sixth Annual Symposium on Logic in Computer Science, pages 162\u2013172. IEEE Computer Society, 1991.","DOI":"10.1109\/LICS.1991.151641"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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 foundations for embedding HOL in Nuprl. In M. Wirsing and M. Nivat, editors, Algebraic Methodology and Software Technology, volume 1101 of Lecture Notes in Computer Science, pages 85\u2013101, Berlin, 1996. Springer-Verlag."},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"P. B. Jackson. Exploring abstract algebra in constructive type theory. In A. Bundy, editor, 12th Conference on Automated Deduction, Lecture Notes in Artifical Intelligence. Springer, June 1994.","DOI":"10.1007\/3-540-58156-1_43"},{"key":"13_CR8","unstructured":"S. Owre and N. Shankar. The formal semantics of PVS. Technical report, SRI, August 1997."},{"key":"13_CR9","unstructured":"B. Werner. Sets in types, types in sets. In International Symposium on Theoretical Aspects of Computer Software."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0055138","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T03:14:36Z","timestamp":1736478876000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0055138"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540649878","9783540498018"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/bfb0055138","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]},"assertion":[{"value":"27 May 2006","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}