{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:53:56Z","timestamp":1776891236669,"version":"3.51.2"},"reference-count":25,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","issue":"2","license":[{"start":{"date-parts":[[2008,11,7]],"date-time":"2008-11-07T00:00:00Z","timestamp":1226016000000},"content-version":"unspecified","delay-in-days":4969,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[1995,4]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Interpreting \u03b7-conversion as an expansion rule in the simply-typed \u03bb-calculus maintains the confluence of reduction in a richer type structure. This use of expansions is supported by categorical models of reduction, where \u03b2-contraction, as the local counit, and \u03b7-expansion, as the local unit, are linked by local triangle laws. The latter form reduction loops, but strong normalization (to the long \u03b2\u03b7-normal forms) can be recovered by \u2018cutting\u2019 the loops.<\/jats:p>","DOI":"10.1017\/s0956796800001301","type":"journal-article","created":{"date-parts":[[2008,11,7]],"date-time":"2008-11-07T11:12:15Z","timestamp":1226056335000},"page":"135-154","source":"Crossref","is-referenced-by-count":34,"title":["The virtues of eta-expansion"],"prefix":"10.46298","volume":"5","author":[{"given":"C. Barry","family":"Jay","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Neil","family":"Ghani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2008,11,7]]},"reference":[{"key":"S0956796800001301_ref014","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(88)90124-7"},{"key":"S0956796800001301_ref024","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-18508-9_23"},{"key":"S0956796800001301_ref009","volume-title":"Formal category theory: Adjointness for 2-categories: Lecture Notes in Mathematics","volume":"391","author":"J.W. Gray J. W.","year":"1974"},{"key":"S0956796800001301_ref008","volume-title":"Proofs and Types","author":"Girard","year":"1989"},{"key":"S0956796800001301_ref005","first-page":"291","volume-title":"Proc. ICALP: Lecture Notes in Computer Science","volume":"510","author":"Curien","year":"1991"},{"key":"S0956796800001301_ref006","volume-title":"Proc. ICALP: Lecture Notes in Computer Science","volume":"700","author":"Di Cosmo","year":"1993"},{"key":"S0956796800001301_ref001","first-page":"1","volume-title":"On Mints' Reduction for ccc-Calculus. Lecture Notes in Computer Science Vol. 664","author":"Akama","year":"1993"},{"key":"S0956796800001301_ref011","unstructured":"Hilken B. P. and Rydeheard D. E. (1994) Towards a categorical semantics of type classes. Fundamenta Informatica (to appear)."},{"key":"S0956796800001301_ref007","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/3-540-56868-9_12","volume-title":"Rewriting Techniques and Applications: Lecture Notes in Computer Science","volume":"690","author":"D.","year":"1993"},{"key":"S0956796800001301_ref004","unstructured":"\u010cubri\u0107 D. Embedding of a free CCC into the category of Sets, unpublished manuscript."},{"key":"S0956796800001301_ref012","volume-title":"Pre-adjunctions in Order Enriched Categories","author":"Hoare","year":"1989"},{"key":"S0956796800001301_ref017","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511525902.009"},{"key":"S0956796800001301_ref013","volume-title":"R\u00e9solution d'\u00e9quations dans des langages d'ordre 1,2,\u2026,\u03c9","author":"Huet","year":"1976"},{"key":"S0956796800001301_ref020","first-page":"23","article-title":"Cofibrations and the realization of non deterministic automata","volume":"24","author":"Kasangian","year":"1983","journal-title":"Cahiers de Topologie et G\u00e9ometrie Diff\u00e9rentielle"},{"key":"S0956796800001301_ref002","volume-title":"The Lambda Calculus Its Syntax and Semantics (Revised Ed.). Studies in Logic and the Foundations of Mathematics 103","author":"Barendregt","year":"1984"},{"key":"S0956796800001301_ref016","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-3182-3_10"},{"key":"S0956796800001301_ref003","unstructured":"Carboni A. , Kelly G. M. and Wood R. (1990) A 2-categorical approach to change of base and geometric morphisms I. Sydney Category Seminar Reports 90-1."},{"key":"S0956796800001301_ref018","unstructured":"Jay C. B. (1991) Long \u03b2\u03b7 Normal Forms and Confluence. Tech. Rep. LFCS-91-183 (and its revised version)."},{"key":"S0956796800001301_ref019","unstructured":"Kahrs S. (1991) \u03bb-rewriting. PhD thesis, Universit\u00e4t Bremen (in German)."},{"key":"S0956796800001301_ref025","volume-title":"Proc. Second Annual Symposium on Logic in Computer Science","author":"Seely","year":"1987"},{"key":"S0956796800001301_ref015","unstructured":"Jay C. B. (1990) Extending properties to categories of partial maps. Tech. Rep. LFCS-90-107."},{"key":"S0956796800001301_ref010","unstructured":"Harper R. , Honsell F. and Plotkin G. (1991) A framework for defining logics. Tech. Rep. LFCS-91-162."},{"key":"S0956796800001301_ref021","volume-title":"Introduction to higher order categorical logic","author":"Lambek","year":"1986"},{"key":"S0956796800001301_ref022","unstructured":"Mints G. E. (1979) Teorija categorii i teoria dokazatelstv.I., in: Aktualnye problemy logiki i metodologii nauky, Kiev, pp. 252\u2013278."},{"key":"S0956796800001301_ref023","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70849-8"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796800001301","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:18:05Z","timestamp":1776889085000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796800001301\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,4]]},"references-count":25,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1995,4]]}},"alternative-id":["S0956796800001301"],"URL":"https:\/\/doi.org\/10.1017\/s0956796800001301","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,4]]}}}