Semantic subtyping_ Dealing set-theoretically with function, union, intersection, and negation types

authors: Alain Frisch, Giuseppe Castagna, Véronique Benzaken
year: 2008
url: https://www.irif.fr/ gc/papers/semanticₛubtyping.pdf
publisher: Association for Computing Machinery (ACM)
abstract: Subtyping relations are usually defined either syntactically by a formal system or semantically by an interpretation of types into an untyped denotational model. This work shows how to define a subtyping relation semantically in the presence of Boolean connectives, functional types and dynamic dispatch on types, without the complexity of denotational models, and how to derive a complete subtyping algorithm.