Denotational and Operational Preciseness of Subtyping : Invited talk

Abstract

The notion of subtyping has gained an important role 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 aspects: 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 for iso-recursive types 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 a technique for formalising and proving operational preciseness of the subtyping relation in concurrent lambda calculus with intersection and union types. An overview of preciseness of subtyping in the setting of session and multiparty session type will be given. We then discuss a universal (language independent) framework to reason about preciseness of subtyping. (The talk is based on the results obtained jointly with Mariangiola Dezani-Ciancaglini, Svetlana Jaksic, Jovanka Pantovic, Alceste Scalas and Nobuko Yoshida.)