{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T04:20:24Z","timestamp":1742617224413,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540617358"},{"type":"electronic","value":"9783540706724"}],"license":[{"start":{"date-parts":[[1996,1,1]],"date-time":"1996-01-01T00:00:00Z","timestamp":820454400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61735-3_19","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:17:48Z","timestamp":1330294668000},"page":"284-298","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["\u03bb-calculi with explicit substitutions and composition which preserve \u03b2-strong normalization"],"prefix":"10.1007","author":[{"given":"Maria C. F.","family":"Ferreira","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Delia","family":"Kesner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laurence","family":"Puel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"issue":"1","key":"19_CR1","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"4","author":"M. Abadi","year":"1991","unstructured":"M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. L\u00e9vy. Explicit substitutions. Journal of Functional Programming, 4(1):375\u2013416, 1991.","journal-title":"Journal of Functional Programming"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"Z.-El-A. Benaissa, D. Briaud, P. Lescanne, and J. Rouyer-Degli. \u03bb\u03bd, a calculus of explicit substitutions which preserves strong normalisation, 1995. Available from http:\/\/www.loria.fr\/ lescanne\/publications.html.","DOI":"10.1017\/S0956796800001945"},{"key":"19_CR3","unstructured":"P.-L. Curien, T. Hardin, and J.-J. L\u00e9vy. Confluence properties of weak and strong calculi of explicit substitutions. Technical Report 1617, INRIA Rocquencourt, 1992."},{"key":"19_CR4","doi-asserted-by":"crossref","unstructured":"P.-L. Curien, T. Hardin, and A. R\u00edos. Strong normalisation of substitutions. In MFCS'92, number 629 in LNCS, pages 209\u2013218, 1992.","DOI":"10.1007\/3-540-55808-X_19"},{"issue":"35","key":"19_CR5","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"5","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., 5(35):381\u2013392, 1972.","journal-title":"Indag. Mat."},{"key":"19_CR6","first-page":"384","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):384\u2013356, 1978.","journal-title":"Indag. Mat."},{"key":"19_CR7","unstructured":"T. Ehrhard. Une s\u00e9mantique cat\u00e9gorique des types d\u00e9pendants. Application au calcul des constructions. Th\u00e8se de doctorat, Universit\u00e9 de Paris VII, 1988."},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"M. C. F. Ferreira, D. Kesner and L. Puel. \u03bb-calculi with explicit substitutions and composition which preserve \u03b2-strong normalization, 1996. Available via ftp at ftp.lri.fr\/LRI\/articles\/kesner\/psn.ps.gz.","DOI":"10.1007\/3-540-61735-3_19"},{"key":"19_CR9","unstructured":"T. Hardin and J.-J. L\u00e9vy. A confluent calculus of substitutions. In France-Japan Artificial Intelligence and Computer Science Symposium, 1989."},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"D. Kesner. Confluence properties of extensional and non-extensional \u03bb-calculi with explicit substitutions. In Proc. of the Seventh Int. Conf. RTA, 1996. To appear.","DOI":"10.1007\/3-540-61464-8_52"},{"key":"19_CR11","unstructured":"F. Kamareddine and A. R\u00edos. The confluence of the \u03bbse-calculus via a generalized interpretation method. Technical report TR-1996-19, Dep. of Computing Science, University of Glasgow, 1996."},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"F. Kamareddine and A. R\u00edos. A \u03bb-calculus \u00e0 la de Bruijn with explicit substitutions. In Proc. of the Int. Symposium on Programming Language Implementation and Logic Programming, number 982 in LNCS. Springer-Verlag, 1995.","DOI":"10.1007\/BFb0026813"},{"key":"19_CR13","unstructured":"P. Lescanne. Personal Communication. 1996."},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"P. Lescanne. From 298-01 to \u03bbv, a journey through calculi of explicit substitutions. In Ann. ACM Symp. POPL, pages 60\u201369. ACM, 1994.","DOI":"10.1145\/174675.174707"},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"P.-A. Mellies. Four typed-lambda calculi with explicit substitutions may not terminate: the first examples, 1994. Draft.","DOI":"10.1007\/BFb0014062"},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"P.-A. Mellies. Typed \u03bb-calculi with explicit substitutions may not terminate. In M. Dezani-Ciancaglini and G. Plotkin, editors, Proc. of Int. Conf. TLCA, number 902 in LNCS, April 1995.","DOI":"10.1007\/BFb0014062"},{"key":"19_CR17","unstructured":"C. Mu\u00f1oz. Confluence and preservation of strong normalisation in an explicit substitutions calculus. In Proc. of the Symposium LICS, 1996 To appear."},{"key":"19_CR18","unstructured":"A. R\u00edos. Contribution \u00e0 l'\u00e9tude des \u03bb-calculus avec substitutions explicites. Th\u00e8se de doctorat, Universit\u00e9 de Paris VII, 1993."}],"container-title":["Lecture Notes in Computer Science","Algebraic and Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61735-3_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:24:54Z","timestamp":1742599494000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61735-3_19"}},"subtitle":["Extended abstract"],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540617358","9783540706724"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-61735-3_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]},"assertion":[{"value":"1 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}