Intersection types and overloading

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 $\lambda$-calculus and as a foundation for practical programming languages. One of the intriguing properties of intersection types is their ability to express an unbounded finite 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.