Intersection types and overloading - Birov, Dimitar (Annual of Sofia University St. Kliment Ohridski. Faculty of Mathematics and Informatics, 1996)
Type systems which are employed in programming languages are a practical result obtained by the formal type theory. Type systems based on intersection types are studied extensively during the past years both as tools for analysis of pure $λ$-calculus and as a foundation for practical programming languages. One of the intriguing properties of intersection types is their ability to express an unbounded amount of information about a program. The notion of overloading sounds very actually in programming languages. We point an addition function (+) for both adding integer and real numbers as a typical example for it. We generalize overloading and describe type system including higher order function overloading in this paper.