Semantic subtyping

Alain Frisch Giuseppe Castagna Véronique Benzaken

To appear at Symposium on Logic in Computer Science (LICS'2002), Copenhagen, Denmark, July 22nd - 25th, 2002


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.

Server START Conference Manager
Update Time 15 Mar 2002 at 15:30:30
Start Conference Manager
Conference Systems