Abstract: Combining intersection types with higher-order subtyping yields a statically typed model of object-oriented programming with multiple inheritance. Objects, message passing, subtyping and inheritance appear as programming idioms in a certain typed lambda-calculus, a technique that facilitates experimentation and clarifies the distinction between essential aspects of the object-oriented style -- encapsulation and subtype polymorphism, which are directly reflected in features of the low-level type system -- and useful programming idioms such as inheritance.
The target calculus, a natural generalization of system F omega with intersection types, is of independent interest. We define it in full and give a proof of type soundness using a simple semantic model based on partial equivalence relations.
A revised version of this report was published under the title ``Higher Order Intersection Types and Multiple Inheritance'' in Mathematical Structures in Computer Science, 1996, volume 6, pp 469-501.Previous | Index | Next