Document Open Access Logo

A Sound and Complete Characterization of Fair Asynchronous Session Subtyping

Authors Mario Bravetti , Luca Padovani , Gianluigi Zavattaro

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.CONCUR.2025.11.pdf
  • Filesize: 0.88 MB
  • 17 pages
HTML5 Logo HTML (experimental)
LIPIcs.CONCUR.2025.11.html

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • Binary sessions
  • session types
  • fair asynchronous subtyping

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Session types are abstractions of communication protocols enabling the static analysis of message-passing processes. Refinement notions for session types are key to support safe forms of process substitution while preserving their compatibility with the rest of the system. Recently, a fair refinement relation for asynchronous session types has been defined allowing the anticipation of message outputs with respect to an unbounded number of message inputs. This refinement is useful to capture common patterns in communication protocols that take advantage of asynchrony. However, while the semantic (à la testing) definition of such refinement is straightforward, its characterization has proved to be quite challenging. In fact, only a sound but not complete characterization is known so far. In this paper we close this open problem by presenting a sound and complete characterization of asynchronous fair refinement for session types. We relate this characterization to those given in the literature for synchronous session types by leveraging a novel labelled transition system of session types that embeds their asynchronous semantics.

Cite As Get BibTex

Mario Bravetti, Luca Padovani, and Gianluigi Zavattaro. A Sound and Complete Characterization of Fair Asynchronous Session Subtyping. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 11:1-11:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CONCUR.2025.11

Author Details

Mario Bravetti
  • University of Bologna, Italy
Luca Padovani
  • University of Bologna, Italy
Gianluigi Zavattaro
  • University of Bologna, Italy

Funding

The authors have been partially supported by the ANR project SmartCloud ANR-23-CE25-0012 and the PNRR project CN-HPC Spoke 9 Innovation Grant RTMER.

Acknowledgements

We are grateful to the anonymous CONCUR'25 reviewers for their feedback.

References

  1. Davide Ancona, Francesco Dagnino, and Elena Zucca. Generalizing inference systems by coaxioms. In Hongseok Yang, editor, Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10201 of Lecture Notes in Computer Science, pages 29-55. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54434-1_2.
  2. Laura Bocchi, Andy King, and Maurizio Murgia. Asynchronous subtyping by trace relaxation. In Bernd Finkbeiner and Laura Kovács, editors, Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I, volume 14570 of Lecture Notes in Computer Science, pages 207-226. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-57246-3_12.
  3. Daniel Brand and Pitro Zafiropulo. On communicating finite-state machines. J. ACM, 30(2):323-342, 1983. URL: https://doi.org/10.1145/322374.322380.
  4. Mario Bravetti, Marco Carbone, Julien Lange, Nobuko Yoshida, and Gianluigi Zavattaro. A sound algorithm for asynchronous session subtyping. In CONCUR, volume 140 of LIPIcs, pages 38:1-38:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPICS.CONCUR.2019.38.
  5. Mario Bravetti, Marco Carbone, Julien Lange, Nobuko Yoshida, and Gianluigi Zavattaro. A sound algorithm for asynchronous session subtyping and its implementation. Log. Methods Comput. Sci., 17(1), 2021. URL: https://lmcs.episciences.org/7238.
  6. Mario Bravetti, Julien Lange, and Gianluigi Zavattaro. Fair asynchronous session subtyping. Log. Methods Comput. Sci., 20(4), 2024. URL: https://doi.org/10.46298/LMCS-20(4:5)2024.
  7. Mario Bravetti, Luca Padovani, and Gianluigi Zavattaro. A Sound and Complete Characterization of Fair Asynchronous Session Subtyping. Technical report, University of Bologna, 2025. URL: https://doi.org/10.48550/arXiv.2506.06078.
  8. Janusz A. Brzozowski. Derivatives of regular expressions. J. ACM, 11(4):481-494, 1964. URL: https://doi.org/10.1145/321239.321249.
  9. Tzu-Chun Chen, Mariangiola Dezani-Ciancaglini, Alceste Scalas, and Nobuko Yoshida. On the preciseness of subtyping in session types. Log. Methods Comput. Sci., 13(2), 2017. URL: https://doi.org/10.23638/LMCS-13(2:12)2017.
  10. Luca Ciccone, Francesco Dagnino, and Luca Padovani. Fair termination of multiparty sessions. J. Log. Algebraic Methods Program., 139:100964, 2024. URL: https://doi.org/10.1016/J.JLAMP.2024.100964.
  11. Luca Ciccone and Luca Padovani. Fair termination of binary sessions. Proc. ACM Program. Lang., 6(POPL):1-30, 2022. URL: https://doi.org/10.1145/3498666.
  12. Luca Ciccone and Luca Padovani. Inference systems with corules for combined safety and liveness properties of binary session types. Log. Methods Comput. Sci., 18(3), 2022. URL: https://doi.org/10.46298/LMCS-18(3:27)2022.
  13. Bruno Courcelle. Fundamental properties of infinite trees. Theor. Comput. Sci., 25:95-169, 1983. URL: https://doi.org/10.1016/0304-3975(83)90059-2.
  14. Francesco Dagnino. Coaxioms: flexible coinductive definitions by inference systems. Log. Methods Comput. Sci., 15(1), 2019. URL: https://doi.org/10.23638/LMCS-15(1:26)2019.
  15. Simon J. Gay. Subtyping supports safe session substitution. In Sam Lindley, Conor McBride, Philip W. Trinder, and Donald Sannella, editors, A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, volume 9600 of Lecture Notes in Computer Science, pages 95-108. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-30936-1_5.
  16. Simon J. Gay and Malcolm Hole. Subtyping for session types in the pi calculus. Acta Informatica, 42(2-3):191-225, 2005. URL: https://doi.org/10.1007/S00236-005-0177-Z.
  17. Silvia Ghilezan, Jovanka Pantovic, Ivan Prokic, Alceste Scalas, and Nobuko Yoshida. Precise subtyping for asynchronous multiparty sessions. Proc. ACM Program. Lang., 5(POPL):1-28, 2021. URL: https://doi.org/10.1145/3434297.
  18. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. J. ACM, 63(1):9, 2016. URL: https://doi.org/10.1145/2827695.
  19. Barbara Liskov and Jeannette M. Wing. A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst., 16(6):1811-1841, 1994. URL: https://doi.org/10.1145/197320.197383.
  20. Robin Milner. Communication and concurrency. PHI Series in computer science. Prentice Hall, 1989. Google Scholar
  21. Dimitris Mostrous and Nobuko Yoshida. Session typing and asynchronous subtyping for the higher-order π-calculus. Inf. Comput., 241:227-263, 2015. URL: https://doi.org/10.1016/J.IC.2015.02.002.
  22. Dimitris Mostrous, Nobuko Yoshida, and Kohei Honda. Global principal typing in partially commutative asynchronous sessions. In ESOP, volume 5502 of Lecture Notes in Computer Science, pages 316-332. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-00590-9_23.
  23. Luca Padovani. Fair subtyping for multi-party session types. Math. Struct. Comput. Sci., 26(3):424-464, 2016. URL: https://doi.org/10.1017/S096012951400022X.
  24. Luca Padovani and Gianluigi Zavattaro. Fair termination of asynchronous binary sessions, 2025. URL: https://doi.org/10.48550/arXiv.2503.07273.
  25. Rob van Glabbeek and Peter Höfner. Progress, justness, and fairness. ACM Comput. Surv., 52(4):69:1-69:38, 2019. URL: https://doi.org/10.1145/3329125.
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