|
Published Articles >> Table of Contents >> Abstract
17th Annual IEEE Symposium on Logic in Computer Science (LICS'02)
p. 137
Semantic Subtyping
Alain Frisch, École Normale Supérieure
Giuseppe Castagna, École Normale Supérieure
Veronique Benzaken, Université Paris-Sud
Full Article Text:
  
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2002.1029823
Send link to a friend
| 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.
|
 Additional Information
|
Citation:
Alain Frisch, Giuseppe Castagna, Veronique Benzaken,
"Semantic Subtyping,"
lics,
p. 137,
17th Annual IEEE Symposium on Logic in Computer Science (LICS'02),
2002
|
|
