{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:11Z","timestamp":1761611171359},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540603597"},{"type":"electronic","value":"9783540450481"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bfb0026813","type":"book-chapter","created":{"date-parts":[[2005,11,19]],"date-time":"2005-11-19T10:29:45Z","timestamp":1132396185000},"page":"45-62","source":"Crossref","is-referenced-by-count":26,"title":["A \u03bb-calculus \u00e0 la de Bruijn with explicit substitutions"],"prefix":"10.1007","author":[{"given":"Fairouz","family":"Kamareddine","sequence":"first","affiliation":[]},{"given":"Alejandro","family":"R\u00edos","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,16]]},"reference":[{"issue":"4","key":"5_CR1","doi-asserted-by":"crossref","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 Substitutions. Journal of Functional Programming, 1(4):375\u2013416, 1991.","journal-title":"Journal of Functional Programming"},{"key":"5_CR2","unstructured":"H. Barendregt. The Lambda Calculus: Its Syntax and Semantics (revised edition). North Holland, 1984."},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Z. Benaissa, D. Briaud, P. Lescanne, and J. Rouyer-Degli. \u03bbv, a calculus of explicit substitutions which preserves strong normalisation. Personal communication, 1995.","DOI":"10.1017\/S0956796800001945"},{"key":"5_CR4","volume-title":"Technical Report RR 1617","author":"P.-L. Curien","year":"1992","unstructured":"P.-L. Curien, T. Hardin, and J.-J. L\u00e9vy. Confluence properties of weak and strong calculi of explicit substitutions. Technical Report RR 1617, INRIA, Rocquencourt, 1992. To appear in the JACM."},{"key":"5_CR5","first-page":"209","volume-title":"Lecture Notes in Computer Science 629","author":"P.-L. Curien","year":"1992","unstructured":"P.-L. Curien, T. Hardin, and A. R\u00edos. Strong Normalization of Substitutions in Proceedings of MFCS'92. In I.M. Havel and V. Koubek, editors, Lecture Notes in Computer Science 629, pages 209\u2013217, Prague, 1992. Springer-Verlag."},{"issue":"I","key":"5_CR6","first-page":"471","volume":"312","author":"P.-L. Curien","year":"1991","unstructured":"P.-L. Curien and A. R\u00edos. Un r\u00e9sultat de Compl\u00e9tude pour les substitutions explicites. Comptes Rendus de l'Acad\u00e9mie des Sciences, 312, I:471\u2013476, 1991.","journal-title":"Comptes Rendus de l'Acad\u00e9mie des Sciences"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"P.-L. Curien. Categorical Combinators, Sequential Algorithms and Functional Programming. Pitman, 1986. Revised edition: Birkh\u00e4user (1993).","DOI":"10.1007\/978-1-4612-0317-9"},{"issue":"5","key":"5_CR8","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N. Bruijn de","year":"1972","unstructured":"N. de Bruijn. Lambda-Calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser Theorem. Indag. Mat., 34(5):381\u2013392, 1972.","journal-title":"Indag. Mat."},{"key":"5_CR9","doi-asserted-by":"crossref","first-page":"348","DOI":"10.1016\/1385-7258(78)90052-5","volume":"40","author":"N. Bruijn de","year":"1978","unstructured":"N. de Bruijn. Lambda-Calculus notation with namefree formulas involving symbols that represent reference transforming mappings. Indag. Mat., 40:348\u2013356, 1978.","journal-title":"Indag. Mat."},{"key":"5_CR10","unstructured":"N. G. de Bruijn. A namefree lambda calculus with facilities for internal definition of expressions and segments. Technical Report TH-Report 78-WSK-03, Department of Mathematics, Eindhoven University of Technology, 1978."},{"issue":"2","key":"5_CR11","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/0304-3975(89)90105-9","volume":"65","author":"T. Hardin","year":"1989","unstructured":"T. Hardin. Confluence Results for the Pure Strong Categorical Logic CCL: \u03bb-calculi as Subsystems of CCL. Theoretical Computer Science, 65(2):291\u2013342, 1989.","journal-title":"Theoretical Computer Science"},{"key":"5_CR12","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1016\/0304-3975(86)90035-6","volume":"46","author":"T. Hardin","year":"1986","unstructured":"T. Hardin and A. Laville. Proof of Termination of the Rewriting System SUBST on CCL. Theoretical Computer Science, 46:305\u2013312, 1986.","journal-title":"Theoretical Computer Science"},{"key":"5_CR13","unstructured":"T. Hardin and J.-J. L\u00e9vy. A Confluent Calculus of Substitutions. France-Japan Artificial Intelligence and Computer Science Symposium, December 1989."},{"key":"5_CR14","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"G. Huet","year":"1980","unstructured":"G. Huet. Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems. Journal of the Association for Computing Machinery, 27:797\u2013821, October 1980.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"D. Knuth and P. Bendix. Simple Word Problems in Universal Algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263\u2013297. Pergamon Press, 1970.","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"issue":"3","key":"5_CR16","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1142\/S0129054193000146","volume":"4","author":"F. Kamareddine","year":"1993","unstructured":"F. Kamareddine and R. P. Nederpelt. On stepwise explicit substitution. International Journal of Foundations of Computer Science, 4(3):197\u2013240, 1993.","journal-title":"International Journal of Foundations of Computer Science"},{"key":"5_CR17","volume-title":"PhD thesis","author":"M. Mauny","year":"1985","unstructured":"M. Mauny. Compilation des langages fonctionnels dans les combinateurs cat\u00e9goriques. Application au langage ML. PhD thesis, Universit\u00e9 Paris VII, Paris, France, 1985."},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"P.-A. Melli\u00e8s. Typed \u03bb-calculi with explicit substitutions may not terminate in Proceedings of TLCA'95. Lecture Notes in Computer Science, 902, 1995.","DOI":"10.1007\/BFb0014062"},{"key":"5_CR19","unstructured":"A. R\u00edos. Contribution \u00e0 l'\u00e9tude des \u03bb-calculs avec substitutions explicites. PhD thesis, Universit\u00e9 de Paris 7, 1993."},{"issue":"1","key":"5_CR20","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1006\/jsco.1994.1003","volume":"17","author":"H. Zantema","year":"1994","unstructured":"H. Zantema. Termination of term rewriting: interpretation and type elimination. J. Symbolic Computation, 17(1):23\u201350, 1994.","journal-title":"J. Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","Programming Languages: Implementations, Logics and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0026813","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T01:54:11Z","timestamp":1586570051000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0026813"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540603597","9783540450481"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/bfb0026813","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}