Logic of subtyping

We introduce new modal logical calculi that describe subtyping properties of Cartesian product and disjoint union type constructors as well as mutually recursive types defined using those type constructors. Basic logic of subtyping S extends classical propositional logic by two new binary modalities x and +. An interpretation of S is a function that maps standard connectives into set-theoretical operations (intersection, union, and complement) and modalities into Cartesian product and disjoint union type constructors. This allows S to capture many subtyping properties of the above type constructors. We also consider logics S(rho) and S(rho)(omega) that incorporate into S mutually recursive types over arbitrary and well-founded universes correspondingly. The main results are completeness of the above three logics with respect to appropriate type universes. In addition, we prove Cut elimination theorem for S and establish decidability of S and S(rho)(omega). (C) 2006 Elsevier B.V. All rights reserved.