{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T19:45:22Z","timestamp":1770752722665,"version":"3.50.0"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540676645","type":"print"},{"value":"9783540451013","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10721959_12","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T16:12:31Z","timestamp":1167408751000},"page":"170-176","source":"Crossref","is-referenced-by-count":22,"title":["The Nuprl Open Logical Environment"],"prefix":"10.1007","author":[{"given":"Stuart F.","family":"Allen","sequence":"first","affiliation":[]},{"given":"Robert L.","family":"Constable","sequence":"additional","affiliation":[]},{"given":"Rich","family":"Eaton","sequence":"additional","affiliation":[]},{"given":"Christoph","family":"Kreitz","sequence":"additional","affiliation":[]},{"given":"Lori","family":"Lorigo","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"M. Aagaard","year":"1993","unstructured":"Aagaard, M., Leeser, M.: Verifying a logic synthesis tool in Nuprl. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol.\u00a0663. pp. 72-83. Springer, Heidelberg (1993)"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"252","DOI":"10.1007\/3-540-63104-6_23","volume-title":"Automated Deduction - CADE-14","author":"C. Benzmiiller","year":"1997","unstructured":"Benzmiiller, C., et al.: \u03a9mega: Towards a mathematical assistant. In: McCune, W. (ed.) CADE 1997. LNCS, vol.\u00a01249, pp. 252\u2013256. Springer, Heidelberg (1997)"},{"key":"12_CR3","volume-title":"Imple meriting Mathematics with the NuPRL proof development system","author":"R. Constable","year":"1986","unstructured":"Constable, R., et al.: Implemeriting Mathematics with the NuPRL proof development system. Prentice Hall, Englewood Cliffs (1986)"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1684","DOI":"10.1007\/3-540-48118-4_39","volume-title":"FM\u201999 - Formal Methods","author":"M. Clavel","year":"1999","unstructured":"Clavel, M., Duran, F., Eker, S., Meseguer, J., Stehr, M.-O.: Maude as a formal meta-tool. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol.\u00a01709, pp. 1684\u20131703. Springer, Heidelberg (1999)"},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/3-540-48685-2_18","volume-title":"Rewriting Techniques and Applications","author":"M. Clavel","year":"1999","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Quesada, J.F.: The Maude system. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol.\u00a01631, pp. 240\u2013243. Springer, Heidelberg (1999)"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1007\/3-540-63104-6_34","volume-title":"Automated Deduction - CADE-14","author":"A. Felty","year":"1997","unstructured":"Felty, A., Howe, D.: Hybrid Interactive Theorem Proving using Nuprl and HOL. In: McCune, W. (ed.) CADE 1997. LNCS, vol.\u00a01249, pp. 351\u2013365. Springer, Heidelberg (1997)"},{"key":"12_CR7","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, Cambridge (1993)"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1007\/BFb0105410","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Howe","year":"1996","unstructured":"Howe, D.: Importing mathematics from HOL into NuPRL. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol.\u00a01125, pp. 267\u2013282. Springer, Heidelberg (1996)"},{"key":"12_CR9","series-title":"Department of Computer Science","volume-title":"The Nuprl Proof Development System","author":"P. Jackson","year":"1994","unstructured":"Jackson, P.: The Nuprl Proof Development System. Version 4-2, Department of Computer Science. Cornell University, Ithica (1994)"},{"key":"12_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/BFb0054269","volume-title":"Automated Deduction - CADE-15","author":"C. Kreitz","year":"1998","unstructured":"Kreitz, C., Hayden, M., Hickey, J.: A proof environment for the development of group communication systems. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol.\u00a01421, pp. 317\u2013332. Springer, Heidelberg (1998)"},{"key":"12_CR11","unstructured":"Kreitz, C.: Formal reasoning about communication systems I: Embedding ML into type theory. Technical Report TR97-1637. Cornell University. Department of Computer Science (1997)"},{"key":"12_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/3-540-49059-0_8","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"C. Kreitz","year":"1999","unstructured":"Kreitz, C.: Automated fast-track reconfiguration of group communication systems. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 104\u2013118. Springer, Heidelberg (1999)"},{"key":"12_CR13","volume-title":"Intellectics and Computational Logic","author":"C. Kreitz","year":"2000","unstructured":"Kreitz, C., Otten, J., Schmitt, S., Pientka, B.: Matrix-based Constructive Theorem Proving. In: Intellectics and Computational Logic. Kluwer, Dordrecht (2000)"},{"issue":"5","key":"12_CR14","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1145\/319344.319157","volume":"34","author":"X. Liu","year":"1999","unstructured":"Liu, X., Kreitz, C., van Renesse, R., Hickey, J., Hayden, M., Birman, K., Constable, R.: Building reliable, high-performance communication systems from components. SOSP 1999, Operating Systems Review\u00a034(5), 80\u201392 (1999)","journal-title":"SOSP 1999, Operating Systems Review"},{"key":"12_CR15","unstructured":"The MathBus Term Structure, http:\/\/www.cs.Cornell.edu\/simlab\/papers\/mathbus\/mathTerm.htm"},{"key":"12_CR16","unstructured":"Metaprl home page, http:\/\/ensembleOl.cs.Cornell.edu:12000\/cvsweb\/meta-prl"},{"key":"12_CR17","unstructured":"Martin-L\u00f6f, P.: Intuitionistic Type Theory. Bibliopolis (1984)"},{"key":"12_CR18","unstructured":"Naumov, P.: Publishing formal mathematics on the web. Technical Report TR98-1689. Cornell University. Department of Computer Science (1998)"},{"key":"12_CR19","unstructured":"Naumov, P.: Importing Isabelle formal mathematics into Nuprl. Technical Report TR99-1734. Cornell University. Department of Computer Science (1999)"},{"key":"12_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/3-540-61474-5_91","volume-title":"Computer Aided Verification","author":"S. Owre","year":"1996","unstructured":"Owre, S.: PVS: Combining specification, proof checking and model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 411\u2013414. Springer, Heidelberg (1996)"},{"key":"12_CR21","first-page":"361","volume-title":"Logic and Computer Science","author":"L.C. Paulson","year":"1990","unstructured":"Paulson, L.C.: Isabelle: The next 700 theorem provers. In: Logic and Computer Science, pp. 361\u2013386. Academic Press, London (1990)"},{"key":"12_CR22","doi-asserted-by":"crossref","unstructured":"Srinivas, Y.V., J\u00fcllig, R.: SPECWARE: Formal Support for composing software. In Mathematics of Program Construction (1995)","DOI":"10.1007\/3-540-60117-1_22"},{"key":"12_CR23","volume-title":"Mathematica: A System for Doing Mathematics by Computer","author":"S. Wolfram","year":"1988","unstructured":"Wolfram, S.: Mathematica: A System for Doing Mathematics by Computer. Addison Wesley, Reading (1988)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-17"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10721959_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,23]],"date-time":"2019-04-23T07:42:30Z","timestamp":1556005350000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10721959_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676645","9783540451013"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/10721959_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2000]]}}}