Higher-order intersection types and multiple inheritance

Abstract

We study a natural generalization of System F ω with intersection types, establishing basic structural properties and constructing a semantic model based on partial equivalence relations to prove the soundness of typing. As an application of this calculus, we define a simple typed model of object-oriented programming with multiple inheritance.