{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:28:17Z","timestamp":1761611297387,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540544159"},{"type":"electronic","value":"9783540476177"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3-540-54415-1_69","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T22:47:22Z","timestamp":1330210042000},"page":"651-674","source":"Crossref","is-referenced-by-count":11,"title":["Intersection and union types"],"prefix":"10.1007","author":[{"given":"Franco","family":"Barbanera","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mariangiola","family":"Dezani-Ciancaglini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"32_CR1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0168-0072(91)90065-T","volume":"51","author":"S. Abramsky","year":"1991","unstructured":"Abramsky S., Domain Theory in Logical Form, Annals of Pure and Applied Logics 51 (1991), 1\u201377.","journal-title":"Annals of Pure and Applied Logics"},{"key":"32_CR2","unstructured":"Altenkirch T., Ein Konstruktiver Ansatz zur Konjunktiven Typisierung des \u03bb-kalkuls, Diplomarbeit, TU Berlin, (1983)."},{"key":"32_CR3","unstructured":"Barendregt H.P., The Lambda Calculus: its Syntax and Semantics, Studies in Logic and the Foundations of Math. 103, North-Holland, (1984)."},{"key":"32_CR4","doi-asserted-by":"crossref","first-page":"931","DOI":"10.2307\/2273659","volume":"48","author":"H.P. Barendregt","year":"1983","unstructured":"Barendregt H.P., Coppo M., Dezani-Ciancaglini M., A Filter Lambda Model and the Completeness of Type Assignment, J. Symbolic Logic 48 (1983), 931\u2013940.","journal-title":"J. Symbolic Logic"},{"key":"32_CR5","unstructured":"Berarducci A., Programmazione Funzionale e Rappresentabilit\u00e0 in alcuni sistemi di Logica Combinatoria, Tesi di Laurea, Universit\u00e0 di Roma, (1983)."},{"key":"32_CR6","unstructured":"Beth E. W., The Foundation of Mathematics, North Holland, (1959) (2nd ed. 1965)."},{"key":"32_CR7","first-page":"14","volume":"324","author":"C. B\u00f6hm","year":"1985","unstructured":"B\u00f6hm C., Functional Programming and Combinatory Algebras, MFCS 88, LNCS 324 (1985), 14\u201326.","journal-title":"LNCS"},{"key":"32_CR8","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0304-3975(85)90135-5","volume":"39","author":"C. B\u00f6hm","year":"1985","unstructured":"B\u00f6hm C., Berarducci A., Automatic Synthesis of Typed \u03bb-programs on Term Algebras, Theor. Comp. Sci. 39 (1985), 135\u2013154.","journal-title":"Theor. Comp. Sci."},{"key":"32_CR9","unstructured":"Boudol G., A Lambda-Calculus for Parallel Functions, Rapport de Recherche INRIA 1231, (1990)."},{"key":"32_CR10","unstructured":"Boudol G., A Lambda-Calculus for (Strict) Parallel Functions, Internal Report, INRIA Sophia-Antipolis, (1991)."},{"key":"32_CR11","first-page":"241","volume":"82","author":"M. Coppo","year":"1984","unstructured":"Coppo M., Dezani-Ciancaglini M., Honsell F., Longo G., Extended Type Structures and Filter Lambda Models, Logic Colloquium 82, North-Holland, (1984), 241\u2013262.","journal-title":"Logic Colloquium"},{"key":"32_CR12","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1002\/malq.19810270205","volume":"27","author":"M. Coppo","year":"1981","unstructured":"Coppo M., Dezani-Ciancaglini M., Venneri B., Functional Characters of Solvable Terms, Zeit. Math. Logik 27 (1981), 45\u201358.","journal-title":"Zeit. Math. Logik"},{"key":"32_CR13","unstructured":"Curry H., Feys R., Combinatory Logic, North-Holland, (1958)."},{"key":"32_CR14","unstructured":"Giannini P., Some Negative Results on Berarducci Numerals, Internal Report, Universita' di Torino, (1988)."},{"key":"32_CR15","first-page":"212","volume":"137","author":"R. Hindley","year":"1982","unstructured":"Hindley R., The Simple Semantic for Coppo-Dezani-Sall\u00e9 Types, ISP 82, LNCS 137 (1982), 212\u2013226.","journal-title":"LNCS"},{"key":"32_CR16","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(83)90136-6","volume":"22","author":"R. Hindley","year":"1983","unstructured":"Hindley R., The Completeness Theorem for Typing Lambda Terms, Theor. Comp. Sci. 22 (1983), 1\u201317.","journal-title":"Theor. Comp. Sci."},{"key":"32_CR17","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1016\/0304-3975(83)90074-9","volume":"28","author":"R. Hindley","year":"1984","unstructured":"Hindley R. Coppo-Dezani Types do not Correspond to Propositional Logic, Theor.Comp.Sci. 28 (1984), 235\u2013236.","journal-title":"Theor.Comp.Sci."},{"key":"32_CR18","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2964568","volume":"24","author":"S. Kripke","year":"1959","unstructured":"Kripke S., A Completeness Theorem in Modal Logic, Journal of Symbolic Logic 24 (1959), 1\u201314.","journal-title":"Journal of Symbolic Logic"},{"key":"32_CR19","doi-asserted-by":"crossref","unstructured":"Leivant D., Discrete Polymorphism, Proc. VI ACM Conference on LISP and Functional Programming, (1990), 288\u2013297.","DOI":"10.1145\/91556.91675"},{"key":"32_CR20","unstructured":"de'Liguoro U., Non-Deterministic Lambda-Calculus: Models and Types, Thesis Proposal, Universit\u00e0 di Roma, (1991)."},{"key":"32_CR21","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 71 (1986), 95\u2013130.","journal-title":"Information and Control"},{"key":"32_CR22","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/S0019-9958(82)80087-9","volume":"52","author":"A. Meyer","year":"1982","unstructured":"Meyer A., What is a Model of the Lambda Calculus?, Information and Control 52 (1982), 87\u2013122.","journal-title":"Information and Control"},{"key":"32_CR23","doi-asserted-by":"crossref","unstructured":"Meyer A., Mitchell J.C., Moggi E., Statman R., Empty Types in Polymorphic Lambda Calculus, Proc. 14th ACM Symposium on Principles of Programming Languages, (1985), 253\u2013262.","DOI":"10.1145\/41625.41648"},{"key":"32_CR24","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1016\/0168-0072(91)90067-V","volume":"51","author":"J. Mitchell","year":"1991","unstructured":"Mitchell J., Moggi E., Kripke-style Models for Typed Lambda Calculus, Annals of Pure and Applied Logics 51 (1991), 99\u2013124.","journal-title":"Annals of Pure and Applied Logics"},{"key":"32_CR25","unstructured":"Pierce B., Preliminary Investigation of a Calculus with Intersection and Union Types, Internal Report, Carnegie Mellon University, (1990)."},{"key":"32_CR26","unstructured":"Pierce B., Programming with Intersection Types, Union Types and Polymorphism, Technical Report, CMU-CS-91-106, Carnegie Mellon University, (1991)."},{"key":"32_CR27","volume-title":"Natural Deduction","author":"D. Prawitz","year":"1965","unstructured":"Prawitz D., Natural Deduction, Almqvist & Wiksell, Stockolm, (1965)."},{"key":"32_CR28","unstructured":"Reynolds J.C., Preliminary Design of the Programming Language FORSYTHE, Report CMU-CS-88-159, Carnegie Mellon University, (1988)."},{"key":"32_CR29","first-page":"704","volume":"372","author":"J.C. Reynolds","year":"1989","unstructured":"Reynolds J.C., Syntactic Control of Interference Part 2, ICALP 89, LNCS 372 (1989), 704\u2013722.","journal-title":"LNCS"},{"key":"32_CR30","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1016\/S0019-9958(82)80022-3","volume":"54","author":"S. Ronchi della Rocca","year":"1982","unstructured":"Ronchi della Rocca S., Characterization Theorems for a Filter Lambda Model, Information and Control 54 (1982), 201\u2013216.","journal-title":"Information and Control"},{"key":"32_CR31","first-page":"488","volume":"5","author":"C. Wadsworth","year":"1976","unstructured":"Wadsworth C., The Relation between Computational and Denotational Properties for D\u221e-models of the Lambda Calculus, S.I.A.M. J. on Computing 5 (1976), 488\u2013521.","journal-title":"S.I.A.M. J. on Computing"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computer Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-54415-1_69.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T21:18:51Z","timestamp":1742591931000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-54415-1_69"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540544159","9783540476177"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/3-540-54415-1_69","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}