π-calculus, Session Types research at Imperial College
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 , which describes a deadlock-free circular communication protocol involving all participants appearing in . We prove operational completeness by showing that, if we place a process not conforming to a subtype of in a context that matches the characteristic global type of , then we obtain a deadlock. The denotational preciseness is proved as a corollary of the operational preciseness.
@article{GJPSY2019,
author = {Silvia Ghilezan and Svetlana Jaksic and Jovanka Pantovic and Alceste Scalas and Nobuko Yoshida},
title = {{Precise subtyping for synchronous multiparty sessions}},
journal = {JLAMP},
volume = {104},
pages = {127--173},
publisher = {Elsevier},
year = 2019
}
@article{GJPSY2019,
author = {Silvia Ghilezan and Svetlana Jaksic and Jovanka Pantovic and Alceste Scalas and Nobuko Yoshida},
title = {{Precise subtyping for synchronous multiparty sessions}},
journal = {Journal of Logical and Algebraic Methods in Programming},
volume = {104},
pages = {127--173},
publisher = {Elsevier},
doi = "10.1016/j.jlamp.2018.12.002",
year = 2019
}