Search Results

Documents authored by Tirore, Dawit

Document
DOI: 10.4230/LIPIcs.ECOOP.2025.31
Multiparty Asynchronous Session Types: A Mechanised Proof of Subject Reduction

Authors: Dawit Tirore, Jesper Bengtson, and Marco Carbone

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
Session types offer a type-based approach to describing the message exchange protocols between participants in communication-based systems. Initially, they were introduced in a binary setting, specifying communication patterns between two components. With the advent of multiparty session types (MPST), the typing discipline was extended to arbitrarily many components. In MPST, communication patterns are given in terms of global types, an Alice-Bob notation that gives a global view of how components interact. A central theorem of MPST is subject reduction: a well-typed system remains well-typed after reduction. The literature contains some formulations of MPST with proofs of subject reduction that have later been shown to be incorrect. In this paper, we show that the subject reduction proof of the original formulation of MPST by Honda et al. contains some flaws. Additionally, we provide a restriction to the theory and show that, for this fragment, subject reduction does indeed hold. Finally, we use subject reduction to show that well-typed processes never go wrong. All of our proofs are mechanised using the Coq proof assistant.
Cite as

Dawit Tirore, Jesper Bengtson, and Marco Carbone. Multiparty Asynchronous Session Types: A Mechanised Proof of Subject Reduction. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 31:1-31:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{tirore_et_al:LIPIcs.ECOOP.2025.31,
  author =	{Tirore, Dawit and Bengtson, Jesper and Carbone, Marco},
  title =	{{Multiparty Asynchronous Session Types: A Mechanised Proof of Subject Reduction}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{31:1--31:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.31},
  URN =		{urn:nbn:de:0030-drops-233238},
  doi =		{10.4230/LIPIcs.ECOOP.2025.31},
  annote =	{Keywords: Session types, Multiparty, Mechanisation, Coq}
}
Document
Artifact
DOI: 10.4230/DARTS.11.2.3
Multiparty Asynchronous Session Types: A Mechanised Proof of Subject Reduction (Artifact)

Authors: Dawit Tirore, Jesper Bengtson, and Marco Carbone

Published in: DARTS, Volume 11, Issue 2, Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
Session types offer a type-based approach to describing the message exchange protocols between participants in communication-based systems. Initially, they were introduced in a binary setting, specifying communication patterns between two components. With the advent of multiparty session types (MPST), the typing discipline was extended to arbitrarily many components. In MPST, communication patterns are given in terms of global types, an Alice-Bob notation that gives a global view of how components interact. A central theorem of MPST is subject reduction: a well-typed system remains well-typed after reduction. The literature contains some formulations of MPST with proofs of subject reduction that have later been shown to be incorrect. In this paper, we show that the subject reduction proof of the original formulation of MPST by Honda et al. contains some flaws. Additionally, we provide a restriction to the theory and show that, for this fragment, subject reduction does indeed hold. Finally, we use subject reduction to show that well-typed processes never go wrong. All of our proofs are mechanised using the Coq proof assistant. This artifact accompanies our paper [Dawit Tirore et al., 2025]. It contains the Coq mechanisation of the theory described therein.
Cite as

Dawit Tirore, Jesper Bengtson, and Marco Carbone. Multiparty Asynchronous Session Types: A Mechanised Proof of Subject Reduction (Artifact). In Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025). Dagstuhl Artifacts Series (DARTS), Volume 11, Issue 2, pp. 3:1-3:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Article{tirore_et_al:DARTS.11.2.3,
  author =	{Tirore, Dawit and Bengtson, Jesper and Carbone, Marco},
  title =	{{Multiparty Asynchronous Session Types: A Mechanised Proof of Subject Reduction (Artifact)}},
  pages =	{3:1--3:5},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2025},
  volume =	{11},
  number =	{2},
  editor =	{Tirore, Dawit and Bengtson, Jesper and Carbone, Marco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.11.2.3},
  URN =		{urn:nbn:de:0030-drops-233467},
  doi =		{10.4230/DARTS.11.2.3},
  annote =	{Keywords: Session types, Multiparty, Mechanisation, Coq}
}
Document
DOI: 10.4230/LIPIcs.ITP.2023.28
A Sound and Complete Projection for Global Types

Authors: Dawit Tirore, Jesper Bengtson, and Marco Carbone

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract
Multiparty session types is a typing discipline used to write specifications, known as global types, for branching and recursive message-passing systems. A necessary operation on global types is projection to abstractions of local behaviour, called local types. Typically, this is a computable partial function that given a global type and a role erases all details irrelevant to this role. Computable projection functions in the literature are either unsound or too restrictive when dealing with recursion and branching. Recent work has taken a more general approach to projection defining it as a coinductive, but not computable, relation. Our work defines a new computable projection function that is sound and complete with respect to its coinductive counterpart and, hence, equally expressive. All results have been mechanised in the Coq proof assistant.
Cite as

Dawit Tirore, Jesper Bengtson, and Marco Carbone. A Sound and Complete Projection for Global Types. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 28:1-28:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{tirore_et_al:LIPIcs.ITP.2023.28,
  author =	{Tirore, Dawit and Bengtson, Jesper and Carbone, Marco},
  title =	{{A Sound and Complete Projection for Global Types}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{28:1--28:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.28},
  URN =		{urn:nbn:de:0030-drops-184039},
  doi =		{10.4230/LIPIcs.ITP.2023.28},
  annote =	{Keywords: Session types, Mechanisation, Projection, Coq}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact