Precise subtyping for synchronous multiparty sessions

Mariangiola Dezani-Ciancaglini
(Università di Torino, Italy)
Silvia Ghilezan
(Univerzitet u Novom Sadu, Serbia)
Svetlana Jakšić
(Univerzitet u Novom Sadu, Serbia)
Jovanka Pantović
(Univerzitet u Novom Sadu, Serbia)
Nobuko Yoshida
(Imperial College London, UK)

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: operational and denotational. The former 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. The latter 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 result of this paper is the operational and denotational preciseness of the subtyping for a synchronous multiparty session calculus. The novelty of this paper is the introduction of characteristic global types to prove the operational completeness.

In Simon Gay and Jade Alglave: Proceedings Eighth International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software (PLACES 2015), London, UK, 18th April 2015, Electronic Proceedings in Theoretical Computer Science 203, pp. 29–43.
Published: 10th February 2016.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: