|Title:||Precise subtyping for synchronous multiparty sessions||Journal:||Journal of Logical and Algebraic Methods in Programming||Volume:||104||First page:||127||Last page:||173||Issue Date:||1-Apr-2019||Rank:||M21||ISSN:||2352-2208||DOI:||10.1016/j.jlamp.2018.12.002||Abstract:||
This paper proves the soundness and completeness, together referred to as preciseness, of the subtyping relation for a synchronous multiparty session calculus. We address preciseness from operational and denotational viewpoints. The operational preciseness has been recently developed with respect to type safety, i.e., the safe replacement of a process of a smaller type in a context where a process of a bigger type is expected. The denotational preciseness is based on the denotation of a type: a mathematical object describing the meaning of the type, in accordance with the denotations of other expressions from the language. The main technical contribution of this paper is a novel proof strategy for the operational completeness of subtyping. We develop the notion of characteristic global type of a session type T, which describes a deadlock-free circular communication protocol involving all participants appearing in T. We prove operational completeness by showing that, if we place a process not conforming to a subtype of T in a context that matches the characteristic global type of T, then we obtain a deadlock. The denotational preciseness is proved as a corollary of the operational preciseness.
|Keywords:||Concurrency | Multiparty session types | Process calculi | Subtyping||Publisher:||Elsevier||Project:||EPSRC EP/K011715/1, EP/K034413/1, EP/L00058X/1, EP/N027833/1 and EP/N028201/1
Representations of logical structures and formal languages and their application in computing
Development of new information and communication technologies, based on advanced mathematical methods, with applications in medicine, telecommunications, power systems, protection of national heritage and education
COST Action EUTYPES (CA15123), BETTY (IC1201) and ARVI (IC1402)
Continuous Observation of Embedded Multicore Systems
Show full item record
checked on Mar 27, 2023
checked on Mar 28, 2023
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.