{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,1]],"date-time":"2025-03-01T05:34:10Z","timestamp":1740807250242,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642175107"},{"type":"electronic","value":"9783642175114"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-17511-4_11","type":"book-chapter","created":{"date-parts":[[2010,12,7]],"date-time":"2010-12-07T06:24:40Z","timestamp":1291703080000},"page":"173-191","source":"Crossref","is-referenced-by-count":3,"title":["Logic and Computation in a Lambda Calculus with Intersection and Union Types"],"prefix":"10.1007","author":[{"given":"Daniel J.","family":"Dougherty","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luigi","family":"Liquori","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0037094","volume-title":"Typed Lambda Calculi and Applications","author":"Y. Akama","year":"1993","unstructured":"Akama, Y.: On Mints\u2019 reduction for ccc-calculus. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664, pp. 1\u201312. Springer, Heidelberg (1993)"},{"doi-asserted-by":"crossref","unstructured":"Altenkirch, T., Dybjer, P., Hofmann, M., Scott, P.J.: Normalization by evaluation for typed lambda calculus with coproducts. In: LICS, pp. 303\u2013310 (2001)","key":"11_CR2","DOI":"10.1109\/LICS.2001.932506"},{"issue":"2","key":"11_CR3","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1006\/inco.1995.1086","volume":"119","author":"F. Barbanera","year":"1995","unstructured":"Barbanera, F., Dezani-Ciancaglini, M., De\u2019Liguoro, U.: Intersection and union types: syntax and semantics. Inf. Comput.\u00a0119(2), 202\u2013230 (1995)","journal-title":"Inf. Comput."},{"issue":"2","key":"11_CR4","first-page":"180","volume":"50","author":"B. Capitani","year":"2001","unstructured":"Capitani, B., Loreti, M., Venneri, B.: Hyperformulae, Parallel Deductions and Intersection Types. BOTH, Electr. Notes Theor. Comput. Sci.\u00a050(2), 180\u2013198 (2001)","journal-title":"BOTH, Electr. Notes Theor. Comput. Sci."},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"645","DOI":"10.1007\/3-540-56939-1_109","volume-title":"Automata, Languages and Programming","author":"R. Cosmo Di","year":"1993","unstructured":"Di Cosmo, R., Kesner, D.: A confluent reduction for the extensional typed lambda-calculus with pairs, sums, recursion and terminal object. In: Lingas, A., Carlsson, S., Karlsson, R. (eds.) ICALP 1993. LNCS, vol.\u00a0700, pp. 645\u2013656. Springer, Heidelberg (1993)"},{"unstructured":"Cubric, D.: Embedding of a free cartesian closed category into the category of sets. McGill University (1992) (manuscript)","key":"11_CR6"},{"issue":"2","key":"11_CR7","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1017\/S0956796800001696","volume":"6","author":"P.-L. Curien","year":"1996","unstructured":"Curien, P.-L., Di Cosmo, R.: A confluent reduction for the lambda-calculus with surjective pairing and terminal object. J. Funct. Program.\u00a06(2), 299\u2013327 (1996)","journal-title":"J. Funct. Program."},{"issue":"1","key":"11_CR8","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1017\/S0960129500001134","volume":"2","author":"P.-L. Curien","year":"1992","unstructured":"Curien, P.-L., Ghelli, G.: Coherence of subsumption, minimum typing and type-checking in F $_{\\mbox{$<$=}}$ . Mathematical Structures in Computer Science\u00a02(1), 55\u201391 (1992)","journal-title":"Mathematical Structures in Computer Science"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/3-540-56868-9_12","volume-title":"Rewriting Techniques and Applications","author":"D.J. Dougherty","year":"1993","unstructured":"Dougherty, D.J.: Some lambda calculi with categorical sums and products. In: Kirchner, C. (ed.) RTA 1993. LNCS, vol.\u00a0690, pp. 137\u2013151. Springer, Heidelberg (1993)"},{"issue":"1,2","key":"11_CR10","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1006\/inco.1999.2833","volume":"157","author":"D.J. Dougherty","year":"2000","unstructured":"Dougherty, D.J., Subrahmanyam, R.: Equality between functionals in the presence of coproducts. Information and Computation\u00a0157(1,2), 52\u201383 (2000)","journal-title":"Information and Computation"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/BFb0014052","volume-title":"Typed Lambda Calculi and Applications","author":"N. Ghani","year":"1995","unstructured":"Ghani, N.: \u00dfn-equality for coproducts. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol.\u00a0902, pp. 171\u2013185. Springer, Heidelberg (1995)"},{"issue":"2","key":"11_CR12","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1017\/S0956796800001301","volume":"5","author":"C.B. Jay","year":"1995","unstructured":"Jay, C.B., Ghani, N.: The virtues of eta-expansion. J. Funct. Program.\u00a05(2), 135\u2013154 (1995)","journal-title":"J. Funct. Program."},{"key":"11_CR13","series-title":"LNM","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/BFb0059699","volume-title":"Symposium on Semantics and Algorithmic Languages","author":"D.E. Knuth","year":"1970","unstructured":"Knuth, D.E.: Examples of formal semantics. In: Engeler, E. (ed.) Symposium on Semantics and Algorithmic Languages. LNM, vol.\u00a0188, pp. 212\u2013235. Springer, Heidelberg (1970)"},{"key":"11_CR14","series-title":"Cambridge Studies in Advanced Mathematics","volume-title":"Introduction to Higher-order Categorical Logic","author":"J. Lambek","year":"1986","unstructured":"Lambek, J., Scott, P.: Introduction to Higher-order Categorical Logic. Cambridge Studies in Advanced Mathematics, vol.\u00a07. Cambridge University Press, Cambridge (1986)"},{"issue":"205","key":"11_CR15","doi-asserted-by":"publisher","first-page":"1371","DOI":"10.1016\/j.ic.2007.03.005","volume":"9","author":"L. Liquori","year":"2007","unstructured":"Liquori, L., Ronchi Della Rocca, S.: Intersection typed system \u00e0 la Church. Information and Computation\u00a09(205), 1371\u20131386 (2007)","journal-title":"Information and Computation"},{"key":"11_CR16","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/S0019-9958(86)80019-5","volume":"71","author":"D. MacQueen","year":"1986","unstructured":"MacQueen, D., Plotkin, G., Sethi, R.: An ideal model for recursive polymorphic types. Information and Control\u00a071, 95\u2013130 (1986)","journal-title":"Information and Control"},{"issue":"2","key":"11_CR17","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1017\/S0956796800001040","volume":"4","author":"B.C. Pierce","year":"1994","unstructured":"Pierce, B.C., Turner, D.N.: Simple type-theoretic foundations for object-oriented programming. Journal of Functional Programming\u00a04(2), 207\u2013247 (1994)","journal-title":"Journal of Functional Programming"},{"key":"11_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/3-540-10250-7_24","volume-title":"Semantics-Directed Compiler Generation","author":"J.C. Reynolds","year":"1980","unstructured":"Reynolds, J.C.: Using category theory to design implicit conversions and generic op erators. In: Jones, N.D. (ed.) Semantics-Directed Compiler Generation. LNCS, vol.\u00a094, pp. 211\u2013258. Springer, Heidelberg (1980)"},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1007\/3-540-54415-1_70","volume-title":"Theoretical Aspects of Computer Software","author":"J.C. Reynolds","year":"1991","unstructured":"Reynolds, J.C.: The coherence of languages with intersection types. In: Ito, T., Meyer, A.R. (eds.) TACS 1991. LNCS, vol.\u00a0526, pp. 675\u2013700. Springer, Heidelberg (1991)"},{"unstructured":"Reynolds, J.C.: Design of the programming language Forsythe. Report CMU\u2013CS\u201396\u2013146, Carnegie Mellon University, Pittsburgh, Pennsylvania, June 28 (1996)","key":"11_CR20"},{"key":"11_CR21","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511626364","volume-title":"Theories of Programming Languages","author":"J.C. Reynolds","year":"1998","unstructured":"Reynolds, J.C.: Theories of Programming Languages. Cambridge University Press, Cambridge (1998)"},{"doi-asserted-by":"crossref","unstructured":"Ronchi Della Rocca, S.: Intersection typed lambda-calculus. Electr. Notes Theor. Comput. Sci.\u00a070(1) (2002)","key":"11_CR22","DOI":"10.1016\/S1571-0661(04)80496-1"},{"key":"11_CR23","series-title":"Lecture Notes in Computer Science","first-page":"421","volume-title":"Computer Science Logic","author":"S. Ronchi Della Rocca","year":"2001","unstructured":"Ronchi Della Rocca, S., Roversi, L.: Intersection logic. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142, pp. 421\u2013428. Springer, Heidelberg (2001)"},{"issue":"1","key":"11_CR24","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1016\/0890-5401(91)90055-7","volume":"93","author":"V. Tannen","year":"1991","unstructured":"Tannen, V., Coquand, T., Gunter, C.A., Scedrov, A.: Inheritance as implicit coercion. Inf. Comput.\u00a093(1), 172\u2013221 (1991)","journal-title":"Inf. Comput."},{"issue":"3","key":"11_CR25","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/S0168-0072(96)00036-X","volume":"86","author":"S. Bakel van","year":"1997","unstructured":"van Bakel, S., Liquori, L., Ronchi della Rocca, S., Urzyczyn, P.: Comparing Cubes of Typed and Type Assignment System. Annal of Pure and Applied Logics\u00a086(3), 267\u2013303 (1997)","journal-title":"Annal of Pure and Applied Logics"},{"key":"11_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/3-540-45927-8_9","volume-title":"Programming Languages and Systems","author":"J.B. Wells","year":"2002","unstructured":"Wells, J.B., Haack, C.: Branching types. In: Le M\u00e9tayer, D. (ed.) ESOP 2002. LNCS, vol.\u00a02305, pp. 115\u2013132. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-17511-4_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,28]],"date-time":"2025-02-28T14:05:43Z","timestamp":1740751543000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-17511-4_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642175107","9783642175114"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-17511-4_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}