An Algebraic Framework for Separate Type-Checking

. We address the problem of defining an algebraic framework for modularization supporting separate type-checking. In order to do that we introduce the notions of abstract type system and logic of constraints and we present a canonical construction of a model part, on top of a logic of constraints. This canonical construction works under reasonable assumptions on the underlying type system (e.g., soundness of the system). We show that the framework is suitable for defining the static and dynamic semantics of module languages, by giving a concrete example of construction on top of the type system of a simple typed module language. As a result, the subtyping relation between module interfaces is captured in a natural way by the notion of signature morphism. Introduction Modularization has been considered since the early 70s an essential principle for managing the complex task of software development [30]. Nowadays there exist many programming languages supporting the notion of module and..