Types with intersection: An introduction (Q1201298)

This is a very lucid introduction to type theory with intersection. The author first clarifies and stresses the distinction between typed systems and type assignment systems, that is, the difference of interpretations of a function from a certain type to another (Church interpretation and Curry interpretation). The Coppo-Dezani type-assignment system \(TA_ \lambda(\land,\omega)\), the simplest of such systems with intersection, is introduced, and its most basic properties, such as \(\beta\)-invariance and characterization of solvable terms, are presented. Many illuminative examples are provided. A comprehensive bibliography up to the end of 1991 is included. Strongly recommended to the newcomer to this field.