|Title:||Precise subtyping for synchronous multiparty sessions||Journal:||Electronic Proceedings in Theoretical Computer Science, EPTCS||Volume:||203||First page:||29||Last page:||43||Conference:||8th International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software, PLACES 2015; London; United Kingdom; 18 April 2015||Issue Date:||10-Feb-2016||ISSN:||2075-2180||DOI:||10.4204/EPTCS.203.3||Abstract:||
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.
|Publisher:||Open Publishing Association||Project:||COST IC1201 BETTY and DART
EPSRC EP/K011715/1, EP/K034413/1, and EP/L00058X/1
EU Project FP7-612985 UpScale
Show full item record
checked on Nov 27, 2022
checked on Nov 28, 2022
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.