TY  - JOUR
T1  - Coinductive Subtyping for Recursive and Union Types
AU  - Im, Hyeonseung 
JO  - Journal of KIISE, JOK
PY  - 2016
DA  - 2016/1/14
DO  - 
KW  - induction
KW  - coinduction
KW  - least/greatest fixed point
KW  - subtyping
KW  - recursive types
KW  - union types
AB  - 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.