Intersection types

Type systems, especially when used in programming languages, often benefit from having a notion of intersection amongst their primitive operators.

Thus, we can postulate a binary operator \land on types, along with an introduction rule

\frac{
  \Gamma \vdash M : A
  \quad
  \Gamma \vdash M : B
}{
	\Gamma \vdash M : A \land B
}

That is: if M has both type A and B, then it can be typed by their intersection.

Conversely, we can eliminate the intersection by 'forgetting' it:

\frac{
  \Gamma \vdash M : A \land B
}{
  \Gamma \vdash M : A
}
\quad
\frac{
  \Gamma \vdash M : A \land B
}{
  \Gamma \vdash M : B
}

Such type systems have many uses:

They can be used to exactly characterise the strong normalizing terms of the untyped \lambda-calculus.
They can be used in type systems for the \pi-calculus.
...

References

A recent survey of intersection types was presented as an invited talk at LICS 2020:

Bono, Viviana, and Mariangiola Dezani-Ciancaglini. 2020. ‘A Tale of Intersection Types’. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, 7–20. Saarbrücken Germany: ACM. https://doi.org/10.1145/3373718.3394733.

@inproceedings{bono_2020,
	address = {Saarbrücken Germany},
	title = {A tale of intersection types},
	doi = {10.1145/3373718.3394733},
	booktitle = {Proceedings of the 35th {Annual} {ACM}/{IEEE} {Symposium} on {Logic} in {Computer} {Science}},
	publisher = {ACM},
	author = {Bono, Viviana and Dezani-Ciancaglini, Mariangiola},
	month = jul,
	year = {2020},
	pages = {7--20}
}