Combining intersection types with higher-order subtyping yields a
typed model of object-oriented programming with multiple inheritance
[CompagnoniPierce93]. The target calculus, FomegaMeet, a natural
generalization of Girard's system Fomega with intersection types
and bounded polymorphism, is of independent interest. We prove that
subtyping in FomegaMeet is decidable, which yields as a corollary the
decidability of subtyping in FomegaSub, its intersection free
fragment, because FomegaMeet subtyping system is a conservative
extension of that of FomegaSub. Since in both cases subtyping is
closed under beta-meet-conversion or beta-conversion of types, which is
not the case for the calculus presented in [CastagnaPierce93],
solving the problem in the present setting is much more difficult.
Moreover, we establish basic structural properties of FomegaMeet and we
prove that the type assignment system is sound using a model based on
partial equivalence relations.