Document Open Access Logo

Multiparty Asynchronous Session Types: A Mechanised Proof of Subject Reduction

Authors Dawit Tirore , Jesper Bengtson , Marco Carbone

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2025.31.pdf
  • Filesize: 1.11 MB
  • 30 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Process calculi
  • Theory of computation → Type structures
  • Theory of computation → Program specifications
Keywords
  • Session types
  • Multiparty
  • Mechanisation
  • Coq

Metrics

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

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 Get BibTex

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) https://doi.org/10.4230/LIPIcs.ECOOP.2025.31

Author Details

Dawit Tirore
  • IT University of Copenhagen, Denmark
Jesper Bengtson
  • IT University of Copenhagen, Denmark
Marco Carbone
  • IT University of Copenhagen, Denmark

Funding

This work was supported by DFF-Research Project 1 Grant no. 1026-00385A, from The Danish Council for Independent Research for the Natural Sciences (FNU).

Supplementary Materials

References

  1. Scribble: Describing Multy Party Protocols. URL: http://www.scribble.org.
  2. Session Types in Programming Languages: A Collection of Implementations. URL: http://groups.inf.ed.ac.uk/abcd/session-implementations.html.
  3. Advanced Message Queuing Protocol. http://www.iona.com/opensource/amqp/, 2015.
  4. Lorenzo Bettini, Mario Coppo, Loris D'Antoni, Marco De Luca, Mariangiola Dezani-Ciancaglini, and Nobuko Yoshida. Global progress in dynamically interleaved multiparty sessions. In Franck van Breugel and Marsha Chechik, editors, CONCUR 2008 - Concurrency Theory, 19th International Conference, CONCUR 2008, Toronto, Canada, August 19-22, 2008. Proceedings, volume 5201 of Lecture Notes in Computer Science, pages 418-433. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-85361-9_33.
  5. Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. A formally-verified C compiler supporting floating-point arithmetic. In Alberto Nannarelli, Peter-Michael Seidel, and Ping Tak Peter Tang, editors, 21st IEEE Symposium on Computer Arithmetic, pages 107-115. IEEE Computer Society, 2013. URL: https://doi.org/10.1109/ARITH.2013.30.
  6. Mario Bravetti, Marco Carbone, and Gianluigi Zavattaro. Undecidability of asynchronous session subtyping. Inf. Comput., 256:300-320, 2017. URL: https://doi.org/10.1016/J.IC.2017.07.010.
  7. Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logic propositions as session types. Math. Struct. Comput. Sci., 26(3):367-423, 2016. URL: https://doi.org/10.1017/S0960129514000218.
  8. Marco Carbone and Søren Debois. A graphical approach to progress for structured communication in web services. In Simon Bliudze, Roberto Bruni, Davide Grohmann, and Alexandra Silva, editors, Proceedings Third Interaction and Concurrency Experience: Guaranteed Interaction, ICE 2010, Amsterdam, The Netherlands, 10th of June 2010, volume 38 of EPTCS, pages 13-27, 2010. URL: https://doi.org/10.4204/EPTCS.38.4.
  9. Marco Carbone, Kohei Honda, and Nobuko Yoshida. Structured communication-centred programming for web services. In Rocco De Nicola, editor, Programming Languages and Systems, 16th European Symposium on Programming, ESOP 2007, Held as Part of the Joint European Conferences on Theory and Practics of Software, ETAPS 2007, Braga, Portugal, March 24 - April 1, 2007, Proceedings, volume 4421 of Lecture Notes in Computer Science, pages 2-17. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-71316-6_2.
  10. Marco Carbone, Kohei Honda, and Nobuko Yoshida. Structured communication-centered programming for web services. ACM Trans. Program. Lang. Syst., 34(2):8:1-8:78, 2012. URL: https://doi.org/10.1145/2220365.2220367.
  11. Marco Carbone, Sam Lindley, Fabrizio Montesi, Carsten Schürmann, and Philip Wadler. Coherence generalises duality: A logical explanation of multiparty session types. In Josée Desharnais and Radha Jagadeesan, editors, 27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Québec City, Canada, volume 59 of LIPIcs, pages 33:1-33:15, Germany, 2016. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2016.33.
  12. Marco Carbone, Sonia Marin, and Carsten Schürmann. A logical interpretation of asynchronous multiparty compatibility. In Robert Glück and Bishoksan Kafle, editors, Logic-Based Program Synthesis and Transformation - 33rd International Symposium, LOPSTR 2023, Cascais, Portugal, October 23-24, 2023, Proceedings, volume 14330 of Lecture Notes in Computer Science, pages 99-117. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-45784-5_7.
  13. David Castro-Perez, Francisco Ferreira, Lorenzo Gheri, and Nobuko Yoshida. Zooid: a DSL for certified multiparty computation: from mechanised metatheory to certified multiparty processes. In Proceedings of PLDI, pages 237-251. ACM, 2021. URL: https://doi.org/10.1145/3453483.3454041.
  14. David Castro-Perez, Francisco Ferreira, and Nobuko Yoshida. EMTST: engineering the meta-theory of session types. In Armin Biere and David Parker, editors, Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part II, volume 12079 of Lecture Notes in Computer Science, pages 278-285. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-45237-7_17.
  15. Arthur Charguéraud. The locally nameless representation. J. Autom. Reason., 49(3):363-408, 2012. URL: https://doi.org/10.1007/S10817-011-9225-2.
  16. Chung-Kil, Georg Neis Georg, Derek Dreyer, and Victor Vafeiadis. The power of parameterization in coinductive proof. SIGPLAN Notices, 48(1):193-206, 2013. URL: https://doi.org/10.1145/2480359.2429093.
  17. Mario Coppo, Mariangiola Dezani-Ciancaglini, Nobuko Yoshida, and Luca Padovani. Global progress for dynamically interleaved multiparty sessions. MSCS, 760:1-65, 2015. Google Scholar
  18. Nils Anders Danielsson and Thorsten Altenkirch. Subtyping, declaratively. In Claude Bolduc, Josée Desharnais, and Béchir Ktari, editors, Mathematics of Program Construction, 10th International Conference, MPC 2010, Québec City, Canada, June 21-23, 2010. Proceedings, volume 6120 of Lecture Notes in Computer Science, pages 100-118. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-13321-3_8.
  19. Pierre-Malo Deniélou and Nobuko Yoshida. Multiparty session types meet communicating automata. In Helmut Seidl, editor, Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings, volume 7211 of Lecture Notes in Computer Science, pages 194-213. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-28869-2_10.
  20. Simon Fowler. An erlang implementation of multiparty session actors. In Massimo Bartoletti, Ludovic Henrio, Sophia Knight, and Hugo Torres Vieira, editors, Proceedings 9th Interaction and Concurrency Experience, ICE 2016, Heraklion, Greece, 8-9 June 2016, volume 223 of EPTCS, pages 36-50, 2016. URL: https://doi.org/10.4204/EPTCS.223.3.
  21. Simon J. Gay and Malcolm Hole. Types and subtypes for client-server interactions. In S. Doaitse Swierstra, editor, Programming Languages and Systems, 8th European Symposium on Programming, ESOP'99, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'99, Amsterdam, The Netherlands, 22-28 March, 1999, Proceedings, volume 1576 of Lecture Notes in Computer Science, pages 74-90. Springer, 1999. URL: https://doi.org/10.1007/3-540-49099-X_6.
  22. 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.
  23. Simon J. Gay, Peter Thiemann, and Vasco T. Vasconcelos. Duality of session types: The final cut. In Stephanie Balzer and Luca Padovani, editors, Proceedings of the 12th International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software, PLACES@ETAPS 2020, Dublin, Ireland, 26th April 2020, volume 314 of EPTCS, pages 23-33, 2020. URL: https://doi.org/10.4204/EPTCS.314.3.
  24. Silvia Ghilezan, Svetlana Jaksic, Jovanka Pantovic, Alceste Scalas, and Nobuko Yoshida. Precise subtyping for synchronous multiparty sessions. Journal of Logical and Algebraic Methods in Programming, 104:127-173, 2019. URL: https://doi.org/10.1016/j.jlamp.2018.12.002.
  25. Georges Gonthier. The four colour theorem: Engineering of a formal proof. In Deepak Kapur, editor, Computer Mathematics, 8th Asian Symposium, ASCM, volume 5081 of Lecture Notes in Computer Science, page 333. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-87827-8_28.
  26. Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry. A machine-checked proof of the odd order theorem. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem Proving - 4th International Conference, ITP, volume 7998 of LNCS, pages 163-179. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39634-2_14.
  27. Thomas C. Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong Le Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason M. Rute, Alexey Solovyev, An Hoai Thi Ta, Trung Nam Tran, Diep Thi Trieu, Josef Urban, Ky Khac Vu, and Roland Zumkeller. A formal proof of the kepler conjecture. CoRR, abs/1501.02155, 2015. URL: https://arxiv.org/abs/1501.02155.
  28. Jesse Michael Han and Floris van Doorn. A formal proof of the independence of the continuum hypothesis. In Jasmin Blanchette and Catalin Hritcu, editors, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 353-366. ACM, 2020. URL: https://doi.org/10.1145/3372885.3373826.
  29. Jonas Kastberg Hinrichsen, Daniël Louwrink, Robbert Krebbers, and Jesper Bengtson. Machine-checked semantic session typing. In Catalin Hritcu and Andrei Popescu, editors, CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021, pages 178-198. ACM, 2021. URL: https://doi.org/10.1145/3437992.3439914.
  30. Kohei Honda. Types for dyadic interaction. In Eike Best, editor, CONCUR '93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 23-26, 1993, Proceedings, volume 715 of Lecture Notes in Computer Science, pages 509-523. Springer, 1993. URL: https://doi.org/10.1007/3-540-57208-2_35.
  31. Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In Proceedings of ESOP, volume 1381 of LNCS, pages 122-138. Springer, 1998. URL: https://doi.org/10.1007/BFb0053567.
  32. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In Proceedings of POPL, pages 273-284. ACM, 2008. URL: https://doi.org/10.1145/1328438.1328472.
  33. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. Journal of the ACM, 63(1):9:1-9:67, 2016. URL: https://doi.org/10.1145/2827695.
  34. Jules Jacobs, Stephanie Balzer, and Robbert Krebbers. Connectivity graphs: a method for proving deadlock freedom based on separation logic. Proc. ACM Program. Lang., 6(POPL):1-33, 2022. URL: https://doi.org/10.1145/3498662.
  35. Jules Jacobs, Stephanie Balzer, and Robbert Krebbers. Multiparty GV: functional multiparty session types with certified deadlock freedom. Proceedings of the ACM on Programming Languages, 6(ICFP):466-495, 2022. URL: https://doi.org/10.1145/3547638.
  36. Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David A. Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: formal verification of an os kernel. In Jeanna Neefe Matthews and Thomas E. Anderson, editors, Proceedings of the 22nd ACM Symposium on Operating Systems Principles, pages 207-220. ACM, 2009. URL: https://doi.org/10.1145/1629575.1629596.
  37. Robbert Krebbers, Amin Timany, and Lars Birkedal. Interactive proofs in higher-order concurrent separation logic. In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 205-217. ACM, 2017. URL: https://doi.org/10.1145/3009837.3009855.
  38. Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida. A static verification framework for message passing in go using behavioural types. In Michel Chaudron, Ivica Crnkovic, Marsha Chechik, and Mark Harman, editors, Proceedings of the 40th International Conference on Software Engineering, ICSE 2018, Gothenburg, Sweden, May 27 - June 03, 2018, pages 1137-1148. ACM, 2018. URL: https://doi.org/10.1145/3180155.3180157.
  39. Julien Lange and Nobuko Yoshida. On the undecidability of asynchronous session subtyping. In Javier Esparza and Andrzej S. Murawski, editors, Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 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 10203 of Lecture Notes in Computer Science, pages 441-457, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7_26.
  40. SIPLAN selection committee. Most Influential POPL Paper Award (2018). https://www.sigplan.org/Awards. Accessed: July 2024.
  41. The Coq development team. The Coq Proof Assistant. https://coq.inria.fr. Accessed: July 2024.
  42. The Lean development team. The Lean Proof Assistant. https://lean-lang.org. Accessed: July 2024.
  43. Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, I and II. Information and Computation, 100(1):1-40,41-77, September 1992. Google Scholar
  44. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002. URL: https://doi.org/10.1007/3-540-45949-9.
  45. Peter W. O'Hearn and David J. Pym. The logic of bunched implications. Bull. Symb. Log., 5(2):215-244, 1999. URL: https://doi.org/10.2307/421090.
  46. Peter W. O'Hearn, John C. Reynolds, and Hongseok Yang. Local reasoning about programs that alter data structures. In Laurent Fribourg, editor, Computer Science Logic, 15th International Workshop, CSL 2001. 10th Annual Conference of the EACSL, Paris, France, September 10-13, 2001, Proceedings, volume 2142 of Lecture Notes in Computer Science, pages 1-19. Springer, 2001. URL: https://doi.org/10.1007/3-540-44802-0_1.
  47. Benjamin C. Pierce. Types and programming languages. MIT Press, 2002. Google Scholar
  48. Chuta Sano, Ryan Kavanagh, and Brigitte Pientka. Mechanizing session-types using a structural view: Enforcing linearity without linearity. Proc. ACM Program. Lang., 7(OOPSLA2):374-399, 2023. URL: https://doi.org/10.1145/3622810.
  49. Alceste Scalas and Nobuko Yoshida. Less is more: multiparty session types revisited. Proc. ACM Program. Lang., 3(POPL):30:1-30:29, 2019. URL: https://doi.org/10.1145/3290343.
  50. Kathrin Stark. Mechanising Syntax with Binders in Coq. Phd thesis, Universität des Saarlandes, Fakultät für Mathematik und Informatik, Saarbrücken, Germany, 2019. Google Scholar
  51. Dawit Legesse Tirore, Jesper Bengtson, and Marco Carbone. A sound and complete projection for global types. In Adam Naumowicz and René Thiemann, editors, 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, volume 268 of LIPIcs, pages 28:1-28:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.ITP.2023.28.
  52. Philip Wadler. Propositions as sessions. In Proceedings of ICFP, pages 273-286. ACM, 2012. URL: https://doi.org/10.1145/2364527.2364568.
  53. Nobuko Yoshida and Lorenzo Gheri. A very gentle introduction to multiparty session types. In Dang Van Hung and Meenakshi D'Souza, editors, Distributed Computing and Internet Technology - 16th International Conference, ICDCIT 2020, Bhubaneswar, India, January 9-12, 2020, Proceedings, volume 11969 of Lecture Notes in Computer Science, pages 73-93. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-36987-3_5.
  54. Nobuko Yoshida and Vasco Thudichum Vasconcelos. Language primitives and type discipline for structured communication-based programming revisited: Two systems for higher-order session communication. In Maribel Fernández and Claude Kirchner, editors, Proceedings of the First International Workshop on Security and Rewriting Techniques, SecReT@ICALP 2006, Venice, Italy, July 15, 2006, volume 171(4) of Electronic Notes in Theoretical Computer Science, pages 73-93. Elsevier, 2006. URL: https://doi.org/10.1016/J.ENTCS.2007.02.056.
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