Multiple Inheritance via Intersection Types

Adriana B Compagnoni and Benjamin C Pierce

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.

LFCS report ECS-LFCS-93-275, August 1993.

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