Subtyping in FomegaMeet is Decidable

Adriana B. Compagnoni

Abstract: Combining intersection types with higher-order subtyping yields a typed model of object-oriented programming with multiple inheritance [Compagnoni and Pierce, 1993]. 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 [Castagna and Pierce, 1993], 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.

LFCS report ECS-LFCS-94-281, January 1994.

A short version of this report was published as Decidability of higher-order subtyping with intersection types. In Proceedings of the Annual Conference of the European Association for Computer Science Logic, CSL'94, Kazimierz, Poland, number 933 in Lecture Notes in Computer Science. Springer-Verlag, June 1995. This report has been superseded by ECS-LFCS-97-363 and ECS-LFCS-97-365.

Previous | Index | Next