Observational Equivalence for Multiparty Sessions

Issue title: Types, terms and reductions: A special issue dedicated to Paweł Urzyczyn for his 65th birthday

Subtitle: Dedicated to Pawel Urzyczyn on the occasion of his 65th birthday

Guest editors: Thorsten Altenkirch and Aleksy Schubert

Article type: Research Article

Authors: Severi, Paula^{a; *} | Dezani-Ciancaglini, Mariangiola^{b; †}

Affiliations: [a] Department of Computer Science, University of Leicester, Leicester, UK. ps396@leicester.ac.uk | [b] Dipartimento di Informatica, Università di Torino, Torino, Italy. dezani@di.unito.it

Correspondence: [*] Address for correspondence: Department of Computer Science, University of Leicester, Leicester UK

Note: [†] Partially supported by Ateneo/Compagnia di San Paolo 2016/2018 project “MnemoComputing - Components for Processing In Memory”.

Abstract: Multiparty sessions are concurrent processes, which allow several participants to communicate by sending and receiving messages. We consider an observational preorder of processes, that captures the idea that the whole session remains correct after replacing one process by another one. This preorder is characterised by means of a structural preorder between processes, which mimics the subtyping relation between session types from the literature.

DOI: 10.3233/FI-2019-1863

Journal: Fundamenta Informaticae, vol. 170, no. 1-3, pp. 267-305, 2019