Semantic Types for Classes and Mixins

ABSTRACT. We consider a formalization of mixins composition and class linearization yielding a class in mixin-based inheritance. We provide an interpretation of the mixin calculus into a lambda-calculus extended with records and a record merge operator. After extending the BCD intersection type assignment to such calculus showing that types are preserved by subject expansion and reduction, we naturally interpret mixin terms as the sets of the types that can be deduced of their translations. It turns out that the class obtained from a composition of mixins and the composition itself have the same logical meaning.