Denotational Semantics for Subtyping Between Recursive Types
Val Tannen, Carl A. Gunter, Andre Scedrov · ScholarlyCommons (University of Pennsylvania) · 1989
Inheritance in the form of subtyping is considered in the framework of a polymorphic type discipline with records, variants, and recursive types. We give a denotational semantics based on the paradigm that interprets subtyping as explicit coercion. The main technical result gives a coherent interpretation for a strong rule for deriving inheritances between recursive types.