A type system for checking specialization of packages in object-oriented programming

Large object-oriented software systems are usually structured using modules or packages to enable large-scale development using clean interfaces that promote encapsulation and information hiding. However, in most OO languages, package interfaces (or signatures) are only implicitly defined. In this paper, we propose explicit package signatures that allow for modularly type-checking packages. We show how the signatures can be derived from packages and define a checkable specialization relation for package signatures. As main contribution, we show that if the package signatures of a new component version Cnew specialize the signatures of the old version Cold, then Cnew type-checks in all contexts in which Cold type-checks. That is, we extend checking of interface types to the level of packages.