{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:56:03Z","timestamp":1725663363573},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540542339"},{"type":"electronic","value":"9783540475163"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3-540-54233-7_142","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T22:37:34Z","timestamp":1330209454000},"page":"291-302","source":"Crossref","is-referenced-by-count":13,"title":["A confluent reduction for the \u03bb-calculus with surjective pairing and terminal object"],"prefix":"10.1007","author":[{"given":"Pierre-Louis","family":"Curien","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roberto","family":"Cosmo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"22_CR1","unstructured":"Henk Barendregt. The Lambda Calculus; Its syntax and Semantics (revised edition). North Holland, 1984."},{"key":"22_CR2","unstructured":"Kim Bruce, Roberto Di Cosmo, and Giuseppe Longo. Provable isomorphisms of types. Technical Report 90\u201314, LIENS \u2014 Ecole Normale Sup\u00e9rieure, 1990. To appear in Proc. of Symposium on Symbolic Computation, ETH, Zurich, March 1990: MSCS."},{"key":"22_CR3","doi-asserted-by":"crossref","unstructured":"Pierre-Louis Curien and Roberto Di Cosmo. A confluent reduction system for the \u03bb-calculus with surjective pairing and terminal object. Technical Report, LIENS \u2014 Ecole Normale Sup\u00e9rieure, 1991. To appear.","DOI":"10.1007\/3-540-54233-7_142"},{"key":"22_CR4","unstructured":"Pierre-Louis Curien and Giorgio Ghelli. Subtyping and extensionality: decidability of \u03b2\u03b7top\u2264 on F\u2264. 1990. Draft."},{"key":"22_CR5","unstructured":"Roberto Di Cosmo. Invertibility of terms and valid isomorphisms. A proof theoretic study on second order \u03bb-calculus with surjective pairing and terminal object. Technical Report, LIENS \u2014 Ecole Normale Sup\u00e9rieure, 1991. To appear."},{"key":"22_CR6","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/0304-3975(76)90085-2","volume":"2","author":"M. Dezani-Ciancaglini","year":"1976","unstructured":"Mariangiola Dezani-Ciancaglini. Characterization of normal forms possessing an inverse in the \u03b3\u03b2\u03b7 calculus. Theoretical Computer Science, 2:323\u2013337, 1976.","journal-title":"Theoretical Computer Science"},{"key":"22_CR7","unstructured":"Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types. Cambridge University Press, 1990."},{"issue":"2","key":"22_CR8","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/0304-3975(89)90105-9","volume":"65","author":"T. Hardin","year":"1989","unstructured":"Th\u00e9r\u00e8se Hardin. Confluence results for the pure strong categorical logic C.C.L.; \u03bb-calculi as subsystems of c.c.l. Theoretical Computer Science, 65(2):291\u2013342, 1989.","journal-title":"Theoretical Computer Science"},{"key":"22_CR9","unstructured":"C. Barry Jay. Strong normalisation for simply-typed lambda-calculus as in lambek-scott. February 1991. LFCS, University of Edimburgh."},{"key":"22_CR10","unstructured":"Jan Wilhelm Klop. Combinatory reduction systems. Mathematical Center Tracts, 27, 1980."},{"key":"22_CR11","unstructured":"Joachim Lambek and Philip J. Scott. An introduction to higher order categorical logic. Cambridge University Press, 1986."},{"key":"22_CR12","unstructured":"Gregory Mints. A simple proof of the coherence theorem for cartesian closed categories. Bibliopolis, to appear."},{"key":"22_CR13","unstructured":"Tobias Nipkow. A critical pair lemma for higher-order rewrite systems and its application to \u03bb*. First Annual Workshop on Logical Frameworks, 1990."},{"issue":"2","key":"22_CR14","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1016\/0890-5401(87)90018-6","volume":"73","author":"A. Obtulowicz","year":"1987","unstructured":"Adam Obtulowicz. Algebra of constructions I. The Word Problem for Partial Algebras. Information and Computation, 73(2):129\u2013173, 1987.","journal-title":"Information and Computation"},{"issue":"3","key":"22_CR15","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1305\/ndjfl\/1093883461","volume":"22","author":"G. Pottinger","year":"1981","unstructured":"Garrel 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"},{"issue":"2\u20133","key":"22_CR16","doi-asserted-by":"crossref","first-page":"340","DOI":"10.1016\/0022-0000(87)90029-8","volume":"34","author":"A. Poign\u00e9","year":"1987","unstructured":"Axel Poign\u00e9 and Josef Voss. On the implementation of abstract data types by programming language constructs. Journal of Computer and System Science, 34(2\u20133):340\u2013376, April\/June 1987.","journal-title":"Journal of Computer and System Science"},{"key":"22_CR17","doi-asserted-by":"crossref","unstructured":"W.W. Tait. Intensional interpretation of functionals of finite type I. Journal of Symbolic Logic, 32, 1967.","DOI":"10.2307\/2271658"},{"key":"22_CR18","doi-asserted-by":"crossref","unstructured":"Ann 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-54233-7_142.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:53:13Z","timestamp":1605646393000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-54233-7_142"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540542339","9783540475163"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-54233-7_142","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}