{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:45Z","timestamp":1749124065754},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540651376"},{"type":"electronic","value":"9783540495628"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0097798","type":"book-chapter","created":{"date-parts":[[2006,11,24]],"date-time":"2006-11-24T14:27:48Z","timestamp":1164378468000},"page":"294-316","source":"Crossref","is-referenced-by-count":2,"title":["Dependent types with explicit substitutions: A meta-theoretical development"],"prefix":"10.1007","author":[{"given":"C\u00e9sar","family":"Mu\u00f1oz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,10,26]]},"reference":[{"issue":"4","key":"16_CR1","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"1","author":"M. Abadi","year":"1991","unstructured":"M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. L\u00e9vy. Explicit substitution. Journal of Functional Programming, 1(4):375\u2013416, 1991.","journal-title":"Journal of Functional Programming"},{"key":"16_CR2","unstructured":"R. Bloo. Manuscript, 1997."},{"issue":"2","key":"16_CR3","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1006\/inco.1996.0041","volume":"126","author":"R. Bloo","year":"1996","unstructured":"R. Bloo, F. Kamareddine, and R. Nederpelt. The Barendregt cube with definitions and generalised reduction. Information and Computation, 126(2):123\u2013143, 1 May 1996.","journal-title":"Information and Computation"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"R. Di Cosmo and D. Kesner. Strong normalization of explicit substitutions via cut elimination in proof nets. In To appear in the Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science (LICS'97) Warsaw, Poland, July 1997.","DOI":"10.1109\/LICS.1997.614927"},{"issue":"2","key":"16_CR5","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1145\/226643.226675","volume":"43","author":"P.-L. Curien","year":"1996","unstructured":"P.-L. Curien, T. Hardin, and J.-J. L\u00e9vy. Confluence properties of weak and strong calculi of explicit substitutions. Journal of the ACM, 43(2):362\u2013397, March 1996.","journal-title":"Journal of the ACM"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"G. Dowek, T. Hardin, and C. Kirchner. Higher-order unification via explicit substitutions (extended abstract). In Proceedings, Tenth Annual IEEE Symposium on Logic in Computer Science, pages 366\u2013374, San Diego, California, 26\u201329 June 1995. IEEE Computer Society Press.","DOI":"10.1109\/LICS.1995.523271"},{"key":"16_CR7","unstructured":"G. Dowek, T. Hardin, C. Kirchner, and F. Pfenning. Unification via explicit substitutions: The case of higher-order patterns. In M. Maher, editor, Proceedings of the Joint International Conference and Symposium on Logic Programming, Bonn, Germany, September 1996. MIT Press. To appear."},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"H. Geuvers. The Church-Rosser property for \u03b2\u03b7-reduction in typed \u03bb-calculi. In Proceedings, Seventh Annual IEEE Symposium on Logic in Computer Science, pages 453\u2013460, Santa Cruz, California, 22\u201325 June 1992. IEEE Computer Society Press.","DOI":"10.1109\/LICS.1992.185556"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"H. Geuvers. A short and flexible proof of Strong Normalization for the Calculus of Constructions. In P. Dybjer and B. Nordstr\u00f6m, editors, Types for Proofs and Programs, International Workshop TYPES'94, volume 996 of LNCS, pages 14\u201338. B\u00e5stad, Sweden, 1994. Springer.","DOI":"10.1007\/3-540-60579-7_2"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"H. Geuvers and B. Werner. On the Church-Rosser property for expressive type systems and its consequences for their metatheoretic study. In Proceedings, Ninth Annual IEEE Symposium on Logic in Computer Science, pages 320\u2013329, Paris, France, 4\u20137 July 1994. IEEE Computer Society Press.","DOI":"10.1109\/LICS.1994.316057"},{"key":"16_CR11","unstructured":"J. Goubault-Larrecq. Une preuve de terminaison faible du \u03bb\u03c3-calcul. Technical Report RR-3090, Unit\u00e9 de recherche INRIA-Rocquencourt, Janvier 1997."},{"issue":"1","key":"16_CR12","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. Journal of the Association for Computing Machinery, 40(1):143\u2013184, 1993.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"G. Huet. Confluent reductions. Abstract properties and applications to term rewriting systems. J.A.C.M., 27(4), October 1980.","DOI":"10.1145\/322217.322230"},{"key":"16_CR14","unstructured":"F. Kamareddine and A. R\u00edos. The \u03bb\u222b-calculus: its typed and its extended versions. manuscript, June 1995."},{"issue":"1","key":"16_CR15","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1016\/0890-5401(90)90023-B","volume":"86","author":"D. Kapur","year":"1990","unstructured":"D. Kapur, P. Narendran, F. Otto. On ground-confluence of term rewriting systems. Information and Computation, 86(1):14\u201331, May 1990.","journal-title":"Information and Computation"},{"key":"16_CR16","unstructured":"D. Kapur and H. Zhang. RRL: A rewrite rule laboratory-user's manual. Technical Report 89-03, Department of Computer Science, The University of Iowa, 1989."},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"C. Kirchner and C. Ringeissen. Higher order equational unification via explicit substitutions. In Proceedings International Conference PLILP\/ALP\/HOA'97, Southampton (England), September 1997. Lecture Notes in Computer Science. Springer-Verlag.","DOI":"10.1007\/BFb0027003"},{"key":"16_CR18","unstructured":"J.-W. Klop. Combinatory reduction systems. Mathematical Center Tracts, (27), 1980."},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"P. Lescanne. From \u03bb\u03c3 to \u03bbv a journey through calculi of explicit substitutions. In Proceedings of the 21st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 60\u201369, January 1994.","DOI":"10.1145\/174675.174707"},{"key":"16_CR20","unstructured":"L. Magnusson. The Implementation of ALF\u2014A Proof Editor Based on Martin-L\u00f6f's Monomorphic Type Theory with Explicit Substitution. PhD thesis, Chalmers University of Technology and G\u00f6teborg University, January 1995."},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"P.-A. Melli\u00e8s. Typed \u03bb-calculi with explicit substitutions may not terminate. In Typed Lambda Calculi and Applications, number 902 in LNCS. Second International Conference TLCA'95, Springer-Verlag, 1995.","DOI":"10.1007\/BFb0014062"},{"key":"16_CR22","unstructured":"C. Mu\u00f1oz. Proof representation in type theory: State of the art. In Proceedings, XXII Latinamerican Conference of Informatics CLEI Panel 96, Santaf\u00e9 de Bogot\u00e1, Colombia, June 1996."},{"key":"16_CR23","unstructured":"C. Mu\u00f1oz. A left-linear variant of \u03bb\u03c3. In Proceedings International Conference PLILP\/ALP\/HOA'97, Southampton (England), September 1997. Lecture Notes in Computer Science. Springer-Verlag."},{"key":"16_CR24","unstructured":"G. Nadathur. The (SCons) rule. Personal communication, 1996."},{"key":"16_CR25","unstructured":"B. Pagano. Confluent extensions of \u03bb\u21d1. Personal communication, 1996."},{"key":"16_CR26","unstructured":"A. R\u00edos. Contributions \u00e0 l'\u00e9tude de \u03bb-calculs avec des substitutions explicites. PhD thesis, U. Paris VII, 1993."},{"issue":"1","key":"16_CR27","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0304-3975(94)00125-3","volume":"136","author":"E. Ritter","year":"1994","unstructured":"E. Ritter. Categorical abstract machines for higher-order lambda calculi. Theoretical Computer Science, 136(1):125\u2013162, 1994.","journal-title":"Theoretical Computer Science"},{"key":"16_CR28","volume-title":"Computational aspects of an order-sorted logic with term declarations, volume 395 of Lecture Notes in Computer Science and Lecture Notes in Artificial Intelligence","author":"M. Schmidt-Schauss","year":"1989","unstructured":"M. Schmidt-Schauss, Computational aspects of an order-sorted logic with term declarations, volume 395 of Lecture Notes in Computer Science and Lecture Notes in Artificial Intelligence. Springer-Verlag Inc., New York, NY, USA, 1989."},{"key":"16_CR29","unstructured":"P. Severi. Normalisation in LAMBDA CALCULUS and its relation to type inference. PhD thesis, Eindhoven University of Technology, 1996."},{"key":"16_CR30","volume-title":"Formulation of Martin-L\u00f6f's theory of types with explicit substitution. Technical report","author":"A. Tasistro","year":"1993","unstructured":"A. Tasistro. Formulation of Martin-L\u00f6f's theory of types with explicit substitution. Technical report, Chalmers University of Technology, University of G\u00f6teborg, G\u00f6teborg, Sweden, May 1993."},{"key":"16_CR31","unstructured":"B. Werner. Une Th\u00e9orie des Constructions Inductives. PhD thesis, U. Paris VII, 1994."},{"issue":"1","key":"16_CR32","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1137\/0219005","volume":"19","author":"H. Yokouchi","year":"1990","unstructured":"H. Yokouchi and T. Hikita. A rewriting system for categorical combinators with multiple arguments. SIAM Journal of Computing, 19(1):78\u201397, February 1990.","journal-title":"SIAM Journal of Computing"},{"key":"16_CR33","doi-asserted-by":"crossref","first-page":"89","DOI":"10.3233\/FI-1995-24124","volume":"24","author":"H. Zantema","year":"1995","unstructured":"H. Zantema. Termination of term rewriting by semantic labelling. Fundamenta Informaticae, 24:89\u2013105, 1995.","journal-title":"Fundamenta Informaticae"},{"key":"16_CR34","unstructured":"H. Zantema. Termination of \u03d5 and \u03a0 \u03c6 by semantic labelling. Personal communication, 1996."}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0097798","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,19]],"date-time":"2020-04-19T03:20:37Z","timestamp":1587266437000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0097798"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540651376","9783540495628"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/bfb0097798","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}