It is well-known that logical connectives conjunction, disjunction, and negation could be interpreted as set operations intersection, union, and complement. Logical tautologies, under this interpretation, capture properties of set operations.

In this talk we will present an extension of the propositional logic by new connectives corresponding, in the sense of above interpretation, to Cartesian product, disjoint union, and type recursion. Most of commonly used data structures could be defined in terms of the these type operations. Thus, logical "tautologies" that include new connectives capture general properties of such data structures. As it turns out, this approach is especially fruitful for describing subtyping properties of the data structures.

We will also provide a complete axiomatization of this extension of the propositional logic and analyze its decidability.