{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T04:00:47Z","timestamp":1648785647267},"reference-count":18,"publisher":"Elsevier BV","issue":"7","license":[{"start":{"date-parts":[[2003,9,1]],"date-time":"2003-09-01T00:00:00Z","timestamp":1062374400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3619,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2003,9]]},"DOI":"10.1016\/s1571-0661(04)80759-x","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T16:47:47Z","timestamp":1096476467000},"page":"86-105","source":"Crossref","is-referenced-by-count":1,"title":["Explicit Substitutions \u00e0 la de Bruijn"],"prefix":"10.1016","volume":"85","author":[{"given":"Fairouz","family":"Kamareddine","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alejandro","family":"R\u00edos","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"issue":"4","key":"10.1016\/S1571-0661(04)80759-X_NEWBIB1","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1017\/S0956796800000186","article-title":"Explicit Substitutions","volume":"1","author":"Abadi","year":"1991","journal-title":"Journal of Functional Programming"},{"issue":"5","key":"10.1016\/S1571-0661(04)80759-X_NEWBIB2","article-title":"\u03bb\u03c5, a calculus of explicit substitutions which preserves strong normalisation","volume":"6","author":"Benaissa","year":"1996","journal-title":"Functional Programming"},{"key":"10.1016\/S1571-0661(04)80759-X_NEWBIB3","series-title":"Categorical Combinators, Sequential Algorithms and Functional Programming","author":"Curien","year":"1986"},{"key":"10.1016\/S1571-0661(04)80759-X_NEWBIB4","doi-asserted-by":"crossref","first-page":"799","DOI":"10.1093\/logcom\/6.6.799","article-title":"Strong normalisation of substitutions","volume":"6","author":"P-L","year":"1996","journal-title":"Logic and Computation"},{"issue":"5","key":"10.1016\/S1571-0661(04)80759-X_NEWBIB5","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","article-title":"Lambda-Calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser Theorem","volume":"34","author":"de Bruijn","year":"1972","journal-title":"Indag. Mat"},{"key":"10.1016\/S1571-0661(04)80759-X_NEWBIB6","unstructured":"B. Guillaume. Un calcul des substitutions avec etiquettes. PhD thesis, Universit\u00e9 de Savoie, Chamb\u00e9ry, France, 1999."},{"key":"10.1016\/S1571-0661(04)80759-X_NEWBIB7","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1016\/0304-3975(86)90035-6","article-title":"Proof of Termination of the Rewriting System SUBST on CCL","volume":"46","author":"Hardin","year":"1986","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80759-X_NEWBIB8","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/0304-3975(95)00101-8","article-title":"A useful \u03bb-notation","volume":"155","author":"Kamareddine","year":"1996","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"10.1016\/S1571-0661(04)80759-X_NEWBIB9","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1142\/S0129054193000146","article-title":"On stepwise explicit substitution","volume":"4","author":"Kamareddine","year":"1993","journal-title":"International Journal of Foundations of Computer Science"},{"key":"10.1016\/S1571-0661(04)80759-X_NEWBIB10","doi-asserted-by":"crossref","unstructured":"F. Kamareddine, and A. R\u00edos. A \u03bb-calculus \u00e0 la de Bruijn with explicit substitutions. Proceedings of PLILP'95. LNCS, 982:45\u201362, 1995.","DOI":"10.1007\/BFb0026813"},{"issue":"4","key":"10.1016\/S1571-0661(04)80759-X_NEWBIB11","doi-asserted-by":"crossref","first-page":"420","DOI":"10.1017\/S0956796897002785","article-title":"Extending a \u03bb-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms","volume":"7","author":"Kamareddine","year":"1997","journal-title":"Journal of Functional Programming"},{"issue":"6","key":"10.1016\/S1571-0661(04)80759-X_NEWBIB12","doi-asserted-by":"crossref","first-page":"843","DOI":"10.1093\/jigpal\/6.6.843","article-title":"Bridging de Bruijn indices and variable names in explicit substitutions calculi","volume":"6","author":"Kamareddine","year":"1998","journal-title":"Logic Journal of the IGPL"},{"issue":"3","key":"10.1016\/S1571-0661(04)80759-X_NEWBIB13","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1093\/logcom\/10.3.349","article-title":"Relating the \u03bb\u03c3- and \u03bbs-styles of explicit substitutions","volume":"10","author":"Kamareddine","year":"2000","journal-title":"Logic and Computation"},{"key":"10.1016\/S1571-0661(04)80759-X_NEWBIB14","series-title":"Handbook of Logic in Computer Science, II","article-title":"Term rewriting systems","author":"Klop","year":"1992"},{"key":"10.1016\/S1571-0661(04)80759-X_NEWBIB15","series-title":"The Implementation of Functional Programming Languages","author":"Peyton-Jones","year":"1987"},{"key":"10.1016\/S1571-0661(04)80759-X_NEWBIB16","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":"10.1016\/S1571-0661(04)80759-X_NEWBIB17","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1006\/jsco.1994.1003","article-title":"Termination of term rewriting: interpretation and type elimination","volume":"17","author":"Zantema","year":"1994","journal-title":"J. Symbolic Computation"},{"key":"10.1016\/S1571-0661(04)80759-X_NEWBIB18","doi-asserted-by":"crossref","first-page":"89","DOI":"10.3233\/FI-1995-24124","article-title":"Termination of term rewriting by semantic labelling","volume":"24","author":"Zantema","year":"1995","journal-title":"Fundamenta Informaticae"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S157106610480759X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S157106610480759X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T07:14:14Z","timestamp":1585898054000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S157106610480759X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,9]]},"references-count":18,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2003,9]]}},"alternative-id":["S157106610480759X"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80759-x","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2003,9]]}}}