Document Open Access Logo

Abstract Subtyping for Asynchronous Multiparty Sessions

Authors Laura Bocchi , Andy King , Maurizio Murgia , Simon Thompson

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.CONCUR.2025.10.pdf
  • Filesize: 1.02 MB
  • 19 pages
HTML5 Logo HTML (experimental)
LIPIcs.CONCUR.2025.10.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Program reasoning
  • Theory of computation → Process calculi
Keywords
  • asynchrony
  • session subtyping
  • automata
  • abstract interpretation

Metrics

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

Abstract

Session subtyping answers the question of whether a program in a communicating system can be safely substituted for another, when their communication behaviour is described by session types. Asynchronous session subtyping is undecidable, even for two participants, hence the interest in sound, but incomplete, subtyping algorithms. Asynchronous multiparty subtyping can be formulated by decomposing session types into single input and output types which preclude, respectively, external and internal choice. This paper shows how abstract interpretation can sit atop this approach and how it leads to an algorithm that can prove subtyping for intricate communication patterns.

Cite As Get BibTex

Laura Bocchi, Andy King, Maurizio Murgia, and Simon Thompson. Abstract Subtyping for Asynchronous Multiparty Sessions. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CONCUR.2025.10

Author Details

Laura Bocchi
  • University of Kent, Canterbury, UK
Andy King
  • University of Kent, Canterbury, UK
Maurizio Murgia
  • Gran Sasso Science Institute, L'Aquila, Italy
Simon Thompson
  • University of Kent, Canterbury, UK

Funding

This work was supported by EPSRC project EP/T014512/1 (STARDUST) and the PRIN 2022 PNRR project DeLiCE (F53D23009130001).

