ITRS

Intersection Types and Related Systems

• HOME
• WORKSHOPS
• CONTACTS
• LINKS

Intersection types were introduced near the end of the 1970s to overcome the limitations of Curry's type assignment system and to provide a characterization of the strongly normalizing terms of the λ-calculus. The key idea is to introduce an intersection type constructor ⋀ such that a term of type σ ⋀ τ can be used with both type σ and τ within the same context. This provides a finite polymorphism where various, even unrelated, types of the term are listed explicitly, differently than the more widely used universally quantified types where the polymorphic type is the common schema which stands for its various type instances. As a consequence, more terms (all and only the normalizing terms) can be typed than with universal polymorphism.

Intersection types have been one of the first examples of behavioural type theory: they provide an abstract specification of computational properties, by expressing a finer and more precise input/output relation than standard, commonly used, type systems can do. In fact also other relevant classes of terms, like weakly normalising terms and terms having a head-normal form, can be characterised via intersection types by adding a universal type ω; further by adding subtyping it is possible to describe models in the category of algebraic lattices, and systems where term denotations coincide with the sets of their types.

Although intersection types were initially intended for use in analysing and/or synthesizing λ-models as well as in analysing normalization properties, over the last twenty years the scope of the research on intersection types and related systems has broadened in many directions. Restricted (and more manageable) forms have been investigated, such as refinement types. Type systems based on intersection type theory have been extensively studied for practical purposes, such as program analysis and synthesis. The dual notion of union types turned out to be quite useful for programming languages. Finally, the behavioural approach to types, which can give a static specification of computational properties, has become central in the most recent research on type theory.