{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,30]],"date-time":"2025-12-30T23:48:44Z","timestamp":1767138524055,"version":"build-2238731810"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540568681","type":"print"},{"value":"9783662215517","type":"electronic"}],"license":[{"start":{"date-parts":[[1993,1,1]],"date-time":"1993-01-01T00:00:00Z","timestamp":725846400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[1993,1,1]],"date-time":"1993-01-01T00:00:00Z","timestamp":725846400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/978-3-662-21551-7_12","type":"book-chapter","created":{"date-parts":[[2022,7,19]],"date-time":"2022-07-19T05:30:08Z","timestamp":1658208608000},"page":"137-151","source":"Crossref","is-referenced-by-count":21,"title":["Some lambda calculi with categorical sums and products"],"prefix":"10.1007","author":[{"given":"Daniel J.","family":"Dougherty","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","unstructured":"Y. Akama. On Mint's Reduction for ccc-Calculus. Proc. Typed Lambda Calculus and Applications 1993."},{"key":"12_CR2","volume-title":"Volume 103 of Studies in Logic and the Foundations of Mathematics","author":"H. P. Barendregt","year":"1984","unstructured":"H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. Volume 103 of Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, 1981. Revised edition, 1984.","edition":"Revised edition"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"P-L Curien, R. Di Cosmo. A confluent reduction system for the \u03bb-calculus with surjective pairing and terminal object, in Leach et. al. (eds.), Int'l. Conf. on Automata, Languages, and Programming, LNCS 510, 291\u2013302, Springer Verlag 1991.","DOI":"10.1007\/3-540-54233-7_142"},{"key":"12_CR4","unstructured":"D. Cubric. Embedding of a free cartesian closed category into the category of Sets. Manuscript, McGill University 1992."},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"R. Di Cosmo, D. Kesner. Simulating expansions without expansions. Tech Rep, INRIA 1993.","DOI":"10.1017\/S0960129500000505"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"R. Di Cosmo, D. Kesner. A confluent reduction system for the extensional \u03bb-calculus with pairs, sums, recursion and terminal object. Proc ICALP 1993.","DOI":"10.1007\/3-540-56939-1_109"},{"key":"12_CR7","first-page":"243","volume-title":"Handbook of Theoretical Computer Science","author":"N. Dershowitz","year":"1991","unstructured":"N. Dershowitz, J.-P. Jounnaud. Term Rewriting Systems, in Handbook of Theoretical Computer Science, 243\u2013320, North-Holland, Amsterdam, 1991."},{"key":"12_CR8","unstructured":"D. J. Dougherty. Some reduction properties of a \u03bb-calculus with categorical sums and products. Manuscript, Wesleyan University 1990."},{"key":"12_CR9","volume-title":"To H. B. Curry, Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"R. O. Gandy","year":"1980","unstructured":"R. O. Gandy. Proofs of strong normalization, in J. P. Seldin and J. R. Hindley (eds.) To H. B. Curry, Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, New York, 1980."},{"key":"12_CR10","unstructured":"C. Barry Jay. Long \u03b2-normal forms and confluence. Manuscript, University of Edinburgh, 1991."},{"key":"12_CR11","volume-title":"Mathematical Centre Tracts, v. 127","author":"J. W. Klop","year":"1980","unstructured":"J. W. Klop. Combinatory Reduction Systems. Mathematical Centre Tracts, v. 127. Centre for Mathematics and Computer Science, Amsterdam 1980."},{"issue":"no.2","key":"12_CR12","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/0890-5401(89)90014-X","volume":"80","author":"J. W. Klop","year":"1989","unstructured":"J. W. Klop, R.C. DeVrijer. Unique normal forms for lambda calculus with surjective pairing. Information and Computation, v.80 no. 2, 97\u2013113, 1989.","journal-title":"Information and Computation"},{"key":"12_CR13","unstructured":"J. Lambek, P. Scott. Introduction to Higher-order Categorical Logic. Cambridge Studies in Advanced Mathematics 7. Cambridge University Press 1986."},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"F. W. Lawvere. Diagonal arguments and cartesian closed categories, in Category Theory, Homology Theory, and Their Applications II, LNM 92, Springer-Verlag, 1969.","DOI":"10.1007\/BFb0080769"},{"key":"12_CR15","unstructured":"G. E. Mints. Category Theory and Proof Theory. In Aktualnie Voprosi Logiki i Metodologiinauki (Russian) 252\u2013278. Kiev, 1980."},{"key":"12_CR16","unstructured":"M. Okada, P. Scott. Rewriting theory for uniqueness conditions: coproducts. Talk presented First Montreal Workshop on Programming Language Theory, April 1991."},{"key":"12_CR17","volume-title":"Proceedings of the Second Scandinavian Logic Symposium","author":"D. Prawitz","year":"1971","unstructured":"D. Prawitz. Ideas and Results in Proof Theory, in J. E. Fenstad, ed., Proceedings of the Second Scandinavian Logic Symposium. North-Holland, Amsterdam, 1971."},{"key":"12_CR18","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1016\/0022-0000(87)90029-8","volume":"34","author":"A. Poign\u00e9","year":"1987","unstructured":"A. Poign\u00e9, J. Voss. On the implementation of Abstract Data Types by Programming Language Constructs. Journal of Computer and System Science\n                34 (1987), 340\u2013376.","journal-title":"Journal of Computer and System Science"},{"key":"12_CR19","doi-asserted-by":"publisher","first-page":"198","DOI":"10.2307\/2271658","volume":"32","author":"W. W. Tait","year":"1967","unstructured":"W. W. Tait. Intensional interpretation of functionals of finite type I, J. Symbolic Logic\n                32, pp. 198\u2013212, 1967.","journal-title":"J. Symbolic Logic"},{"key":"12_CR20","first-page":"473","volume":"90\/4","author":"R. C. de Vrijer","year":"1987","unstructured":"R. C. de Vrijer, Strong Normalization in N \u2014 HA\n                \n                  \u03c9\n                . Proc. Koninklijke Nederlandse Akademie van Wetenschappen Series A, 90\/4, pp. 473\u2013478, 1987.","journal-title":"Proc. Koninklijke Nederlandse Akademie van Wetenschappen Series A"}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-21551-7_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,19]],"date-time":"2022-07-19T05:30:29Z","timestamp":1658208629000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-21551-7_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540568681","9783662215517"],"references-count":20,"aliases":["10.1007\/3-540-56868-9_12"],"URL":"https:\/\/doi.org\/10.1007\/978-3-662-21551-7_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993]]}}}