Authors: Ghilezan, Silvia 
Jakšić, Svetlana
Pantović, Jovanka
Scalas, Alceste
Yoshida, Nobuko
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
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 Jun 22, 2024

Page view(s)

checked on May 9, 2024

Google ScholarTM




Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.