Intersection type discipline

In mathematical logic, the intersection type discipline is a branch of type theory encompassing type systems that use the intersection type constructor formula_1 to assign multiple types to a single term.
In particular, if a term formula_2 can be assigned "both' the type formula_3 and the type formula_4, then formula_2 can be assigned the intersection type formula_6 (and vice versa).
Therefore, the intersection type constructor can be used to express finite heterogeneous ad hoc polymorphism (as opposed to parametric polymorphism).
For example, the λ-term formula_7 can be assigned the type formula_8 in most intersection type systems, assuming for the term variable formula_9 both the function type formula_10 and the corresponding argument type formula_11.
Prominent intersection type systems include the Coppo–Dezani type assignment system, the Barendregt-Coppo–Dezani type assignment system, and the essential intersection type assignment system.
Most strikingly, intersection type systems are closely related to (and often exactly characterize) normalization properties of λ-terms under β-reduction.
In programming languages, such as TypeScript and Scala, intersection types are used to express ad hoc polymorphism.
History.
The intersection type discipline was pioneered by Mario Coppo, Mariangiola Dezani-Ciancaglini, Patrick Sallé, and Garrel Pottinger.
The underlying motivation was to study semantic properties (such as normalization) of the λ-calculus by means of type theory.
While the initial work by Coppo and Dezani established a type theoretic characterization of strong normalization for the λI-calculus, Pottinger extended this characterization to the λK-calculus.
In addition, Sallé contributed the notion of the universal type formula_12 that can be assigned to any λ-term, thereby corresponding to the empty intersection.
Using the universal type formula_12 allowed for a fine-grained analysis of head normalization, normalization, and strong normalization.
In collaboration with Henk Barendregt, a filter λ-model for an intersection type system was given, tying intersection types ever more closely to λ-calculus semantics.
Due to the correspondence with normalization, typability in prominent intersection type systems (excluding the universal type) is undecidable.
Complementarily, undecidability of the dual problem of type inhabitation in prominent intersection type systems was proven by Paweł Urzyczyn.
Later, this result was refined showing exponential space completeness of rank 2 intersection type inhabitation and undecidability of rank 3 intersection type inhabitation.
Remarkably, "principal" type inhabitation is decidable in polynomial time.
Coppo–Dezani type assignment system.
The Coppo–Dezani type assignment system formula_14 extends the simply typed λ-calculus by allowing multiple types to be assumed for a term variable.
Term language.
The term language of formula_15 is given by λ-terms (or, lambda expressions):
Type language.
The type language of formula_15 is inductively defined by the following grammar:
The intersection type constructor (formula_19) is taken modulo associativity, commutativity and idempotence.
Type rules.
The type rules formula_20, formula_21, formula_22, and formula_23 of formula_15 are:
Properties.
Typability and normalization are closely related in formula_14 by the following properties:
If the type language is extended to contain the empty intersection, i.e. formula_40, 
then formula_14 is closed under β-equality and is sound and complete for inference semantics.
Barendregt–Coppo–Dezani type assignment system.
The Barendregt–Coppo–Dezani type assignment system formula_42 extends the Coppo–Dezani type assignment system in the following three aspects:
Term language.
The term language of formula_42 is given by λ-terms (or, lambda expressions):
Type language.
The type language of formula_42 is inductively defined by the following grammar:
Intersection type subtyping.
Intersection type subtyping formula_49 is defined as the smallest preorder (reflexive and transitive relation) over intersection types satisfying the following properties:
Intersection type subtyping is decidable in quadratic time.
Type rules.
The type rules formula_20, formula_21, formula_22, formula_49, formula_60, and formula_61 of formula_42 are: