TY - JOUR
T1 - Precise subtyping for synchronous multiparty sessions
AU - Ghilezan, Silvia
AU - Jakšić, Svetlana
AU - Pantović, Jovanka
AU - Scalas, Alceste
AU - Yoshida, Nobuko
PY - 2019/4
Y1 - 2019/4
N2 - 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.
AB - 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.
KW - Concurrency
KW - Multiparty session types
KW - Process calculi
KW - Subtyping
UR - http://www.scopus.com/inward/record.url?scp=85069436653&partnerID=8YFLogxK
UR - https://www.sciencedirect.com/science/article/pii/S2352220817302237?via%3Dihub
U2 - 10.1016/j.jlamp.2018.12.002
DO - 10.1016/j.jlamp.2018.12.002
M3 - Article
AN - SCOPUS:85069436653
SN - 2352-2216
VL - 104
SP - 127
EP - 173
JO - Journal of Logical and Algebraic Methods in Programming
JF - Journal of Logical and Algebraic Methods in Programming
ER -