{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T04:05:57Z","timestamp":1648872357834},"reference-count":19,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[1994,11,1]],"date-time":"1994-11-01T00:00:00Z","timestamp":783648000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["AAECC"],"published-print":{"date-parts":[[1994,11]]},"DOI":"10.1007\/bf01188746","type":"journal-article","created":{"date-parts":[[2005,2,17]],"date-time":"2005-02-17T21:01:13Z","timestamp":1108674073000},"page":"317-341","source":"Crossref","is-referenced-by-count":3,"title":["Eta-conversion for the languages of explicit substitutions"],"prefix":"10.1007","volume":"5","author":[{"given":"Th\ufffdr\ufffdse","family":"Hardin","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Cardelli, L., Curien, P.-L., L\u00e9vy, J.-J.: Explicit Substitutions. ACM Conference on Principle of Programming Languages, San Francisco, 1990","DOI":"10.1145\/96709.96712"},{"key":"CR2","volume-title":"The Lambda-Calculus. vol 103","author":"H. P. Barendregt","year":"1984","unstructured":"Barendregt, H. P.: The Lambda-Calculus. vol 103. Amsterdam: Elsevier Science 1984"},{"issue":"5","key":"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":"de Bruijn, N.: Lambda-calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser Theorem. Indag. Math.34(5), 381?392 (1972)","journal-title":"Indag. Math."},{"key":"CR4","doi-asserted-by":"crossref","first-page":"348","DOI":"10.1016\/S1385-7258(78)80025-0","volume":"40","author":"N. Bruijn de","year":"1978","unstructured":"de Bruijn, N.: Lambda-Calculus notation with namefree formulas involving symbols that represent reference transforming mappings. Indag. Math.40, 348?356 (1978)","journal-title":"Indag. Math."},{"key":"CR5","unstructured":"Church, A.: The Calculi of Lambda-Conversion. Ann. Math. Studies6 (1941)"},{"key":"CR6","volume-title":"Research Notes in Theoretical Computer Science","author":"P.-L. Curien","year":"1986","unstructured":"Curien, P.-L.: Categorical Combinators, Sequential Algorithms and Functional Programming. Research Notes in Theoretical Computer Science, Pitman, London 1986"},{"key":"CR7","unstructured":"Curien, P.-L., Hardin, T., L\u00e9vy, J.-J.: Confluence properties of weak and strong calculi of explicit substitutions. INRIA Report 1617"},{"key":"CR8","unstructured":"Hardin, T.: 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":"CR9","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/0304-3975(89)90105-9","volume":"65","author":"T. Hardin","year":"1989","unstructured":"Hardin, T.: Confluence Results for the Pure Strong Categorical Logic CCL. ?-calculi as subsystems of CCL. Theoret. Comput. Sci.,65, 291?342 (1989)","journal-title":"Theoret. Comput. Sci."},{"key":"CR10","volume-title":"Algebraic and Logic Programming'92, LNCS vol. 632","author":"T. Hardin","year":"1992","unstructured":"Hardin, T.: ?-reduction for explicit substitutions. Algebraic and Logic Programming'92, LNCS vol. 632. Berlin, Heidelberg, New York: Springer 1992"},{"key":"CR11","volume-title":"Rapport INRIA 1777","author":"T. Hardin","year":"1992","unstructured":"Hardin, T.: From Categorical Combinators to??-calculi, a quest for confluence, Rapport INRIA 1777 (1992), to appear in Term Graph Rewriting, M. R. Sleep, van Eckelen, Plasmeijer (Eds) New York: John Wiley"},{"key":"CR12","volume-title":"Report 90-11","author":"T. Hardin","year":"1989","unstructured":"Hardin, T., L\u00e9vy, J.-J.: A Confluent Calculus of Substitutions. France-Japan Artificial Intelligence and Computer Science Symposium, Izu, 1989. Report 90-11, C.N.A.M., 292 Rue Saint-Martin, 75141 Paris Cedex 03, France"},{"key":"CR13","volume-title":"London Mathematical Society Student texts","author":"R. Hindley","year":"1986","unstructured":"Hindley, R., Seldin, J.: Introduction to Combinators and?-calculus, Vol.1. London Mathematical Society Student texts, Cambridge: Cambridge University Press, 1986"},{"issue":"4","key":"CR14","first-page":"797","volume":"27","author":"G. Huet","year":"1980","unstructured":"Huet, G.: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems. J.A.C.M., vol27(4), pp. 797?821, October 1980","journal-title":"J.A.C.M."},{"key":"CR15","unstructured":"Klop, J. W.: Combinatory Reduction Systems, PhD, Mathematisch Centrum Amsterdam 1982"},{"key":"CR16","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1016\/B978-0-08-012975-4.50028-X","volume-title":"Comput. Problems in Abstract Algebra","author":"D. Knuth","year":"1970","unstructured":"Knuth, D., Bendix, P.: Simple Word Problems in Universal Algebras. In: Leech, J. (ed). Comput. Problems in Abstract Algebra, pp. 263?297. Pergamon Press. New York 1970"},{"key":"CR17","volume-title":"Technical Report 117","author":"X. Leroy","year":"1990","unstructured":"Leroy, X.: The ZINC experiment: an economical implementation of the ml language. Technical Report 117, INRIA, 78153, Le Chesnay Cedex, France, 1990"},{"key":"CR18","unstructured":"L\u00e9vy, J.-J.: R\u00e9ductions correctes and optimales dans le Lambda-Calcul, Th\u00e8se d'Etat, Universit\u00e9 de Paris 7, 1978"},{"key":"CR19","unstructured":"Rios, A.: Variations sur le calcul explicite de la substitution, Th\u00e8se, Universit\u00e9 Paris 7, 1992"}],"container-title":["Applicable Algebra in Engineering, Communication and Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01188746.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01188746\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01188746","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T16:41:48Z","timestamp":1556728908000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01188746"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994,11]]},"references-count":19,"journal-issue":{"issue":"6","published-print":{"date-parts":[[1994,11]]}},"alternative-id":["BF01188746"],"URL":"https:\/\/doi.org\/10.1007\/bf01188746","relation":{},"ISSN":["0938-1279","1432-0622"],"issn-type":[{"value":"0938-1279","type":"print"},{"value":"1432-0622","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994,11]]}}}