{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:38Z","timestamp":1749124058233},"publisher-location":"Berlin\/Heidelberg","reference-count":17,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354055873X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0013834","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T07:24:11Z","timestamp":1132730651000},"page":"306-321","source":"Crossref","is-referenced-by-count":7,"title":["Eta-conversion for the languages of explicit substitutions"],"prefix":"10.1007","author":[{"given":"Th\u00e9r\u00e8se","family":"Hardin","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","doi-asserted-by":"crossref","unstructured":"M. Abadi, L. Cardelli, P.-L. Curien, J.-J. L\u00e9vy, Explicit Substitutions, ACM Conference on Principle of Programming Languages, San Francisco, 1990.","DOI":"10.1145\/96709.96712"},{"key":"20_CR2","volume-title":"The Lambda-Calculus, vol 103","author":"H. P. Barendregt","year":"1984","unstructured":"H. P. Barendregt, The Lambda-Calculus, vol 103, Elsevier Science Publishing Company, Amsterdam, 1984."},{"issue":"5","key":"20_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, with application to the Church-Rosser Theorem, Indag. Math., 34(5), pp 381\u2013392, 1972.","journal-title":"Indag. Math."},{"key":"20_CR4","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 involing symbols that represent reference transforming mappings Indag. Math., 40, pp 348\u2013356, 1978.","journal-title":"Indag. Math."},{"key":"20_CR5","unstructured":"A. Church, The Calculi of Lambda-Conversion, Ann. of Math. Studies, 6, 1941."},{"key":"20_CR6","volume-title":"Research Notes in Theoretical Computer Science","author":"P.-L. Curien","year":"1986","unstructured":"P.-L. Curien, Categorical Combinators, Sequential Algorithms and Functional Programming, Research Notes in Theoretical Computer Science, Pitman, London, 1986."},{"key":"20_CR7","unstructured":"P.-L. Curien, T. Hardin, Yet Yet Another Counterexample for Lambda-calculus with Surjective Pairing, Communication in forum Types (1990)."},{"key":"20_CR8","unstructured":"Curien, P.-L., Hardin, T., L\u00e9vy, J.-J., Confluence properties of weak and strong calculi of explicit substitutions, submitted to J.A.C.M. Report CNAM 92-1 and report INRIA."},{"key":"20_CR9","unstructured":"T. Hardin, R\u00e9sultats de confluence pour les R\u00e8gles fortes de la Logique Combinatoire Cat\u00e9gorique et Liens avec les Lambda-calculs, th\u00e8se de Doctorat, Universit\u00e9 de Paris 7, 1987."},{"key":"20_CR10","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 Sc., 65, pp 291\u2013342, 1989.","journal-title":"Theoretical Computer Sc."},{"key":"20_CR11","unstructured":"T. Hardin, Eta-conversion for the languages of explicit substitutions. Report 92-04, C.N.A.M., 292 Rue Saint-Martin, 75141 Paris Cedex 03, France."},{"key":"20_CR12","volume-title":"Report 90-11","author":"T. Hardin","year":"1989","unstructured":"T. Hardin, J.-J. L\u00e9vy, A Confluent Calculus of Substitutions, France-Japan Artificial Intelligence and Computer Science Symposium, Izu, 1989. Report 90-11, C.N.A.M., Paris"},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"R. Hindley and J. Seldin, Introduction to Combinators and \u03bb-calculus, Volume 1 of London Mathematical Society Student texts, Cambridge University Press, 1986.","DOI":"10.1017\/CBO9780511809835.002"},{"issue":"4","key":"20_CR14","first-page":"797","volume":"27","author":"G. Huet","year":"1980","unstructured":"G. Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems, J.A.C.M., vol 27(4), pp 797\u2013821, October 1980.","journal-title":"J.A.C.M."},{"key":"20_CR15","unstructured":"J. W. Klop, Combinatory Reduction Systems, PhD, Mathematisch Centrum Amsterdam, 1982."},{"key":"20_CR16","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, pp 263\u2013297, Pergamon, 1970.","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"20_CR17","unstructured":"J.-J. L\u00e9vy, R\u00e9ductions correctes and optimales dans le Lambda-Calcul, Th\u00e8se d'Etat, Universit\u00e9 de Paris 7, 1978."}],"container-title":["Lecture Notes in Computer Science","Algebraic and Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/BFb0013834","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,5]],"date-time":"2023-05-05T15:40:19Z","timestamp":1683301219000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0013834"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354055873X"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/bfb0013834","relation":{},"subject":[]}}