DROPS

Document

Pearl/Brave New Idea

DOI: 10.4230/LIPIcs.ECOOP.2023.42

Synthetic Behavioural Typing: Sound, Regular Multiparty Sessions via Implicit Local Types (Pearl/Brave New Idea)

Authors: Sung-Shik Jongmans and Francisco Ferreira

Published in: LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract

Programming distributed systems is difficult. Multiparty session typing (MPST) is a method to automatically prove safety and liveness of protocol implementations relative to protocol specifications. In this paper, we introduce two new techniques to significantly improve the expressiveness of the MPST method: projection is based on implicit local types instead of explicit; type checking is based on the operational semantics of implicit local types instead of on the syntax. That is, the reduction relation on implicit local types is used not only "a posteriori" to prove type soundness (as usual), but also "a priori" to define the typing rules - synthetically. Classes of protocols that can now be specified/implemented/verified for the first time using the MPST method include: recursive protocols in which different roles participate in different branches; protocols in which a receiver chooses the sender of the first communication; protocols in which multiple roles synchronously choose both the sender and the receiver of a next communication, implemented as mixed input/output processes. We present the theory of the new techniques, as well as their future potential, and we demonstrate their present capabilities to effectively support regular expressions as global types (not possible before).

Cite as

Sung-Shik Jongmans and Francisco Ferreira. Synthetic Behavioural Typing: Sound, Regular Multiparty Sessions via Implicit Local Types (Pearl/Brave New Idea). In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 42:1-42:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{jongmans_et_al:LIPIcs.ECOOP.2023.42,
  author =	{Jongmans, Sung-Shik and Ferreira, Francisco},
  title =	{{Synthetic Behavioural Typing: Sound, Regular Multiparty Sessions via Implicit Local Types}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{42:1--42:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.42},
  URN =		{urn:nbn:de:0030-drops-182358},
  doi =		{10.4230/LIPIcs.ECOOP.2023.42},
  annote =	{Keywords: behavioural types, multiparty session types, choreographies}
}

Document

Artifact

DOI: 10.4230/DARTS.9.2.18

Synthetic Behavioural Typing: Sound, Regular Multiparty Sessions via Implicit Local Types (Artifact)

Authors: Sung-Shik Jongmans and Francisco Ferreira

Published in: DARTS, Volume 9, Issue 2, Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract

Programming distributed systems is difficult. Multiparty session typing (MPST) is a method to automatically prove safety and liveness of protocol implementations relative to protocol specifications. In the related article ("Synthetic Behavioural Typing: Sound, Regular Multiparty Sessions via Implicit Local Types", in ECOOP 2023, LIPIcs, Vol. 263, pp. 42:1-42:30), we introduce two new techniques to significantly improve the expressiveness of the MPST method: projection is based on implicit local types instead of explicit; type checking is based on the operational semantics of implicit local types instead of on the syntax. That is, the reduction relation on implicit local types is used not only "a posteriori" to prove type soundness (as usual), but also "a priori" to define the typing rules - synthetically. Classes of protocols that can now be specified/implemented/verified for the first time using the MPST method include: recursive protocols in which different roles participate in different branches; protocols in which a receiver chooses the sender of the first communication; protocols in which multiple roles synchronously choose both the sender and the receiver of a next communication, implemented as mixed input/output processes. In the related article, we present the theory of the new techniques, as well as their future potential, and we demonstrate their present capabilities to effectively support regular expressions as global types (not possible before). As evidence that the new techniques are implementable, we implemented them; this implementation is available in this artifact.

Cite as

Sung-Shik Jongmans and Francisco Ferreira. Synthetic Behavioural Typing: Sound, Regular Multiparty Sessions via Implicit Local Types (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 18:1-18:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{jongmans_et_al:DARTS.9.2.18,
  author =	{Jongmans, Sung-Shik and Ferreira, Francisco},
  title =	{{Synthetic Behavioural Typing: Sound, Regular Multiparty Sessions via Implicit Local Types (Artifact)}},
  pages =	{18:1--18:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2023},
  volume =	{9},
  number =	{2},
  editor =	{Jongmans, Sung-Shik and Ferreira, Francisco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.18},
  URN =		{urn:nbn:de:0030-drops-182580},
  doi =		{10.4230/DARTS.9.2.18},
  annote =	{Keywords: behavioural types, multiparty session types, choreographies}
}

Search Results

Documents authored by Ferreira, Francisco

Synthetic Behavioural Typing: Sound, Regular Multiparty Sessions via Implicit Local Types (Pearl/Brave New Idea)

Abstract

Cite as

Synthetic Behavioural Typing: Sound, Regular Multiparty Sessions via Implicit Local Types (Artifact)

Abstract

Cite as

Thanks for your feedback!

Could not send message