Precise subtyping for synchronous multiparty sessions

Silvia Ghilezan, Svetlana Jakšić, Jovanka Pantović, Alceste Scalas, Nobuko Yoshida

Research output: Contribution to journalArticlepeer-review

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.

Original languageEnglish
Pages (from-to)127-173
Number of pages47
JournalJournal of Logical and Algebraic Methods in Programming
Volume104
Early online date29 Dec 2018
DOIs
Publication statusPublished - Apr 2019

Keywords

  • Concurrency
  • Multiparty session types
  • Process calculi
  • Subtyping

Fingerprint Dive into the research topics of 'Precise subtyping for synchronous multiparty sessions'. Together they form a unique fingerprint.

Cite this