In a nutshell the intersection type systems form a class of type assignment systems for untyped lambda-calculus, extending Curry's basic functionality with a new type constructor, intersection. This simple move allows expressing naturally and in a finitary way many of the most important operational and denotational properties of terms.

Intersection types have been originally introduced as a language for describing and capturing properties of lambda-terms, which had escaped all previous typing disciplines. For instance, they were used in order to give the first type-theoretic characterization of strongly normalizable terms, and later in order to capture persistently normalizing terms and normalizing terms.

Very early on it was realized, that intersection types had also a very distinctive semantical flavour. Namely, they expressed at a syntactical level the fact that a term belonged to suitable compact open sets in a Scott domain.

Since then, intersection types have been used as a powerful tool both for the analysis and the synthesis of lambda-models. On the one hand, intersection type disciplines provide finitary inductive definitions of the interpretation of lambda-terms in models. On the other hand, they are suggestive for the shape the domain model has to have in order to exhibit certain properties.

Keywords: intersection types, lambda calculus, normalization properties, denotational semantics, lambda models