{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T00:53:52Z","timestamp":1776214432158,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":8,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540590484","type":"print"},{"value":"9783540491781","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bfb0014062","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T07:50:31Z","timestamp":1132732231000},"page":"328-334","source":"Crossref","is-referenced-by-count":58,"title":["Typed \u03bb-calculi with explicit substitutions may not terminate"],"prefix":"10.1007","author":[{"given":"Paul-Andr\u00e9","family":"Mellies","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"22_CR1","unstructured":"C.P. Wadsworth. Semantics and Pragmatics of the Lambda Calculus. PhD thesis, Oxford Universtity, 1971."},{"issue":"4","key":"22_CR2","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 J.-J. L\u00e9vy. Explicit substitutions. Journal of Functionnal Programming, 1(4):375\u2013416, 1991.","journal-title":"Journal of Functionnal Programming"},{"key":"22_CR3","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. Indag. Mat., 34:381\u2013392, 1972.","journal-title":"Indag. Mat."},{"key":"22_CR4","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1016\/0304-3975(86)90035-6","volume":"46","author":"T. Hardin","year":"1986","unstructured":"T. Hardin 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":"22_CR5","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/3-540-55808-X_19","volume":"629","author":"P.-L. Curien","year":"1992","unstructured":"P.-L. Curien T. Hardin A. R\u00edos. Strong normalization of substitutions. Lecture Notes in Computer Science, 629:209\u2013217, 1992.","journal-title":"Lecture Notes in Computer Science"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"H. Zantema. Termination of term rewriting by interpretation. Lecture Notes in Computer Science, 656, 1993.","DOI":"10.1007\/3-540-56393-8_12"},{"key":"22_CR7","unstructured":"P. Lescanne J. Rouyer-Degli. The calculus of explicit substitutions \u03bb\u03c5. Submitted to the Journal of Functionnal Programming. 1993."},{"key":"22_CR8","unstructured":"T. Hardin, J.-J. L\u00e9vy, A Confluent Calculus of Substitutions, France-Japan Artificial Intelligence and Computer Science Symposium, Izu, 1989."}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0014062","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,5]],"date-time":"2019-02-05T10:10:49Z","timestamp":1549361449000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0014062"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540590484","9783540491781"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/bfb0014062","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995]]}}}