References

  1. Franco Barbanera and Ugo de'Liguoro. Sub-behaviour relations for session-based client/server systems. Mathematical Structures in Computer Science, 25(6):1339-1381, 2015. URL: https://doi.org/10.1017/S096012951400005X.
  2. Giovanni Bernardi, Ilaria Castellani, Paul Laforgue, and Léo Stefanesco. Constructive Characterisations of the MUST-preorder for Asynchrony. In European Symposium on Programming, volume 15694 of Lecture Notes in Computer Science, pages 88-116, 2025. URL: https://doi.org/10.1007/978-3-031-91118-7_4.
  3. Laura Bocchi, Andy King, and Maurizio Murgia. Asynchronous Subtyping by Trace Relaxation. In Tools and Algorithms for the Construction and Analysis of Systems, volume 14570 of Lecture Notes in Computer Science, pages 207-226, Berlin, 2024. Springer-Verlag. URL: https://doi.org/10.1007/978-3-031-57246-3_12.
  4. François Bourdoncle. Efficient Chaotic Iteration Strategies with Widenings. In Formal Methods in Programming and Their Applications, volume 735 of Lecture Notes in Computer Science, pages 128-141, New York, 1993. Springer-Verlag. URL: https://doi.org/10.1007/BFb0039704.
  5. Mario Bravetti, Marco Carbone, Julien Lange, Nobuko Yoshida, and Gianluigi Zavattaro. A Sound Algorithm for Asychronous Session Subtyping. In International Conference on Concurrency Theory, volume 140 of LIPIcs, pages 38:1-38:16, Dagstuhl, 2019. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2019.38.
  6. Mario Bravetti, Marco Carbone, Julien Lange, Nobuko Yoshida, and Gianluigi Zavattaro. A Sound Algorithm for Asychronous Session Subtyping and its Implementation. Logical Methods in Computer Science, 17(1):1-35, 2021. URL: https://doi.org/10.23638/LMCS-17(1:20)2021.
  7. Mario Bravetti, Marco Carbone, and Gianluigi Zavattaro. Undecidability of Asynchronous Session Subtyping. Information and Computation, 256:300-320, 2017. URL: https://doi.org/10.1016/j.ic.2017.07.010.
  8. Mario Bravetti, Marco Carbone, and Gianluigi Zavattaro. On the Boundary between Decidability and Undecidability of Asynchronous Session Subtyping. Theoretical Computer Science, 722:19-51, 2018. URL: https://doi.org/10.1016/j.tcs.2018.02.010.
  9. Mario Bravetti, Julien Lange, and Gianluigi Zavattaro. Fair Asynchronous Session Subtyping. Logical Methods in Computer Science, 20:5:1-5:47, 2024. URL: https://doi.org/10.48550/arXiv.2101.08181.
  10. Janusz Brzozowski. Derivatives of Regular Expressions. Journal of the ACM, 11(4):481-494, 1964. URL: https://doi.org/10.1145/321239.321249.
  11. David Castro-Perez and Nobuko Yoshida. CAMP: cost-aware multiparty session protocols. Proc. ACM Program. Lang., 4(OOPSLA):155:1-155:30, 2020. URL: https://doi.org/10.1145/3428223.
  12. Tzu-Chun Chen, Mariangiola Dezani-Ciancaglini, Alceste Scalas, and Nobuko Yoshida. On the Preciseness of Subtyping in Session Types. Logical Methods in Computer Science, 13(2):1-61, 2017. URL: https://doi.org/10.23638/LMCS-13(2:12)2017.
  13. Tzu-Chun Chen, Mariangiola Dezani-Ciancaglini, and Nobuko Yoshida. On the Preciseness of Subtyping in Session Types. In Principles and Practice of Declarative Programming, pages 135-146, New York, 2014. ACM Press. URL: https://doi.org/10.1145/2643135.2643138.
  14. Tae-Hyoung Choi, Oukseh Lee, Hyunha Kim, and Kyung-Goo Doh. A Practical String Analyzer by the Widening Approach. In Asian Symposium on Programming and Systems, volume 4279 of Lecture Notes in Computer Science, pages 374-388, Berlin, 2006. Springer-Verlag. URL: https://doi.org/10.1007/11924661_23.
  15. Liron Cohen. Non-well-founded Deduction for Induction and Coinduction. In Conference on Automated Deduction, volume 12699 of Lecture Notes in Computer Science, pages 3-24. Springer-Verlag, 2021. URL: https://doi.org/10.1007/978-3-030-79876-5_1.
  16. Bruno Courcelle. Fundamental Properties of Infinite Trees. Theoretical Computer Science, 25:95-169, 1983. URL: https://doi.org/10.1016/0304-3975(83)90059-2.
  17. Patrick Cousot and Radhia Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Principles of Programming Languages, pages 238-252, New York, 1977. ACM Press. URL: https://doi.org/10.1145/512950.512973.
  18. Zak Cutner, Nobuko Yoshida, and Martin Vassor. Deadlock-Free Asynchronous Message Reordering in Rust with Multiparty Session Types. In Symposium on Principles and Practice of Parallel Programming, pages 246-261, New York, 2022. ACM Press. URL: https://doi.org/10.1145/3503221.3508404.
  19. Rocco De Nicola and Matthew Hennessy. Testing Equivalences for Processes. Theoretical Computer Science, 34:83-133, 1984. URL: https://doi.org/10.1007/BFb0036936.
  20. Rocco De Nicola and Hernán Melgratti. Multiparty Testing Preorders. Logical Methods in Computer Science, 19:1:1-1:31, 2016. URL: https://doi.org/10.46298/lmcs-19(1:1)2023.
  21. Romain Demangeon and Kohei Honda. Full Abstraction in a Subtyped pi-Calculus with Linear Types. In International Conference on Concurrency Theory, volume 6901 of Lecture Notes in Computer Science, pages 280-296, Berlin, 2011. Springer-Verlag. URL: https://doi.org/10.1007/978-3-642-23217-6_19.
  22. Romain Demangeon, Kohei Honda, Raymond Hu, Rumyana Neykova, and Nobuko Yoshida. Practical interruptible conversations: distributed dynamic verification with multiparty session types and Python. Formal Methods in Systems Design, 46(3):197-225, 2015. URL: https://doi.org/10.1007/s10703-014-0218-8.
  23. Burak Ekici and Nobuko Yoshida. Completeness of asynchronous session tree subtyping in coq. In Yves Bertot, Temur Kutsia, and Michael Norrish, editors, International Conference on Interactive Theorem Proving, volume 309 of LIPIcs, pages 13:1-13:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPICS.ITP.2024.13.
  24. Simon Fowler. An Erlang Implementation of Multiparty Session Actors. In Interaction and Concurrency Experience, volume 223 of EPTCS, pages 36-50, 2016. URL: https://doi.org/10.4204/EPTCS.223.3.
  25. Simon Gay and Malcolm Hole. Types and Subtypes for Client-Server Interactions. In European Symposium on Programming, volume 1576 of Lecture Notes in Computer Science, pages 74-90, Berlin, 1999. Springer-Verlag. URL: https://doi.org/10.1007/3-540-49099-X_6.
  26. Simon Gay and Malcolm Hole. Subtyping for Session Types in the Pi Calculus. Acta Informatica, 42:191-225, 2005. URL: https://doi.org/10.1007/s00236-005-0177-z.
  27. 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.
  28. Steve Hill. Combinators for Parsing Expressions. Journal of Functional Programming, 6(3):445-463, 1996. URL: https://doi.org/10.1017/S0956796800001799.
  29. Kohei Honda, Vasco T. Vasconcelos, and Makoto Kubo. Language Primitives and Type Disciplines for Structured Communication-based Programming. In European Symposium on Programming, volume 1381 of Lecture Notes in Computer Science, pages 22-138, Berlin, 1998. Springer-Verlag. URL: https://doi.org/10.1007/BFb0053567.
  30. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In Principles of Programming Languages, pages 273-284. ACM, 2008. URL: https://doi.org/10.1145/1328438.1328472.
  31. Raymond Hu, Nobuko Yoshida, and Kohei Honda. Session-Based Distributed Programming in Java. In European Conference on Object-Oriented Programming, volume 5142 of Lecture Notes in Computer Science, pages 516-541, Berlin, 2008. Springer-Verlag. URL: https://doi.org/10.1007/978-3-540-70592-5_22.
  32. Gerda Janssens and Maurice Bruynooghe. Deriving Descriptions of Possible Values of Program Variables by Means of Abstract Interpretation. Journal of Logic Programming, 13(2&3):205-258, 1992. URL: https://doi.org/10.1016/0743-1066(92)90032-X.
  33. Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida. Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types. In European Conference on Object-Oriented Programming, volume 222, pages 4:1-4:29, Dagstuhl, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2022.4.
  34. Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida. Fencing off Go: liveness and safety for channel-based programming. In Principles of Programming Languages, pages 748-761, 2017. URL: https://doi.org/10.1145/3009837.3009847.
  35. Julien Lange and Nobuko Yoshida. On the Undecidability of Asynchronous Session Subtyping. In Foundations of Software Science and Computation Structures, volume 10203 of Lecture Notes in Computer Science, pages 441-457, Berlin, 2017. Springer-Verlag. URL: https://doi.org/10.1007/978-3-662-54458-7_26.
  36. Elaine Li, Felix Stutz, and Thomas Wies. Deciding Subtyping for Asynchronous Multiparty Sessions. In European Symposium on Programming, volume 14576 of Lecture Notes in Computer Science, pages 176-205, Berlin, 2024. Springer-Verlag. URL: https://doi.org/10.1007/978-3-031-57262-3_8.
  37. Dimitris Mostrous and Vasco Vasconcelos. Session Typing for a Featherweight Erlang. In Coordination Models and Languages, Lecture Notes in Computer Science, pages 95-109, 2011. URL: https://doi.org/10.1007/978-3-642-21464-6_7.
  38. Dimitris Mostrous, Nobuko Yoshida, and Kohei Honda. Global Principal Typing in Partially Commutative Asynchronous Sessions. In European Symposium on Programming, volume 5502 of Lecture Notes in Computer Science, pages 316-332, Berlin, 2009. Springer-Verlag. URL: https://doi.org/10.1007/978-3-642-00590-9_23.
  39. Maurizio Murgia. A fixed-points based framework for compliance of behavioural contracts. J. Log. Algebraic Methods Program., 120:100641, 2021. URL: https://doi.org/10.1016/j.jlamp.2021.100641.
  40. Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002. Google Scholar
  41. Arend Rensink and Walter Vogler. Fair testing. Information and Computation, 205(2):125-198, 2007. URL: https://doi.org/10.1016/j.ic.2006.06.002.
  42. Pascal Van Hentenryck, Agostino Cortesi, and Baudouin Le Charlier. Type Analysis of Prolog Using Type Graphs. In Programming Language Design and Implementation, pages 337-348. ACM Press, 1994. URL: https://doi.org/10.1145/773473.178479.
  43. Pascal Van Hentenryck, Agostino Cortesi, and Baudouin Le Charlier. Type Analysis of Prolog Using Type Graphs. Journal of Logic Programming, 22(3):179-209, 1995. URL: https://doi.org/10.1016/0743-1066(94)00021-W.
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