Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, Svetlana Jakšić, Jovanka Pantović and Nobuko Yoshida
The notion of subtyping has gained an important role both in theoretical 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 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. Operational preciseness has been first introduced for a call-by-value lambda-calculus with sum, product and recursive types. Both operational and denotational preciseness have been studied for a lambda-calculus with choice and parallel constructors and for binary sessions.
Subtyping for session calculi can be defined to assure safety of substitutability of either channels or processes. We claim that substitutability of processes better fits the notion of preciseness.
This paper shows the operational and denotational preciseness of subtyping for a synchronous multiparty session calculus. For the denotational preciseness we interpret a type as the set of processes having that type. For the operational preciseness we take the view that well-typed sessions never get stuck.