Paper: Semantic subtyping (at LICS 2002)
Authors: Alain Frisch Giuseppe Castagna Véronique BenzakenAbstract
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.
BibTeX
@InProceedings{FrischCastagnaBenza-Semanticsubtyping, author = {Alain Frisch and Giuseppe Castagna and Véronique Benzaken}, title = {Semantic subtyping}, booktitle = {Proceedings of the Seventeenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2002}, year = 2002, editor = {Gordon Plotkin}, month = {July}, location = {Copenhagen, Denmark}, publisher = {IEEE Computer Society Press} }