Coinductive Subtyping for Recursive and Union Types

Hyeonseung Im

http://doi.org/

Induction and coinduction are well-established proof principles, which are widely used in mathematics and computer science. In particular, induction is taught in most undergraduate programs and well understood in the field of computer science. In contrast, coinduction is not as widespread or well understood as induction. In this paper, we introduce coinduction by defining a subtype system for recursive and union types and proving the transitivity property of the system. This paper will help to promote familiarity with coinduction and provides a basis for a subtype system for recursive types with other advanced type constructors and connectives.