{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:08:31Z","timestamp":1763467711175},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540590484"},{"type":"electronic","value":"9783540491781"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bfb0014052","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T07:50:31Z","timestamp":1132732231000},"page":"171-185","source":"Crossref","is-referenced-by-count":19,"title":["\u03b2\u03b7-Equality for coproducts"],"prefix":"10.1007","author":[{"given":"Neil","family":"Ghani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"12_CR1","unstructured":"Y. Akama, On Mints' Reduction for ccc-Calculus, in Typed Lambda Calculi and Applications, 1993."},{"key":"12_CR2","unstructured":"H.P. Barendregt, The Lambda Calculus Its Syntax and Semantics (Revised Edition) Studies in Logic and the Foundations of Mathematics 103 (North Holland, 1984)."},{"key":"12_CR3","unstructured":"D. \u010cubri\u0107, On Free CCC, manuscript."},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"N. Dershowitz, J.P. Jouannaud, Rewrite Systems, in The Handbook of Theoretical Computer Science, Elsevier, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"12_CR5","unstructured":"R. Di Cosmo and D. Kesner, A confluent reduction for the extensional typed \u03bb-calculus, in Proceedings ICALP '93"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"D. Dougherty, Some \u03bb-calculi with categorical sums and products, in Rewriting Techniques and Applications LNCS 690, 137\u2013151.","DOI":"10.1007\/3-540-56868-9_12"},{"key":"12_CR7","unstructured":"J-Y. Girard, P. Taylor and Y. Lafont, Proofs and Types, Cambridge Tracts in Theoretical Computer Science (Cambridge University Press, 1989)."},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"J.W. Gray, Formal category theory: adjointness for 2-categories, Lecture Notes in Mathematics 391 (Springer-Verlag, 1974).","DOI":"10.1007\/BFb0061280"},{"key":"12_CR9","unstructured":"G. Huet, R\u00e9solution d'\u00e9quations dans des langages d'ordre 1, 2, \u22ef, \u03c9. Th\u00e8se d'Etat, Universit\u00e9 de Paris VII, 1976."},{"issue":"No4","key":"12_CR10","doi-asserted-by":"publisher","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"G. Huet","year":"1980","unstructured":"G. Huet, Abstract Properties and Applications of Term Rewriting Systems, in JACM, Vol. 27, No 4, pp. 797\u2013821, 1980.","journal-title":"JACM"},{"key":"12_CR11","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/0022-4049(88)90124-7","volume":"53","author":"C.B. Jay","year":"1988","unstructured":"C.B. Jay, Local adjunctions, J. Pure and Appl. Alg. 53 (1988) 227\u2013238.","journal-title":"J. Pure and Appl. Alg."},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"C.B. Jay, Modelling reduction in confluent categories, in: Proceedings of the Durham Symposium on Applications of Categories in Computer Science, Lecture Note Series 177 (London Mathematics Society, 1992) 143\u2013162.","DOI":"10.1017\/CBO9780511525902.009"},{"key":"12_CR13","unstructured":"C.B. Jay and N. Ghani, The Virtues of Eta-expansion, to appear in Journal of Functional Programming."},{"key":"12_CR14","unstructured":"J. Lambek and P. Scott, Introduction to higher order categorical logic, Cambridge Studies in Advanced Mathematics 7 (Cambridge Univ. Press, 1986)."},{"key":"12_CR15","unstructured":"G.E. Mints, Teorija categorii i teoria dokazatelstv.I., in: Aktualnye problemy logiki i metodologii nauky, Kiev, 1979 252\u2013278."},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"D. Prawitz, Ideas and results in proof theory, in: J.E. Fenstad (ed) Proc. 2nd Scandinavian Logic Symp. (North-Holland, 1971) 235\u2013307.","DOI":"10.1016\/S0049-237X(08)70849-8"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"D.E. Rydeheard & J.G. Stell, Foundations of equational deduction: A categorical treatment of equational proofs and unification algorithms, in: Pitt et al, (eds), Category Theory and Computer Science, Lecture Notes in Computer Science 283 (Springer, 1987) 114\u2013139.","DOI":"10.1007\/3-540-18508-9_23"},{"key":"12_CR18","unstructured":"R.A.G. Seely, Modelling computations: a 2-categorical framework, in: Proceedings of the Second Annual Symposium on Logic in Computer Science (1987)."}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0014052","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T04:37:47Z","timestamp":1586579867000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0014052"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540590484","9783540491781"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/bfb0014052","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}