{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,20]],"date-time":"2026-05-20T22:23:30Z","timestamp":1779315810005,"version":"3.51.4"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[1992,9,1]],"date-time":"1992-09-01T00:00:00Z","timestamp":715305600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[1992,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            This paper is an informal introduction to the theory of types which use a connective \u201c\u2227\u201d for the intersection of two types and a constant \u201c\n            <jats:italic>\u03c9<\/jats:italic>\n            \u201d for a universal type, besides the usual connective \u201c\u2192\u201d for function-types. This theory was first devised in about 1977 by Coppo, Dezani and Sall\u00e9 in the context of\n            <jats:italic>\u03bb<\/jats:italic>\n            -calculus and its main development has been by Coppo and Dezani and their collaborators in Turin. With suitable axioms and rules to assign types to\n            <jats:italic>\u03bb<\/jats:italic>\n            -calculus terms, they obtained a system in which (i) the set of types given to a term does not change under\n            <jats:italic>\u03bb<\/jats:italic>\n            -conversion, (ii) some interesting sets of terms, for example the solvable terms and the terms with normal form, can be characterised exactly by the types of their members, and (iii) the type-apparatus is not so complex as polymorphic systems with quantifier-containing types and therefore probably not so expensive to implement mechanically as these systems.\n          <\/jats:p>\n          <jats:p>There are in fact several variant systems with different detailed properties. This paper defines and motivates the simplest one from which the others are derived, and describes its most basic properties. No proofs are given but the motivation is shown by examples. A comprehensive bibliography is included.<\/jats:p>","DOI":"10.1007\/bf01211394","type":"journal-article","created":{"date-parts":[[2005,2,25]],"date-time":"2005-02-25T22:14:33Z","timestamp":1109369673000},"page":"470-486","source":"Crossref","is-referenced-by-count":14,"title":["Types with intersection: An introduction"],"prefix":"10.1145","volume":"4","author":[{"given":"J. Roger","family":"Hindley","sequence":"first","affiliation":[{"name":"Mathematics Department, University College of Swansea, SA2 8PP, Swansea, Wales UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Alessi F. and Barbanera F.: Strong Conjunction and intersection Types. In: Mathematical Foundations of Computer Science 1991 A. Tarlecki (ed.) Lecture Notes in Computer Science 520 Springer-Verlag pp. 64\u201373 (1991).","DOI":"10.1007\/3-540-54345-7_49"},{"key":"e_1_2_1_2_2_2","unstructured":"van Bakel S: Complete Restrictions of the Intersection Type Discipline Theoretical Computer Science (to appear)."},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Barbanera F. and Dezani M.: Intersection and Union Types. In: Theoretical Aspects of Computer Software International Conference TACS '91 Sendai Japan September 1991 Proceedings T. Ito and A. R. Meyer (eds.) Lecture Notes in Computer Science 526 Springer-Verlag pp. 651\u2013674 (1991).","DOI":"10.1007\/3-540-54415-1_69"},{"key":"e_1_2_1_2_4_2","unstructured":"Barbanera F.: Combining Term Rewriting and Type Assignment Systems Proc. Third Italian Conf. on Theoretical Computer Science Mantova 1989 A. Bertoni et al. (eds) World Scientific Press pp. 71\u201384 (1989). (To appear in Foundations of Computer Science )."},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.2307\/2273659"},{"key":"e_1_2_1_2_6_2","unstructured":"Bosio E. and Ronchi della Rocca S.: Type Synthesis for Intersection Type Discipline. In: Proc. Third Italian Conference on Theoretical Computer Science Mantova 1989 A. Bertoni et al. (eds.) World Scientific Press pp. 109\u2013122 (1989)."},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Coppo M.: An Extended Polymorphic Type System for Applicative Languages. In: Mathematical Foundations of Computer Science 1980 Proceedings of the 9th Symposium Held in Rydzyna Poland P. Dembinski (ed.) Lecture Notes in Computer Science 88 Springer-Verlag pp. 194\u2013204 (1980).","DOI":"10.1007\/BFb0022505"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF02011875"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093883253"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Coppo M. Dezani M. Honsell F. and Longo G.: Extended Type Structures and Filter Lambda Models. In: Logic Colloquium '82 G. Lolli et al. (eds) North-Holland pp. 241\u2013262 (1983).","DOI":"10.1016\/S0049-237X(08)71819-6"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Coppo M. Dezani M. and Sall\u00e9 P.: Functional Characterization of Some Semantic Equalities Inside \u03bb -Calculus. In: Automata Languages and programming Sixth Colloquium Graz July 1979 H. A. Maurer (ed.) Lecture Notes in Computer Science 71 Springer-Verlag pp. 133\u2013146 (1979).","DOI":"10.1007\/3-540-09510-1_11"},{"key":"e_1_2_1_2_13_2","unstructured":"Coppo M. Dezani M. and Venneri B. Principal Type Schemes and \u03bb-Calculus Semantics. In: To H. B. Curry J. R. Hindley and J. P. Seldin (eds) Academic Press pp. 535\u2013560 (1980)."},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19810270205"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(87)90042-3"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1111\/j.1746-8361.1969.tb01183.x"},{"key":"e_1_2_1_2_17_2","unstructured":"Dezani M. and Hindley J. R.: Intersection Types for Combinatory Logic Theoretical Computer Science (to appear)."},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Dezani M. and Margaria I.: F-Semantics for Intersection Type Discipline. In: Semantics of Data Types International Symposium Sophia-Antipolis France June 1984 Proceedings G. Kahn D. MacQueen and G. Plotkin (eds.) Lecture Notes in Computer Science 173 Springer-Verlag 279\u2013300 (1984).","DOI":"10.1007\/3-540-13346-1_14"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/0304-3975(86)90043-5","article-title":"A Characterization of F-complete Type Assignments","volume":"45","author":"Dezani M.","year":"1986","journal-title":"Theoretical Computer Science"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Hayashi S.: Singleton union and intersection types for program extraction. In: Theoretical Aspects of Computer Software international Conference TACS '91 Sendai Japan September 1991 Proceedings T. Ito and A. R. Meyer (eds.) Lecture Notes in Computer Science 526 Springer-Verlag pp. 701\u2013730 (1991).","DOI":"10.1007\/3-540-54415-1_71"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Hindley J. R.: The Simple Semantics for Coppo-Dezani-Sall\u00e9 Types. In: International Symposium on programming 5th Colloquium Turin April 1982 M. Dezani and U. Montanari (eds.) Lecture Notes in Computer Science 137 Springer-Verlag 212\u2013226 (1982).","DOI":"10.1007\/3-540-11494-7_15"},{"key":"e_1_2_1_2_22_2","unstructured":"Hindley J. R. and Seldin J. P.: Introduction to Combinators and \u03bb-Calculus Cambridge University Press 1986."},{"key":"e_1_2_1_2_23_2","unstructured":"Honsell F. and Ronchi della Rocca S.: Reasoning About Interpretation in Qualitative Lambda Models. In: IFIP TC2 Working Conf. on Programming Concepts and Methods 1990 North-Holland pp. 492\u2013508 (1991)."},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Lopez-Escobar E. K. G.: Proof Functional Connectives. In: Lecture Notes in Mathematics. 1130 Springer-Verlag 208\u2013221 (1985).","DOI":"10.1007\/BFb0075313"},{"key":"e_1_2_1_2_25_2","first-page":"117","article-title":"On Intuitionistic Sentential Connectives","volume":"19","author":"Lopez-Escobar E. K. G.","year":"1985","journal-title":"Rev. Colombiana de Math."},{"key":"e_1_2_1_2_26_2","unstructured":"Margaria I. Zacchi M.: Principal Typing in a Polymorphic-intersection Type Discipline. MS Dipartimento di Informatica Corso Svizzera 185 Turin Italy (1991)."},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093635158"},{"key":"e_1_2_1_2_28_2","volume-title":"Technical Report CMU-CS-91-106","author":"Pierce B. C.","year":"1991"},{"key":"e_1_2_1_2_29_2","unstructured":"Pottinger G.: A Type Assignment for the Strongly Normalizable \u03bb-Terms. In: To H. B. Curry J. R. Hindley and J. P. Seldin (eds) Academic Press pp. 561\u2013577 (1980)."},{"key":"e_1_2_1_2_30_2","volume-title":"Report CMU-CS-88-159","author":"Reynolds J. C.","year":"1988"},{"key":"e_1_2_1_2_31_2","unstructured":"Reynolds J. C.: Syntactic Control of Interference Part 2. In: Automata Languages and Programming 16th International Colloquium Stresa Italy July 1989 Proceedings G. Ausiello M. Dezani and S. Ronchi della Rocca (eds.) Lecture Notes in Computer Science 372 Springer-Verlag pp. 704\u2013722 (1989)."},{"key":"e_1_2_1_2_32_2","unstructured":"Reynolds J. C.: The Coherence of Languages with Intersection Types. In: Theoretical Aspects of Computer Software International Conference TACS '91 Sendai Japan September 1991 Proceedings T. Ito and A. R. Meyer (eds.) Lecture Notes in Computer Science 526 Springer-Verlag pp. 675\u2013700 (1991)."},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1016\/S0019-9958(82)80022-3","article-title":"Characterization Theorems for a Filter Lambda Model","volume":"54","author":"Ronchi Della Rocca S.","year":"1982","journal-title":"Information and Control"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90069-5"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Sall\u00e9 P.: Une Extension de la Th\u00e9orie des Types. In: Automata Languages and Programming Fifth Colloquium Udine July 1978 G. Ausiello and C. B\u00f6hm (eds.) Lecture Notes in Computer Science 62 Springer-Verlag pp. 398\u2013410 (1978).","DOI":"10.1007\/3-540-08860-1_30"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01211394.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01211394\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01211394","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:23:13Z","timestamp":1641482593000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01211394"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992,9]]},"references-count":35,"journal-issue":{"issue":"5","published-print":{"date-parts":[[1992,9]]}},"alternative-id":["10.1007\/BF01211394"],"URL":"https:\/\/doi.org\/10.1007\/bf01211394","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1992,9]]}}}