Sound and complete subtyping on intersection and union types

Abstract

The notion of subtyping has gained an important role both in the oretical and applicative domains: in lambda and concurrent calculi as well as in programming languages. The soundness and the completeness, together referred to as the preciseness of subtyping, can be considered from two different points of view: denotational and operational. The former preciseness is based on the denotation of a type which is a mathematical object that describes the meaning of the type in accordance with the denotations of other expressions from the language. The latter preciseness has been recently developed in [3] with respect to type safety, i.e. the safe replacement of a term of a smaller type when a term of a bigger type is expected. We present the technique for formalising and proving operational preciseness of the subtyping relation in the setting of a concurrent lambda calculus with intersection and union types given in [1]. An overview of preciseness of subtyping in other frameworks will be given ([2]). This is a joint work with Mariangiola Dezani-Ciancaglini.