Logic in Computer Science (LICS 2002)

Paper: Semantic subtyping (at LICS 2002)

Authors: Alain Frisch Giuseppe Castagna Véronique Benzaken

Abstract

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}
  }