Search Results

Documents authored by Ekici, Burak

Artifact
Software
DOI: 10.4230/artifacts.24677
Subject Reduction and Progress for Synchronous MPST

Authors: Burak Ekici, Tadayoshi Kamegai, and Nobuko Yoshida

Abstract
Cite as

Burak Ekici, Tadayoshi Kamegai, Nobuko Yoshida. Subject Reduction and Progress for Synchronous MPST (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-24677,
   title = {{Subject Reduction and Progress for Synchronous MPST}}, 
   author = {Ekici, Burak and Kamegai, Tadayoshi and Yoshida, Nobuko},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:dde907697cf2446177177fa14a2d21b1c08149f5;origin=https://github.com/Apiros3/smpst-sr-smer;visit=swh:1:snp:3a02010b54199925764021babd0e391fa180a01b;anchor=swh:1:rev:583edde920ef3833382ff6c9130f0d20db90744b}{\texttt{swh:1:dir:dde907697cf2446177177fa14a2d21b1c08149f5}} (visited on 2025-09-22)},
   url = {https://github.com/Apiros3/smpst-sr-smer},
   doi = {10.4230/artifacts.24677},
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.19
Formalising Subject Reduction and Progress for Multiparty Session Processes

Authors: Burak Ekici, Tadayoshi Kamegai, and Nobuko Yoshida

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Multiparty session types (MPST) provide a robust typing discipline for specifying and verifying communication protocols in concurrent and distributed systems involving multiple participants. This work formalises the non-stuck theorem for synchronous MPST in the Coq proof assistant, ensuring that well-typed communications never get stuck. We present a fully mechanised proof of the theorem, where recursive type unfoldings are modelled as infinite trees, leveraging coinductive reasoning. This marks the first formal proof to incorporate precise subtyping, aiming to extend the typability of processes thus precision of the type system. The proof is grounded in fundamental properties such as subject reduction and progress. During the mechanisation process, we discovered that the structural congruence rule for recursive processes, as presented in several prior works on MPST, violates subject reduction. We resolve this issue by revising and formalising the rule to ensure the preservation of type soundness. Our approach to formal proofs about infinite type trees involves analysing their finite prefixes through inductive reasoning within outer-level coinductively stated goals. We employ the greatest fixed point of the parameterised least fixed point technique to define coinductive predicates and use parameterised coinduction to prove properties. The formalisation comprises approximately 16K lines of Coq code, accessible at: https://github.com/Apiros3/smpst-sr-smer.
Cite as

Burak Ekici, Tadayoshi Kamegai, and Nobuko Yoshida. Formalising Subject Reduction and Progress for Multiparty Session Processes. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 19:1-19:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ekici_et_al:LIPIcs.ITP.2025.19,
  author =	{Ekici, Burak and Kamegai, Tadayoshi and Yoshida, Nobuko},
  title =	{{Formalising Subject Reduction and Progress for Multiparty Session Processes}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{19:1--19:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.19},
  URN =		{urn:nbn:de:0030-drops-246177},
  doi =		{10.4230/LIPIcs.ITP.2025.19},
  annote =	{Keywords: multiparty session types, type trees, subtyping, progress, subject reduction, non-stuck theorem, Coq}
}
Artifact
Software
DOI: 10.4230/artifacts.22491
https://github.com/ekiciburak/sessionTreeST/tree/localtype

Authors: Burak Ekici and Nobuko Yoshida

Abstract
Cite as

Burak Ekici, Nobuko Yoshida. https://github.com/ekiciburak/sessionTreeST/tree/localtype (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-22491,
   title = {{https://github.com/ekiciburak/sessionTreeST/tree/localtype}}, 
   author = {Ekici, Burak and Yoshida, Nobuko},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:33823a0054801bcf4ea95f2dffe733579cbd53c8;origin=https://github.com/ekiciburak/sessionTreeST;visit=swh:1:snp:e36eb4662d8731a175e95b8081f861339f588412;anchor=swh:1:rev:a8aafb319882c90f11b2b43032ce9faabace5f95}{\texttt{swh:1:dir:33823a0054801bcf4ea95f2dffe733579cbd53c8}} (visited on 2024-11-28)},
   url = {https://github.com/ekiciburak/sessionTreeST/tree/itp2024},
   doi = {10.4230/artifacts.22491},
}
Document
DOI: 10.4230/LIPIcs.ITP.2024.13
Completeness of Asynchronous Session Tree Subtyping in Coq

Authors: Burak Ekici and Nobuko Yoshida

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
Multiparty session types (MPST) serve as a foundational framework for formally specifying and verifying message passing protocols. Asynchronous subtyping in MPST allows for typing optimised programs preserving type safety and deadlock freedom under asynchronous interactions where the message order is preserved and sending is non-blocking. The optimisation is obtained by message reordering, which allows for sending messages earlier or receiving them later. Sound subtyping algorithms have been extensively studied and implemented as part of various programming languages and tools including C, Rust and C-MPI. However, formalising all such permutations under sequencing, selection, branching and recursion in session types is an intricate task. Additionally, checking asynchronous subtyping has been proven to be undecidable. This paper introduces the first formalisation of asynchronous subtyping in MPST within the Coq proof assistant. We first decompose session types into session trees that do not involve branching and selection, and then establish a coinductive refinement relation over them to govern subtyping. To showcase our formalisation, we prove example subtyping schemas that appear in the literature, all of which cannot be verified, at the same time, by any of the existing decidable sound algorithms. Additionally, we take the (inductive) negation of the refinement relation from a prior work by Ghilezan et al. [Ghilezan et al., 2023] and re-implement it, significantly reducing the number of rules (from eighteen to eight). We establish the completeness of subtyping with respect to its negation in Coq, addressing the issues concerning the negation rules outlined in the previous work [Ghilezan et al., 2023]. In the formalisation, we use the greatest fixed point of the least fixed point technique, facilitated by the paco library, to define coinductive predicates. We employ parametrised coinduction to prove their properties. The formalisation consists of roughly 10K lines of Coq code, accessible at: https://github.com/ekiciburak/sessionTreeST/tree/itp2024.
Cite as

Burak Ekici and Nobuko Yoshida. Completeness of Asynchronous Session Tree Subtyping in Coq. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 13:1-13:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{ekici_et_al:LIPIcs.ITP.2024.13,
  author =	{Ekici, Burak and Yoshida, Nobuko},
  title =	{{Completeness of Asynchronous Session Tree Subtyping in Coq}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{13:1--13:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.13},
  URN =		{urn:nbn:de:0030-drops-207418},
  doi =		{10.4230/LIPIcs.ITP.2024.13},
  annote =	{Keywords: asynchronous multiparty session types, session trees, subtyping, Coq}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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