One approach to give semantics to languages with subtypes is by translation to target languages without subtyping: subtypings A 6 B are interpreted via conversion functions A B. ...
We show how to implement a calculus with higher-order subtyping and subkinding by replacing uses of implicit subsumption with explicit coercions. To ensure this can be done, a pol...