{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:48:11Z","timestamp":1767926891376,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":53,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540406648","type":"print"},{"value":"9783540451303","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/10930755_19","type":"book-chapter","created":{"date-parts":[[2006,6,19]],"date-time":"2006-06-19T15:27:09Z","timestamp":1150730829000},"page":"287-303","source":"Crossref","is-referenced-by-count":18,"title":["MetaPRL \u2013 A Modular Logical Environment"],"prefix":"10.1007","author":[{"given":"Jason","family":"Hickey","sequence":"first","affiliation":[]},{"given":"Aleksey","family":"Nogin","sequence":"additional","affiliation":[]},{"given":"Robert L.","family":"Constable","sequence":"additional","affiliation":[]},{"given":"Brian E.","family":"Aydemir","sequence":"additional","affiliation":[]},{"given":"Eli","family":"Barzilay","sequence":"additional","affiliation":[]},{"given":"Yegor","family":"Bryukhov","sequence":"additional","affiliation":[]},{"given":"Richard","family":"Eaton","sequence":"additional","affiliation":[]},{"given":"Adam","family":"Granicz","sequence":"additional","affiliation":[]},{"given":"Alexei","family":"Kopylov","sequence":"additional","affiliation":[]},{"given":"Christoph","family":"Kreitz","sequence":"additional","affiliation":[]},{"given":"Vladimir N.","family":"Krupski","sequence":"additional","affiliation":[]},{"given":"Lori","family":"Lorigo","sequence":"additional","affiliation":[]},{"given":"Stephan","family":"Schmitt","sequence":"additional","affiliation":[]},{"given":"Carl","family":"Witty","sequence":"additional","affiliation":[]},{"given":"Xin","family":"Yu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4419-8598-9","volume-title":"A Theory of Objects","author":"M. Abadi","year":"1996","unstructured":"Abadi, M., Cardelli, L.: A Theory of Objects. Springer, Heidelberg (1996)"},{"key":"19_CR2","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/S0049-237X(09)70683-4","volume-title":"Logic, Methodology and Philosophy of Science VII","author":"P. Aczel","year":"1986","unstructured":"Aczel, P.: The type theoretic interpretation of constructive set theory: Inductive definition. In: Logic, Methodology and Philosophy of Science VII, pp. 17\u201349. Elsevier Science Publishers, Amsterdam (1986)"},{"key":"19_CR3","unstructured":"Aczel, P., Rathjen, M.: Notes on constructive set theory. Technical Report 40, Mittag-Leffler (2000\/2001)"},{"key":"19_CR4","unstructured":"Allen, S., Bickford, M., Constable, R., et al.: FDL: A prototype formal digital library. PostScript document on website (May 2002), http:\/\/www.nuprl.org\/html\/FDLProject\/02cucs-fdl.html"},{"key":"19_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/10721959_12","volume-title":"Automated Deduction - CADE-17","author":"S. Allen","year":"2000","unstructured":"Allen, S., Constable, R., Eaton, R., Kreitz, C., Lorigo, L.: The NuPRL open logical environment. In: McAllester, D. (ed.) CADE 2000. LNCS, vol.\u00a01831, pp. 170\u2013176. Springer, Heidelberg (2000)"},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/3-540-46419-0_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Aspinall","year":"2000","unstructured":"Aspinall, D.: Proof General \u2013 A generic tool for proof development. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol.\u00a01785, p. 38. Springer, Heidelberg (2000), http:\/\/zermelo.dcs.ed.ac.uk\/home\/da\/papers\/pgoutline\/"},{"key":"19_CR7","unstructured":"Aydemir, B., Granicz, A., Hickey, J.: Formal design environments. In: Carre\u00f1o et al. [16], pp. 12\u201322"},{"key":"19_CR8","unstructured":"Barras, B., Boutin, S., Cornes, C., Courant, J., Filli\u00e2tre, J.-C., Gim\u00e9nez, E., Herbelin, H., G\u00e9rard-Mohring, Sa\u00efbi, A., Werner, B.: The Coq Proof Assistant Reference Manual. INRIA-Rocquencourt, CNRS and ENS Lyon (1996)"},{"key":"19_CR9","unstructured":"Barzilay, E., Allen, S.: Reflecting higher-order abstract syntax in NuPRL. In: Carre\u00f1o et al. [16], pp. 23\u201332"},{"key":"19_CR10","unstructured":"Bates, J.L.: A Logic for Correct Program Development. PhD thesis, Cornell University (1979)"},{"key":"19_CR11","unstructured":"Bates, J.L., Constable, R.L.: Definition of micro-PRL. Technical Report 82\u2013492, Cornell University, Computer Science Department, Ithaca, NY (1981)"},{"issue":"1","key":"19_CR12","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1145\/2363.2528","volume":"7","author":"J.L. Bates","year":"1985","unstructured":"Bates, J.L., Constable, R.L.: Proofs as programs. ACM Transactions on Programming Languages and Systems\u00a07(1), 53\u201371 (1985)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"19_CR13","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-322-90102-6","volume-title":"Automated Theorem Proving","author":"W. Bibel","year":"1987","unstructured":"Bibel, W.: Automated Theorem Proving, 2nd edn. Vieweg Verlag, Braunschweig (1987)","edition":"2"},{"key":"19_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/3-540-44755-5_9","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Bickford","year":"2001","unstructured":"Bickford, M., Kreitz, C., van Renesse, R., Liu, X.: Proving hybrid protocols correct. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol.\u00a02152, pp. 105\u2013120. Springer, Heidelberg (2001)"},{"key":"19_CR15","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2002)","year":"2002","unstructured":"Carre\u00f1o, V.A., Mu\u00f1oz, C.A., Tahar, S. (eds.): TPHOLs 2002. LNCS, vol.\u00a02410. Springer, Heidelberg (2002)"},{"key":"19_CR16","series-title":"Lecture Notes in Computer Science","volume-title":"Theorem Proving in Higher Order Logics; Track B Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2002)","year":"2002","unstructured":"Carre\u00f1o, V.A., Mu\u00f1oz, C.A., Tahar, S. (eds.): TPHOLs 2002. LNCS, vol.\u00a02410. Springer, Heidelberg (2002); National Aeronautics and Space Administration (2002)"},{"key":"19_CR17","doi-asserted-by":"crossref","unstructured":"Constable, R.L.: On the theory of programming logics. In: Proceedings of the 9th Annual ACM Symposium on the Theory of Computing, Boulder, CO, May 1977, pp. 269\u2013285 (1977)","DOI":"10.1145\/800105.803417"},{"key":"19_CR18","volume-title":"Implementing Mathematics with the NuPRL Development System","author":"R.L. Constable","year":"1986","unstructured":"Constable, R.L., Allen, S.F., Bromley, H.M., Cleaveland, W.R., Cremer, J.F., Harper, R.W., Howe, D.J., Knoblock, T.B., Mendler, N.P., Panangaden, P., Sasaki, J.T., Smith, S.F.: Implementing Mathematics with the NuPRL Development System. Prentice-Hall, NJ (1986)"},{"key":"19_CR19","series-title":"NATO ASI Series, Series F: Computer & System Sciences","first-page":"91","volume-title":"Foundations of Secure Computation","author":"R.L. Constable","year":"2000","unstructured":"Constable, R.L., Hickey, J.: NuPRL\u2019s class theory and its applications. In: Bauer, F.L., Steinbrueggen, R. (eds.) Foundations of Secure Computation. NATO ASI Series, Series F: Computer & System Sciences, pp. 91\u2013116. IOS Press, Amsterdam (2000)"},{"key":"19_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF","author":"M. Gordon","year":"1979","unstructured":"Gordon, M., Milner, R., Wadsworth, C.: Edinburgh LCF. LNCS, vol.\u00a078. Springer, Heidelberg (1979)"},{"key":"19_CR21","volume-title":"36th Hawaii International Conference on System Sciences","author":"A. Granicz","year":"2002","unstructured":"Granicz, A., Hickey, J.: Phobos: A front-end approach to extensible compilers. In: 36th Hawaii International Conference on System Sciences. IEEE, Los Alamitos (2002)"},{"key":"19_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"Formal Methods in Computer-Aided Design","author":"J. Harrison","year":"1996","unstructured":"Harrison, J.: HOL Light: A tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 265\u2013269. Springer, Heidelberg (1996)"},{"key":"19_CR23","unstructured":"Hayden, M.: The Ensemble System. PhD thesis, Department of Computer Science, Cornell University, Ithaca, NY (January 1998)"},{"key":"19_CR24","doi-asserted-by":"crossref","unstructured":"Hickey, J., Nogin, A., Granicz, A., Aydemir, B.: Formal compiler implementation in a logical framework. Submitted to ICFP 2003. Extended version of the paper is available as Caltech Technical Report caltechCSTR:2003.002 (2003)","DOI":"10.21236\/ADA437424"},{"key":"19_CR25","unstructured":"Hickey, J., Smith, J.D., Aydemir, B., Gray, N., Granicz, A., Tapus, C.: Process migration and transactions using a novel intermediate language. Technical Report caltechCSTR 2002.007, California Institute of Technology, Computer Science (July 2002)"},{"key":"19_CR26","unstructured":"Hickey, J.J.: Formal objects in type theory using very dependent types. In: Foundations of Object Oriented Languages 3 (1996), Available electronically through the http:\/\/www.cis.upenn.edu\/~bcpierce\/FOOL\/FOOL3.html"},{"key":"19_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1007\/3-540-63104-6_37","volume-title":"Automated Deduction - CADE-14","author":"J.J. Hickey","year":"1997","unstructured":"Hickey, J.J.: NuPRL-Light: An implementation framework for higer-order logics. In: McCune, W. (ed.) CADE 1997. LNCS, vol.\u00a01249, pp. 395\u2013399. Springer, Heidelberg (1997), An extended version of the paper can be found at http:\/\/www.cs.caltech.edu\/~jyh\/papers\/cade14_nl\/default.html"},{"key":"19_CR28","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/3-540-48660-7_19","volume-title":"Automated Deduction - CADE-16","author":"J.J. Hickey","year":"1999","unstructured":"Hickey, J.J.: Fault-tolerant distributed theorem proving. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 227\u2013231. Springer, Heidelberg (1999)"},{"key":"19_CR29","unstructured":"Hickey, J.J.: The MetaPRL Logical Programming Environment. PhD thesis, Cornell University, Ithaca, NY (January 2001)"},{"key":"19_CR30","unstructured":"Hickey, J.J., Aydemir, B., Bryukhov, Y., Kopylov, A., Nogin, A., Yu, X.: A listing of MetaPRL theories, http:\/\/metaprl.org\/theories.pdf"},{"key":"19_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/3-540-44659-1_16","volume-title":"Theorem Proving in Higher Order Logics","author":"J.J. Hickey","year":"2000","unstructured":"Hickey, J.J., Nogin, A.: Fast tactic-based theorem proving. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol.\u00a01869, pp. 252\u2013266. Springer, Heidelberg (2000)"},{"key":"19_CR32","unstructured":"Hickey, J.J., Nogin, A., Kopylov, A., et al.: MetaPRL home page, http:\/\/metaprl.org\/"},{"key":"19_CR33","unstructured":"Jackson, P.B.: Enhancing the NuPRL Proof Development System and Applying it to Computational Abstract Algebra. PhD thesis, Cornell University, Ithaca, NY (January 1995)"},{"key":"19_CR34","doi-asserted-by":"crossref","unstructured":"Kopylov, A.: Dependent intersection: A new way of defining records in type theory. In: Proceedings of 18th IEEE Symposium on Logic in Computer Science (2003) (to appear)","DOI":"10.1109\/LICS.2003.1210048"},{"key":"19_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1007\/3-540-44802-0_40","volume-title":"Computer Science Logic","author":"A. Kopylov","year":"2001","unstructured":"Kopylov, A., Nogin, A.: Markov\u2019s principle for propositional type theory. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142, pp. 570\u2013584. Springer, Heidelberg (2001)"},{"issue":"3","key":"19_CR36","first-page":"88","volume":"5","author":"C. Kreitz","year":"1999","unstructured":"Kreitz, C., Otten, J.: Connection-based theorem proving in classical and non-classical logics. Journal for Universal Computer Science, Special Issue on Integration of Deductive Systems\u00a05(3), 88\u2013112 (1999)","journal-title":"Journal for Universal Computer Science, Special Issue on Integration of Deductive Systems"},{"issue":"1-2","key":"19_CR37","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1006\/inco.2000.2913","volume":"162","author":"C. Kreitz","year":"2000","unstructured":"Kreitz, C., Schmitt, S.: A uniform procedure for converting matrix proofs into sequent-style systems. Journal of Information and Computation\u00a0162(1-2), 226\u2013254 (2000)","journal-title":"Journal of Information and Computation"},{"key":"19_CR38","doi-asserted-by":"crossref","unstructured":"Liu, X., Kreitz, C., van Renesse, R., Hickey, J.J., Hayden, M., Birman, K., Constable, R.: Building reliable, high-performance communication systems from components. In: 17th ACM Symposium on Operating Systems Principles (SOSP 1999), December 1999. Operating Systems Review, vol.\u00a034, pp. 80\u201392 (1999)","DOI":"10.1145\/319151.319157"},{"key":"19_CR39","unstructured":"Mannion, C.L., Allen, S.F.: A notation for computer aided mathematics. Department of Computer Science TR94-1465, Cornell University, Ithaca, NY (November 1994)"},{"key":"19_CR40","first-page":"8","volume":"67","author":"A.A. Markov","year":"1962","unstructured":"Markov, A.A.: On constructive mathematics. Trudy Matematicheskogo Instituta imeni V.A. Steklova\u00a067, 8\u201314 (1962); In Russian. English Translation: A.M.S. Translations, series 2, vol.98, pp. 1-9, MR 27#3528","journal-title":"Trudy Matematicheskogo Instituta imeni V.A. Steklova"},{"key":"19_CR41","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/S0049-237X(09)70189-2","volume-title":"Proceedings of the Sixth International Congress for Logic, Methodology, and Philosophy of Science","author":"P. Martin-L\u00f6f","year":"1982","unstructured":"Martin-L\u00f6f, P.: Constructive mathematics and computer programming. In: Proceedings of the Sixth International Congress for Logic, Methodology, and Philosophy of Science, pp. 153\u2013175. North Holland, Amsterdam (1982)"},{"key":"19_CR42","doi-asserted-by":"crossref","unstructured":"Nogin, A.: Quotient types: A modular approach. In: Carre\u00f1o et al. [15], pp. 263\u2013280, Available at http:\/\/nogin.org\/papers\/quotients.html","DOI":"10.1007\/3-540-45685-6_18"},{"key":"19_CR43","unstructured":"Nogin, A.: Theory and Implementation of an Efficient Tactic-Based Logical Framework. PhD thesis, Cornell University, Ithaca, NY (August 2002)"},{"key":"19_CR44","doi-asserted-by":"crossref","unstructured":"Nogin, A., Hickey, J.: Sequent schema for derived rules. In: Carre\u00f1o et al. [15], pp. 281\u2013297","DOI":"10.1007\/3-540-45685-6_19"},{"key":"19_CR45","unstructured":"Paulson, L., Nipkow, T.: Isabelle tutorial and user\u2019s manual. Technical report, University of Cambridge Computing Laboratory (1990)"},{"key":"19_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle","author":"L.C. Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle. LNCS, vol.\u00a0828. Springer, Heidelberg (1994)"},{"key":"19_CR47","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50019-9","volume-title":"Handbook of Automated Reasoning","author":"F. Pfenning","year":"2001","unstructured":"Pfenning, F.: Logical frameworks. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a02. Elsevier Science Publishers, Amsterdam (2001)"},{"key":"19_CR48","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/3-540-45744-5_34","volume-title":"Automated Reasoning","author":"S. Schmitt","year":"2001","unstructured":"Schmitt, S., Lorigo, L., Kreitz, C., Nogin, A.: JProver: Integrating connection-based theorem proving into interactive proof assistants. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 421\u2013426. Springer, Heidelberg (2001)"},{"key":"19_CR49","unstructured":"The Nuprl Staff. PRL: Proof refinement logic programmer\u2019s manual (Lambda PRL, VAX version). Cornell University, Department of Computer Science (1983)"},{"key":"19_CR50","unstructured":"Weis, P., Leroy, X.: Le langage Caml, 2nd edn., Dunod, Paris (1999) (in french)"},{"key":"19_CR51","unstructured":"Yu, X.: Formalizing abstract algebra in constructive set theory. Master\u2019s thesis, California Institute of Technology (2002)"},{"key":"19_CR52","unstructured":"Yu, X., Hickey, J.J.: Formalizing abstract algebra in constructive set theory. Submitted to LICS conference (2003)"},{"key":"19_CR53","unstructured":"Zippel, R.: MathBus, Available online at http:\/\/www.cs.cornell.edu\/Simlab\/papers\/mathbus\/mathTerm.htm"}],"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\/10930755_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,19]],"date-time":"2019-04-19T12:24:12Z","timestamp":1555676652000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10930755_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540406648","9783540451303"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/10930755_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003]]}}}