{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:00:14Z","timestamp":1725663614980},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540569398"},{"type":"electronic","value":"9783540478263"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-56939-1_109","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T11:56:56Z","timestamp":1330257416000},"page":"645-656","source":"Crossref","is-referenced-by-count":15,"title":["A confluent reduction for the extensional typed \u03bb-calculus with pairs, sums, recursion and terminal object"],"prefix":"10.1007","author":[{"given":"Roberto Di","family":"Cosmo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Delia","family":"Kesner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,28]]},"reference":[{"key":"53_CR1","unstructured":"Y. Akama. On mints' reductions for ccc-calculus. TLCA. LNCS 664, Springer Verlag, 1993."},{"key":"53_CR2","unstructured":"H. Barendregt. The Lambda Calculus; Its syntax and Semantics. North Holland, 1984."},{"key":"53_CR3","doi-asserted-by":"crossref","unstructured":"P.L. Curien and R. Di Cosmo. A confluent reduction system for the \u03bb-calculus with surjective pairing and terminal object. ICALP 91, LNCS 510, pages 291\u2013302.","DOI":"10.1007\/3-540-54233-7_142"},{"key":"53_CR4","unstructured":"H.B. Curry and R. Feys. Combinatory Logic, volume 1. North Holland, 1958."},{"key":"53_CR5","unstructured":"D. Cubric. On free ccc. Distributed on the types mailing list, 1992."},{"key":"53_CR6","doi-asserted-by":"crossref","unstructured":"R. Di Cosmo and D. Kesner. Simulating expansions without expansions. Technical report, INRIA, 1993.","DOI":"10.1017\/S0960129500000505"},{"key":"53_CR7","unstructured":"D. Dougherty. Some reduction properties of a lambda calculus with coproducts and recursive types. Technical report, Wesleyan University, 1990. E-mail: ddougherty@eagle.wesleyan.edu."},{"key":"53_CR8","unstructured":"J.Y. Girard. Interpr\u00e9tation fonctionelle et \u00e9limination des coupures dans l'arithm\u00e9tique d'ordre sup\u00e9rieure. Th\u00e8se de doctorat d'\u00e9tat, Universit\u00e9 de Paris VII, 1972."},{"key":"53_CR9","unstructured":"J.Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, 1990."},{"key":"53_CR10","unstructured":"G. Huet. R\u00e9solution d'\u00e9quations dans les langages d'ordre 1,2,..., \u03a9. Th\u00e8se de doctorat d'\u00e9tat, Universit\u00e9 de Paris VII, 1976."},{"key":"53_CR11","unstructured":"C. Barry Jay. Long \u0392\u03b7 normal forms and confluence (revised). Technical Report ECS-LFCS-91-183, LFCS, 1992. University of Edimburgh."},{"key":"53_CR12","unstructured":"C. Barry Jay and N. Ghani. The virtues of eta-expansion. Technical Report ECS-LFCS-92-243, LFCS, 1992. University of Edimburgh."},{"key":"53_CR13","unstructured":"J.W. Klop. Combinatory reduction systems. Mathematical Center Tracts, 27, 1980."},{"key":"53_CR14","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0304-3975(76)90009-8","volume":"2","author":"J. J. L\u00e9vy","year":"1976","unstructured":"J.J. L\u00e9vy. An algebraic interpretation of the \u03bb\u0392\u03ba-calculus and a labelled \u03bb-calculus. TCS, 2:97\u2013114, 1976.","journal-title":"TCS"},{"key":"53_CR15","unstructured":"J. Lambek and P.J. Scott. An introduction to higher order categorical logic. CUP, 1986."},{"key":"53_CR16","first-page":"83","volume":"68","author":"G. Mints","year":"1977","unstructured":"G. Mints. Closed categories and the theory of proofs. Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta im. V.A. Steklova AN SSSR, 68:83\u2013114, 1977.","journal-title":"Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta im. V.A. Steklova AN SSSR"},{"key":"53_CR17","unstructured":"G. Mints. Teorija categorii i teoria dokazatelstv.I. Aktualnye problemy logiki i metodologii nauky, pages 252\u2013278, 1979."},{"issue":"3","key":"53_CR18","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1305\/ndjfl\/1093883461","volume":"22","author":"G. Pottinger","year":"1981","unstructured":"G. Pottinger. The Church Rosser Theorem for the Typed lambda-calculus with Surjective Pairing. Notre Dame Journal of Formal Logic, 22(3):264\u2013268, 1981.","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"53_CR19","doi-asserted-by":"crossref","unstructured":"D. Prawitz. Ideas and results in proof theory. Proc. 2nd Scand. Logic Symp., pages 235\u2013307, 1971.","DOI":"10.1016\/S0049-237X(08)70849-8"},{"issue":"2\u20133","key":"53_CR20","first-page":"340","volume":"34","author":"A. Poign\u00e9","year":"1987","unstructured":"A. Poign\u00e9 and J. Voss. On the implementation of abstract data types by programming language constructs. JCSS, 34(2\u20133):340\u2013376, April\/June 1987.","journal-title":"JCSS"},{"key":"53_CR21","doi-asserted-by":"crossref","unstructured":"A.S. Troelstra. Strong normalization for typed terms with surjective pairing. Notre Dame Journal of Formal Logic, 27(4), 1986.","DOI":"10.1305\/ndjfl\/1093636767"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-56939-1_109.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:07:25Z","timestamp":1605647245000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-56939-1_109"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540569398","9783540478263"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-56939-1_109","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}