Sound and complete subtyping between coinductive types for object-oriented languages

Structural subtyping is an important notion for effective static type analysis; it can be defined either axiomatically by a collection of subtyping rules, or by means of set inclusion between type interpretations, following the semantic subtyping approach, which is more intuitive, and allows simpler proofs of the expected properties of the subtyping relation. In object-oriented programming, recursive types typically correspond to inductively defined data structures, and subtyping is defined axiomatically; however, in object-oriented languages objects can also be cyclic, but inductive types cannot represent them as precisely as happens for coinductive types. We study semantic subtyping between coinductive types with records and unions, which are particularly interesting for object-oriented programming, show cases where it allows more precise type analysis, and develop a sound and complete effective algorithm for deciding it. To our knowledge, this is the first proposal for a sound and complete algorithm for semantic subtyping between coinductive types.