{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:17Z","timestamp":1779836717232,"version":"3.53.1"},"reference-count":25,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2008,11,7]],"date-time":"2008-11-07T00:00:00Z","timestamp":1226016000000},"content-version":"unspecified","delay-in-days":4634,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[1996,3]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    We exhibit confluent and effectively weakly normalizing (thus decidable) rewriting systems for the full equational theory underlying cartesian closed categories, and for polymorphic extensions of it. The \u03bb-calculus extended with surjective pairing has been well-studied in the last two decades. It is not confluent in the untyped case, and confluent in the typed case. But to the best of our knowledge the present work is the first treatment of the lambda calculus extended with surjective pairing\n                    <jats:italic>and<\/jats:italic>\n                    terminal object via a\n                    <jats:italic>confluent<\/jats:italic>\n                    rewriting system, and is the first solution to the decidability problem of the full equational theory of Cartesian Closed Categories extended with\n                    <jats:italic>polymorphic types<\/jats:italic>\n                    . Our approach yields conservativity results as well. In separate papers we apply our results to the study of provable type isomorphisms, and to the decidability of equality in a typed \u03bb-calculus with subtyping.\n                  <\/jats:p>","DOI":"10.1017\/s0956796800001696","type":"journal-article","created":{"date-parts":[[2008,11,7]],"date-time":"2008-11-07T11:11:13Z","timestamp":1226056273000},"page":"299-327","source":"Crossref","is-referenced-by-count":7,"title":["A confluent reduction for the \u03bb-calculus with surjective pairing and terminal object"],"prefix":"10.1017","volume":"6","author":[{"given":"Pierre-Louis","family":"Curien","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Roberto Di","family":"Cosmo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2008,11,7]]},"reference":[{"key":"S0956796800001696_ref025","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093636767"},{"key":"S0956796800001696_ref024","doi-asserted-by":"publisher","DOI":"10.2307\/2271658"},{"key":"S0956796800001696_ref023","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093883461"},{"key":"S0956796800001696_ref022","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(87)90029-8"},{"key":"S0956796800001696_ref021","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(87)90018-6"},{"key":"S0956796800001696_ref020","unstructured":"Nipkow T. (1990) A critical pair lemma for higher-order rewrite systems and its application to \u03bb*. In: First Annual Workshop on Logical Frameworks."},{"key":"S0956796800001696_ref019","unstructured":"Mints G. A simple proof of the coherence theorem for cartesian closed categories. Bibliopolis. To appear."},{"key":"S0956796800001696_ref018","volume-title":"An Introduction to Higher Order Categorical Logic","author":"Lambek","year":"1986"},{"key":"S0956796800001696_ref012","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500000505"},{"key":"S0956796800001696_ref014","volume-title":"Proofs and Types","author":"Girard","year":"1990"},{"key":"S0956796800001696_ref003","doi-asserted-by":"crossref","unstructured":"Breazu-Tannen V. (1988) Combining algebra and higher order types. In: Proceedings of the symposium on logic in computer science (LICS), pp. 82\u201390.","DOI":"10.1109\/LICS.1988.5103"},{"key":"S0956796800001696_ref006","unstructured":"Cubric D. (1992) On free CCC. Distributed on the types mailing list."},{"key":"S0956796800001696_ref004","doi-asserted-by":"crossref","unstructured":"Breazu-Tannen V. and Gallier J. (1994) Polymorphic rewiting preserves algebraic confluence. Information and Computation. To appear.","DOI":"10.1006\/inco.1994.1078"},{"key":"S0956796800001696_ref016","volume-title":"The Virtues of Eta-expansion","author":"Jay","year":"1992"},{"key":"S0956796800001696_ref008","unstructured":"de Vrijer R. C. (1987) Surjective pairing and strong normalization: two themes in \u03bb-calculus. Ph.D. thesis, Universiteit van Amsterdam."},{"key":"S0956796800001696_ref009","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(76)90085-2"},{"key":"S0956796800001696_ref001","first-page":"1","volume-title":"Typed lambda calculus and applications","author":"Akama","year":"1993"},{"key":"S0956796800001696_ref005","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001444"},{"key":"S0956796800001696_ref002","volume-title":"The lambda calculus; its syntax and semantics (revised edition)","author":"Barendregt","year":"1984"},{"key":"S0956796800001696_ref007","unstructured":"Curien P.lL. and Ghelli G. (1990) Confluence and decidability of \u03b2\u03b7top\u2264 reduction on F\u2264. Information and Computation. To appear."},{"key":"S0956796800001696_ref010","doi-asserted-by":"crossref","unstructured":"Di Cosmo R. (1994) Second order isomorphic types. A proof theoretic study on second order \u03bb-calculus with surjective pairing and terminal object. Information and Computation. To appear.","DOI":"10.1007\/978-1-4612-2572-0_5"},{"key":"S0956796800001696_ref011","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58201-0_90"},{"key":"S0956796800001696_ref013","doi-asserted-by":"crossref","unstructured":"Dougherty D. J. (1993) Some lambda calculi with categorical sums and products. In: Proceedings of the Fifth International Conference on Rewriting Techniques and Applications (RTA).","DOI":"10.1007\/3-540-56868-9_12"},{"key":"S0956796800001696_ref015","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(89)90105-9"},{"key":"S0956796800001696_ref017","article-title":"Combinatory reduction systems","volume":"27","author":"Klop","year":"1980","journal-title":"Mathematical Center Tracts"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796800001696","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:35:22Z","timestamp":1779834922000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796800001696\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,3]]},"references-count":25,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1996,3]]}},"alternative-id":["S0956796800001696"],"URL":"https:\/\/doi.org\/10.1017\/s0956796800001696","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996,3]]}}}