A Coalgebraic Semantics of Subtyping

Subtyping is a central notion in object-oriented programming. In this paper we investigate how the coalgebraic semantics of objects accounts for subtyping. We show that different characterisations of so-called behavioural subtyping found in the literature can conveniently be expressed in coalgebraic terms. We define subtyping between coalgebras and subtyping between coalgebraic specifications, and show that the latter is sound and complete w.r.t. the former. We also illustrate the subtle difference between the notions of subtyping and refinement.