{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T20:19:09Z","timestamp":1790885949616,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":52,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540213666","type":"print"},{"value":"9783540399933","type":"electronic"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-39993-3_16","type":"book-chapter","created":{"date-parts":[[2010,6,22]],"date-time":"2010-06-22T18:30:36Z","timestamp":1277231436000},"page":"334-375","source":"Crossref","is-referenced-by-count":11,"title":["Pure Type Systems in Rewriting Logic: Specifying Typed Higher-Order Languages in a First-Order Logical Framework"],"prefix":"10.1007","author":[{"given":"Mark-Oliver","family":"Stehr","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"16_CR1","series-title":"Handbook of Logic in Computer Science","volume-title":"Background: Computational Structures","author":"H.P. Barendregt","year":"1992","unstructured":"Barendregt, H.P.: Lambda-calculi with types. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Background: Computational Structures. Handbook of Logic in Computer Science, vol.\u00a02. Claredon Press, Oxford (1992)"},{"key":"16_CR2","unstructured":"Barras, B., Boutin, S., Cornes, C., Courant, J., Coscoy, Y., Delahaye, D., de Rauglaudre, D., Filliatre, J.C., Gim\u00e9nez, E., Herbelin, H., Huet, G., Laulh\u00e8re, H., Mu\u00f1oz, C., Murthy, C., Parent-Vigouroux, C., Loiseleur, P., Paulin, C., Sa\u00efbi, A., Werner, B.: The Coq Proof Assistent Reference Manual, Version 6.3.1, Coq Project. Technical report, INRIA (1999), http:\/\/logical.inria.fr\/"},{"key":"16_CR3","unstructured":"Basin, D., Clavel, M., Meseguer, J.: Reflective metalogical frameworks. In: LFM 1999: Workshop on Logical Frameworks and Meta-languages, Proceedings, Paris, France, September 28 (1999), http:\/\/plan9.bell-labs.com\/who\/felty\/LFM99\/"},{"key":"16_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/3-540-44450-5_4","volume-title":"FST TCS 2000: Foundations of Software Technology and Theoretical Science","author":"D. Basin","year":"2000","unstructured":"Basin, D., Clavel, M., Meseguer, J.: Rewriting logic as a metalogical framework. In: Kapoor, S., Prasad, S. (eds.) FST TCS 2000. LNCS, vol.\u00a01974, pp. 55\u201380. Springer, Heidelberg (2000)"},{"issue":"5","key":"16_CR5","doi-asserted-by":"publisher","first-page":"699","DOI":"10.1017\/S0956796800001945","volume":"6","author":"Z. Benaissa","year":"1996","unstructured":"Benaissa, Z., Briaud, D., Lescanne, P., Rouyer-Degli, J.: \u03bb\u03c5, a calculus of explicit substitutions which preserves strong normalisation. Journal of Functional Programming\u00a06(5), 699\u2013722 (1996)","journal-title":"Journal of Functional Programming"},{"key":"16_CR6","unstructured":"Berardi, S.: Towards a mathematical analysis of the Coquand-Huet calculus of constructions and other systems in Barendregt\u2019s cube. Technical report, Carnegie Mellon University and Universita di Torino (1988)"},{"key":"16_CR7","unstructured":"Berkling, K.J.: A symmetric complement to the lambda-calulus. Interner Bericht ISF-76-7, GMD, St. Augustin, Germany (1976)"},{"key":"16_CR8","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/S0019-9958(82)90458-2","volume":"55","author":"K.J. Berkling","year":"1982","unstructured":"Berkling, K.J., Fehr, E.: A consistent extension of the lambda-calculus as a base for functional programming languages. Information and Control\u00a055, 89\u2013101 (1982)","journal-title":"Information and Control"},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/3-540-48685-2_25","volume-title":"Rewriting Techniques and Applications","author":"F. Blanqui","year":"1999","unstructured":"Blanqui, F., Jouannaud, J.-P., Okada, M.: The calculus of algebraic constructions. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol.\u00a01631, p. 301. Springer, Heidelberg (1999)"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030589","volume-title":"TAPSOFT\u201997: Theory and Practice of Software Development","author":"A. Bouhoula","year":"1997","unstructured":"Bouhoula, A., Jouannaud, J.-P., Meseguer, J.: Specification and proof in membership equational logic. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol.\u00a01214, Springer, Heidelberg (1997)"},{"key":"16_CR11","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/S0304-3975(99)00206-6","volume":"236","author":"A. Bouhoula","year":"2000","unstructured":"Bouhoula, A., Jouannaud, J.-P., Meseguer, J.: Specification and proof in membership equational logic. Theoretical Computer Science\u00a0236, 35\u2013132 (2000)","journal-title":"Theoretical Computer Science"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Church, A.: A formulation of the simple theory of types. Journal of Symbolic Logic\u00a05(1) (1940)","DOI":"10.2307\/2266170"},{"key":"16_CR13","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Quesada, J.: Maude: Specification and Programming in Rewriting Logic. SRI International (January 1999), http:\/\/maude.csl.sri.com"},{"key":"16_CR14","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Quesada, J.: A tutorial on maude (March 2000), http:\/\/maude.csl.sri.com"},{"key":"16_CR15","volume-title":"Logical Frameworks","author":"T. Coquand","year":"1991","unstructured":"Coquand, T.: An algorithm for testing conversion in type theory. In: Huet, G., Plotkin, G.D. (eds.) Logical Frameworks. Cambridge University Press, Cambridge (1991)"},{"issue":"2\/3","key":"16_CR16","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"Coquand, T., Huet, G.: The calculus of constructions. Information and Computation\u00a076(2\/3), 95\u2013120 (1988)","journal-title":"Information and Computation"},{"key":"16_CR17","series-title":"Lecture Notes in Computer Science","volume-title":"COLOG-88","author":"T. Coquand","year":"1990","unstructured":"Coquand, T., Paulin-Mohring, C.: Inductively defined types. In: Martin-L\u00f6f, P., Mints, G. (eds.) COLOG 1988. LNCS, vol.\u00a0417. Springer, Heidelberg (1990)"},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"de Bruijn, N.G.: Lambda calculus with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. In: Proceedings Kninkl. Nederl. Akademie van Wetenschappen, vol.\u00a075(5), pp. 381\u2013392 (1972)","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"16_CR19","first-page":"191","volume-title":"Proceedings of Logic Colloquium 1988","author":"S. Feferman","year":"1988","unstructured":"Feferman, S.: Finitary inductive systems. In: Ferro, R. (ed.) Proceedings of Logic Colloquium 1988, Padova, Italy, pp. 191\u2013220. North-Holland, Amsterdam (1988)"},{"key":"16_CR20","unstructured":"Gardner, P.: Representing Logics in Type Theory. PhD thesis, University of Edinburgh (1992)"},{"key":"16_CR21","unstructured":"Geuvers, H.: Logics and Type Systems. PhD thesis, University of Nijmegen (1993)"},{"issue":"2","key":"16_CR22","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1017\/S0956796800020037","volume":"1","author":"H. Geuvers","year":"1991","unstructured":"Geuvers, H., Nederhof, M.-J.: A modular proof of strong normalization for the calculus of constructions. Journal of Functional Programming\u00a01(2), 155\u2013189 (1991)","journal-title":"Journal of Functional Programming"},{"key":"16_CR23","unstructured":"Girard, J.Y.: Interpretation fonctionelle et elimination des coupures dans l\u2019arithmetique d\u2019ordre superieur. PhD thesis, Universit\u00e9 Paris VII (1972)"},{"key":"16_CR24","first-page":"193","volume-title":"Second Annual Symposium on Logic in Computer Science, Proceedings","author":"R. Harper","year":"1987","unstructured":"Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. In: Second Annual Symposium on Logic in Computer Science, Proceedings, Ithaca, New York, pp. 193\u2013204. IEEE, Los Alamitos (1987)"},{"key":"16_CR25","volume-title":"A Perspective in Theoretical Computer Science","author":"G. Huet","year":"1989","unstructured":"Huet, G.: The constructive engine. In: Narasimhan, R. (ed.) A Perspective in Theoretical Computer Science. World Scientific, Singapore (1989)"},{"key":"16_CR26","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"International Workshop on Rewriting Logic and its Applications Abbaye des Pr\u00e9montr\u00e9s at Pont-\u00e0-Mousson, Proceedings","author":"J.-P. Jouannaud","year":"1998","unstructured":"Jouannaud, J.-P.: Membership equational logic, calculus of inductive constructions, and rewrite logic. In: International Workshop on Rewriting Logic and its Applications Abbaye des Pr\u00e9montr\u00e9s at Pont-\u00e0-Mousson, Proceedings, France, September 1998. Electronic Notes in Theoretical Computer Science, vol.\u00a015. Elsevier, Amsterdam (1998), http:\/\/www.elsevier.nl\/locate\/entcs\/volume15.html"},{"key":"16_CR27","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1145\/174675.174707","volume-title":"Conference Record of POPL 1994: 21st ACM SIGPLANSIGACT Symposium on Principles of Programming Languages","author":"P. Lescanne","year":"1994","unstructured":"Lescanne, P.: From \u03bb\u03c3 to \u03bb\u03c5, a journey through calculi of explicit substitutions. In: Boehm, H. (ed.) Conference Record of POPL 1994: 21st ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, Portland, Oregon, pp. 60\u201369. ACM, New York (1994)"},{"key":"16_CR28","unstructured":"Lescanne, P., Rouyer-Degli, J.: The calculus of explicit substitutions \u03bb\u03c5. Technical Report RR-2222, INRIA-Lorraine (January 1994)"},{"key":"16_CR29","series-title":"International Series of Monographs on Computer Science","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198538356.001.0001","volume-title":"Computation and Reasoning: A Type Theory for Computer Science","author":"Z. Luo","year":"1994","unstructured":"Luo, Z.: Computation and Reasoning: A Type Theory for Computer Science. International Series of Monographs on Computer Science. Oxford University Press, Oxford (1994)"},{"key":"16_CR30","unstructured":"Magnussen, L.: The Implementation of ALF \u2013 A Proof Editor based on Martin-L\u00f6f\u2019s Monomorphic Type Theory with Explicit Substitutions. PhD thesis, University of G\u00f6teborg, Department of Computer Science (1994)"},{"key":"16_CR31","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1093\/oso\/9780198538592.003.0014","volume-title":"What is a Logical System?","author":"N. Mart\u00ed-Oliet","year":"1994","unstructured":"Mart\u00ed-Oliet, N., Meseguer, J.: General logics and logical frameworks. In: Gabbay, D. (ed.) What is a Logical System?, pp. 355\u2013392. Oxford University Press, Oxford (1994)"},{"key":"16_CR32","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"RWLW 1996, First International Workshop on Rewriting Logic and its Applications Asilomar Conference Center, Proceedings","author":"N. Mart\u00ed-Oliet","year":"1996","unstructured":"Mart\u00ed-Oliet, N., Meseguer, J.: Rewriting logic as a logical and semantic framework. In: RWLW 1996, First International Workshop on Rewriting Logic and its Applications Asilomar Conference Center, Proceedings, Pacific Grove, CA, USA. Electronic Notes in Theoretical Computer Science, vol.\u00a04. Elsevier, Amsterdam (1996), http:\/\/www.elsevier.nl\/locate\/entcs\/volume4.html"},{"key":"16_CR33","unstructured":"Martin-L\u00f6f, P.: An intuitionistic theory of types. Technical report, University of Stockholm (1972)"},{"key":"16_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037113","volume-title":"Typed Lambda Calculi and Applications","author":"J. McKinna","year":"1993","unstructured":"McKinna, J., Pollack, R.: Pure type systems formalized. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664. Springer, Heidelberg (1993)"},{"key":"16_CR35","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/S0049-237X(08)70132-0","volume-title":"Logic Colloquium 1987, Proceedings","author":"J. Meseguer","year":"1989","unstructured":"Meseguer, J.: General logics. In: Ebbinghaus, H.-D., et al. (eds.) Logic Colloquium 1987, Proceedings, Granada, Spain, pp. 275\u2013329. North-Holland, Amsterdam (1989)"},{"key":"16_CR36","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J. Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science\u00a096, 73\u2013155 (1992)","journal-title":"Theoretical Computer Science"},{"key":"16_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1007\/3-540-64299-4_26","volume-title":"Recent Trends in Algebraic Development Techniques","author":"J. Meseguer","year":"1998","unstructured":"Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol.\u00a01376, pp. 18\u201361. Springer, Heidelberg (1998)"},{"key":"16_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-08531-9","volume-title":"Fundamentals of Computation Theory, International Conference, Proceedings","author":"M.J. O\u2019Donnell","year":"1977","unstructured":"O\u2019Donnell, M.J.: Computing in systems descibed by equations. In: Fundamentals of Computation Theory, International Conference, Proceedings, Pozna\u00f1-Kornik, Poland. LNCS, vol.\u00a058. Springer, Heidelberg (1977)"},{"key":"16_CR39","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":"16_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1007\/3-540-58085-9_82","volume-title":"Types for Proofs and Programs","author":"R. Pollack","year":"1994","unstructured":"Pollack, R.: Closure under alpha-conversion. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol.\u00a0806, pp. 313\u2013332. Springer, Heidelberg (1994)"},{"key":"16_CR41","unstructured":"Pollack, R.: The Theory of LEGO: A Proof Checker for the Extended Calculus of Constructions. PhD thesis, University of Edinburgh (1994)"},{"key":"16_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014065","volume-title":"Typed Lambda Calculi and Applications","author":"R. Pollack","year":"1995","unstructured":"Pollack, R.: A verified typechecker. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol.\u00a0902. Springer, Heidelberg (1995)"},{"key":"16_CR43","series-title":"Lecture Notes in Computer Science","volume-title":"Programming Symposium","author":"J. Reynolds","year":"1974","unstructured":"Reynolds, J.: Towards a theory of type structure. In: Robinet, B. (ed.) Programming Symposium. LNCS, vol.\u00a019. Springer, Heidelberg (1974)"},{"key":"16_CR44","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/BFb0054266","volume-title":"Automated Deduction - CADE-15","author":"C. Sch\u00fcrmann","year":"1998","unstructured":"Sch\u00fcrmann, C., Pfenning, F.: Automated theorem proving in a simple meta-logic for LF. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol.\u00a01421, pp. 286\u2013300. Springer, Heidelberg (1998)"},{"key":"16_CR45","unstructured":"Severi, P.G.: Normalization in Lambda Calculus and its relation to Type Inference. PhD thesis, Eindhoven University of Technology (1996)"},{"key":"16_CR46","unstructured":"Stehr, M.-O.: CINNI - A New Calculus of Explicit Substitutions and its Application to Pure Type Systems. Manuscript, CSL, SRI-International, Menlo Park, CA, USA (1999)"},{"key":"16_CR47","doi-asserted-by":"crossref","unstructured":"Stehr, M.-O.: CINNI \u2013 A Generic Calculus of Explicit Substitutions and its Application to \u03bb-, \u03c3- and \u03c0-calculi. In: Futatsugi, K. (ed.) The 3rd International Workshop on Rewriting Logic and its Applications Kanazawa City Cultural Hall. Proceedings, Kanzawa Japan. Electronic Notes in Theoretical Computer Science, vol.\u00a036, pp. 71\u201392. Elsevier, Amsterdam (2000), http:\/\/www.elsevier.nl\/locate\/entcs\/volume36.html Extended version at http:\/\/www.csl.sri.com\/~stehr","DOI":"10.1016\/S1571-0661(05)80125-2"},{"key":"16_CR48","unstructured":"Stehr, M.-O.: Programming, Specification, and Interactive Theorem Proving \u2014 Towards a Unified Language based on Equational Logic, Rewriting Logic, and Type Theory. Doctoral Thesis, Universit\u00e4t Hamburg, Fachbereich Informatik, Germany (2002), http:\/\/www.sub.uni-hamburg.de\/disse\/810\/"},{"key":"16_CR49","unstructured":"Stehr, M.-O., Meseguer, J.: Pure type systems in rewriting logic. In: LFM 1999: Workshop on Logical Frameworks and Meta-languages. Proceedings, Paris, France, September 28 (1999), http:\/\/plan9.bell-labs.com\/who\/felty\/LFM99\/"},{"key":"16_CR50","unstructured":"Terlouw, J.: Een nadere bewijstheoretische analyse van GSTTs. Manuscript, University of Nijmegen, The Netherlands (1989)"},{"key":"16_CR51","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1006\/inco.1993.1038","volume":"105","author":"L.S. Benthem Jutting van","year":"1993","unstructured":"van Benthem Jutting, L.S.: Typing in pure type systems. Information and Computation\u00a0105, 30\u201341 (1993)","journal-title":"Information and Computation"},{"key":"16_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1007\/3-540-58085-9_71","volume-title":"Types for Proofs and Programs","author":"L.S. Benthem Jutting van","year":"1994","unstructured":"van Benthem Jutting, L.S., McKinna, J., Pollack, R.: Checking algorithms for pure type systems. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol.\u00a0806, pp. 19\u201361. Springer, Heidelberg (1994)"}],"container-title":["Lecture Notes in Computer Science","From Object-Orientation to Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-39993-3_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,27]],"date-time":"2024-03-27T19:17:37Z","timestamp":1711567057000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39993-3_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540213666","9783540399933"],"references-count":52,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39993-3_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}