Usually subtyping relations are defined either syntactically by
a formal system or semantically by an interpretation of types
in an untyped denotational model. In this work we show how to define a
subtyping relation semantically, for a language whose _operational_
semantics is _driven by types_; we consider a rich type algebra,
with product, arrow, recursive, intersection, union and complement types.
Our approach is to ``bootstrap'' the subtyping relation through
a notion of set-theoretic model _of the type algebra_.
The advantages of the semantic approach are manifold. Foremost we get
``for free'' many properties (e.g., the transitivity of subtyping)
that, with axiomatized subtyping, would require tedious and error
prone proofs. Equally important is
that the semantic approach allows one to _derive_ complete algorithms
for the subtyping relation or the propagation of types through
patterns. As the subtyping relation has a natural (inasmuch as
semantic) interpretation, the type system can give informative error
messages when static type-checking fails. Last but not least the
approach has an immediate impact in the definition _and the
implementation_ of languages manipulating XML documents, as this was
our original motivation.
