pith. sign in

arxiv: 2605.23633 · v1 · pith:JG2Q5B3Snew · submitted 2026-05-22 · 💻 cs.LO

Formally Verified Liveness with Multiparty Session Types in Rocq

Omer Keskin , Nobuko Yoshida , Rob van Glabbeek This is my paper

Pith reviewed 2026-05-25 02:58 UTC · model grok-4.3

classification 💻 cs.LO
keywords multiparty session typeslivenessformal verificationRocqcoinductionprojectionsubtypingsafety
0
0 comments X

The pith

An association relation between coinductive local type contexts and global types proves safety and liveness for multiparty sessions in Rocq.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper mechanizes the top-down approach to multiparty session types, where a global type is projected to local types for each participant. It defines coinductive relations for subtyping on local types and plain-merge projection linking locals to globals, then builds an association between collections of local types and global types. Using this association, it establishes an operational correspondence and proves that associated contexts yield safe and live sessions. This provides the first Rocq-certified guarantee of liveness for synchronous multiparty sessions and allows certification of protocol properties.

Core claim

We represent global and local types as coinductive trees, define coinductive subtyping and plain-merge projection, associate local type contexts with global types via these relations, prove operational correspondence between them, and then prove safety and liveness of the associated local type contexts and the multiparty sessions they type.

What carries the argument

The association relation between local type contexts and global types, constructed from coinductive subtyping and plain-merge projection.

If this is right

  • Typed multiparty sessions possess safety and liveness.
  • Liveness properties of communication protocols can be certified in Rocq.
  • The mechanization clarifies informal proofs in the multiparty session types literature.
  • Around 14K lines of Rocq code formalize the relations and proofs.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same association technique might extend to proving additional properties such as termination or fairness in sessions.
  • Certified local types could serve as verified specifications for implementing communication libraries in verified languages.
  • Mechanized liveness could support automated checking of protocol descriptions before deployment in distributed systems.

Load-bearing premise

The coinductive definitions of global types, local types, subtyping, and plain-merge projection match the informal notions of liveness used in the multiparty session types literature.

What would settle it

A concrete multiparty protocol whose global type projects to local types that satisfy the association relation in Rocq yet the running session deadlocks or violates liveness under the standard operational semantics.

read the original abstract

Multiparty session types (MPST) offer a framework for the description of communication-based protocols involving multiple participants. In the top-down approach to MPST, the communication pattern of the session is described using a global type. Then the global type is projected on to a local type for each participant, and the individual processes making up the session are type-checked against these projections. Typed sessions possess certain desirable properties such as safety, deadlock-freedom and liveness. In this work, we present the first mechanised proof of liveness for synchronous multiparty session types in the Rocq Proof Assistant. Building on recent work, we represent global and local types as coinductive trees using the paco library. We use a coinductively defined subtyping relation on local types together with another coinductively defined plain-merge projection relation relating local and global types. We then associate collections of local types, or local type contexts, with global types using this projection and subtyping relations, and prove an operational correspondence between a local type context and its associated global type. We utilise this association relation to prove the safety and liveness of associated local type contexts and, consequently, the multiparty sessions typed by these contexts. Besides clarifying the often informal proofs found in the MPST literature, our Rocq mechanisation also enables the certification of liveness properties of communication protocols. Our contribution amounts to around 14K lines of Rocq code, available at https://github.com/omerskeskin/mpstlive .

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper presents the first mechanized proof of liveness for synchronous multiparty session types (MPST) in Rocq. Global and local types are represented as coinductive trees using the paco library. A coinductively defined subtyping relation on local types and a plain-merge projection relation are used to associate local type contexts with global types. An operational correspondence is proved between associated contexts and global types, from which safety and liveness of the contexts (and thus of typed multiparty sessions) are derived. The development comprises ~14K lines of Rocq code with an accompanying GitHub artifact.

Significance. If correct, the result supplies the first machine-checked liveness guarantees for synchronous MPST, moving beyond the informal arguments common in the literature. The use of a self-contained coinductive development with paco, together with the public artifact, allows direct inspection of the definitions and proofs; this strengthens the reliability of the safety and liveness claims and supports certification of concrete protocols.

minor comments (2)
  1. The abstract and introduction would benefit from an explicit early statement of the precise coinductive definition of liveness that is being mechanized (currently only referenced via the association relation).
  2. Figure or table summarizing the main Rocq lemmas (operational correspondence, safety, liveness) and their dependencies would improve readability of the 14K-line development.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive review, accurate summary of our contribution, and recommendation to accept the paper. We are pleased that the mechanized proof of liveness for synchronous MPST in Rocq, along with the public artifact, is viewed as strengthening the reliability of the safety and liveness claims.

Circularity Check

0 steps flagged

No significant circularity; self-contained mechanized derivation

full rationale

The paper's central contribution is a complete Rocq mechanization (~14K LOC) of an association relation between local-type contexts and global types, defined via explicitly coinductive subtyping and plain-merge projection relations, followed by operational correspondence, safety, and liveness theorems. All steps are proved inside Rocq against the stated coinductive definitions using the paco library; no parameters are fitted, no results are renamed as predictions, and no load-bearing premise reduces to a self-citation or self-definition. The mechanized theorems constitute the derivation chain itself and are externally inspectable via the artifact. The weakest assumption (fidelity of coinductive encodings to informal MPST notions) is a modeling choice, not a circular reduction.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The development rests on standard coinductive reasoning and the paco library; no free parameters are introduced and no new entities are postulated.

axioms (2)
  • domain assumption Coinductive definitions of global and local types as trees are faithful to the informal MPST syntax and semantics.
    Invoked when representing types and defining the projection and subtyping relations.
  • standard math The paco library correctly implements coinductive reasoning in Rocq.
    Used throughout the mechanization for coinductive predicates.

pith-pipeline@v0.9.0 · 5809 in / 1366 out tokens · 19189 ms · 2026-05-25T02:58:21.116345+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

65 extracted references · 65 canonical work pages

  1. [1]

    doi:https://doi.org/10.46298/lmcs-21(2:5)2025

    Adam Barwell and Ping Hou and Nobuko Yoshida and Fangyi Zhou , title =. doi:https://doi.org/10.46298/lmcs-21(2:5)2025

    work page doi:10.46298/lmcs-21(2:5)2025 2025

  2. [2]

    Theoretical Computer Science , publisher =

    Nobuko Yoshida and Ping Hou and Iona Kuhn , title =. Theoretical Computer Science , publisher =

    work page

  3. [3]

    Components Operationally: Reversibility and System Engineering , series =

    Kai Pischke and Nobuko Yoshida , title =. Components Operationally: Reversibility and System Engineering , series =

    work page

  4. [4]

    A Very Gentle Introduction to Multiparty Session Types , year =

    Yoshida, Nobuko and Gheri, Lorenzo , booktitle =. A Very Gentle Introduction to Multiparty Session Types , year =

    work page

  5. [5]

    2002 , publisher=

    Types and programming languages , author=. 2002 , publisher=

    work page 2002

  6. [6]

    Stuttering for Free , year =

    Cho, Minki and Song, Youngju and Lee, Dongjae and G\". Stuttering for Free , year =. Proc. ACM Program. Lang. , month = oct, articleno =. doi:10.1145/3622857 , abstract =

    work page doi:10.1145/3622857

  7. [7]

    Fundamenta Informaticae , volume =

    Paula Severi and Mariangiola Dezani-Ciancaglini , title =. Fundamenta Informaticae , volume =. 2019 , doi =

    work page 2019

  8. [8]

    Chappe, Nicolas , title =. Proc. ACM Program. Lang. , month = jan, articleno =. 2026 , issue_date =. doi:10.1145/3776714 , abstract =

    work page doi:10.1145/3776714 2026

  9. [9]

    2011 , publisher=

    Introduction to bisimulation and coinduction , author=. 2011 , publisher=

    work page 2011

  10. [10]

    Precise subtyping for synchronous multiparty sessions , volume =

    Silvia Ghilezan and Svetlana Jak. Precise subtyping for synchronous multiparty sessions , volume =. Journal of Logical and Algebraic Methods in Programming , keywords =. 2019 , bdsk-url-1 =. doi:https://doi.org/10.1016/j.jlamp.2018.12.002 , issn =

    work page doi:10.1016/j.jlamp.2018.12.002 2019

  11. [11]

    Scalas, Alceste and Yoshida, Nobuko , title =. Proc. ACM Program. Lang. , month = jan, articleno =. 2019 , issue_date =. doi:10.1145/3290343 , abstract =

    work page doi:10.1145/3290343 2019

  12. [12]

    Less is More Revisited

    Yoshida, Nobuko and Hou, Ping. Less is More Revisited. The Practice of Formal Methods: Essays in Honour of Cliff Jones, Part II. 2024. doi:10.1007/978-3-031-66673-5_14

    work page doi:10.1007/978-3-031-66673-5_14 2024

  13. [13]

    Formal Models and Semantics , publisher =

    Operational and Algebraic Semantics of Concurrent Processes , editor =. Formal Models and Semantics , publisher =. 1990 , series =. doi:https://doi.org/10.1016/B978-0-444-88074-1.50024-X , author =

    work page doi:10.1016/b978-0-444-88074-1.50024-x 1990

  14. [14]

    Padovani, Luca , title =. Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) , articleno =. 2014 , isbn =. doi:10.1145/2603088.2603116 , abstract =

    work page doi:10.1145/2603088.2603116 2014

  15. [15]

    16th International Conference on Interactive Theorem Proving (ITP 2025) , pages =

    Li, Elaine and Wies, Thomas , title =. 16th International Conference on Interactive Theorem Proving (ITP 2025) , pages =. 2025 , volume =. doi:10.4230/LIPIcs.ITP.2025.15 , annote =

    work page doi:10.4230/lipics.itp.2025.15 2025

  16. [16]

    Subtyping Supports Safe Session Substitution

    Gay, Simon J. Subtyping Supports Safe Session Substitution. A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday. 2016. doi:10.1007/978-3-319-30936-1_5

    work page doi:10.1007/978-3-319-30936-1_5 2016

  17. [17]

    Acta Informatica , author =

    Reversible sessions with flexible choices , volume =. Acta Informatica , author =. 2019 , pages =. doi:10.1007/s00236-019-00332-y , abstract =

    work page doi:10.1007/s00236-019-00332-y 2019

  18. [18]

    Composition and decomposition of multiparty sessions , journal =

    Franco Barbanera and Mariangiola Dezani-Ciancaglini and Ivan Lanese and Emilio Tuosto , abstract =. Composition and decomposition of multiparty sessions , journal =. 2021 , issn =. doi:https://doi.org/10.1016/j.jlamp.2020.100620 , url =

    work page doi:10.1016/j.jlamp.2020.100620 2021

  19. [19]

    Partially typed multiparty sessions with internal delegation , journal =

    Franco Barbanera and Viviana Bono and Mariangiola Dezani-Ciancaglini , keywords =. Partially typed multiparty sessions with internal delegation , journal =. 2025 , issn =. doi:https://doi.org/10.1016/j.jlamp.2024.101018 , url =

    work page doi:10.1016/j.jlamp.2024.101018 2025

  20. [20]

    Electronic Proceedings in Theoretical Computer Science , author =

    Partially. Electronic Proceedings in Theoretical Computer Science , author =. 2023 , NOnote =. doi:10.4204/EPTCS.383.2 , abstract =

    work page doi:10.4204/eptcs.383.2 2023

  21. [21]

    Information and Computation , author =

    A. Information and Computation , author =. 2002 , pages =. doi:10.1006/inco.2002.3171 , abstract =

    work page doi:10.1006/inco.2002.3171 2002

  22. [22]

    Journal of Logical and Algebraic Methods in Programming , author =

    Fair termination of multiparty sessions , volume =. Journal of Logical and Algebraic Methods in Programming , author =. 2024 , keywords =. doi:https://doi.org/10.1016/j.jlamp.2024.100964 , abstract =

    work page doi:10.1016/j.jlamp.2024.100964 2024

  23. [23]

    39th European Conference on Object-Oriented Programming (ECOOP 2025) , pages =

    Tirore, Dawit and Bengtson, Jesper and Carbone, Marco , title =. 39th European Conference on Object-Oriented Programming (ECOOP 2025) , pages =. 2025 , volume =. doi:10.4230/LIPIcs.ECOOP.2025.31 , annote =

    work page doi:10.4230/lipics.ecoop.2025.31 2025

  24. [24]

    Asynchronous Global Protocols, Precisely

    Pischke, Kai and Yoshida, Nobuko. Asynchronous Global Protocols, Precisely. Components Operationally: Reversibility and System Engineering: Essays Dedicated to Jean-Bernard Stefani on the Occasion of His 65th Birthday. 2026. doi:10.1007/978-3-031-99717-4_7

    work page doi:10.1007/978-3-031-99717-4_7 2026

  25. [25]

    A Sound and Complete Projection for Global Types , booktitle =

    Dawit Legesse Tirore and Jesper Bengtson and Marco Carbone , editor =. A Sound and Complete Projection for Global Types , booktitle =. 2023 , doi =

    work page 2023

  26. [26]

    A Mechanisation of Multiparty Session Types

    Dawit Tirore. A Mechanisation of Multiparty Session Types. 2024

    work page 2024

  27. [27]

    Castro-Perez, David and Ferreira, Francisco and Jongmans, Sung-Shik , title =. Proc. ACM Program. Lang. , month = jan, articleno =. 2026 , issue_date =. doi:10.1145/3776692 , abstract =

    work page doi:10.1145/3776692 2026

  28. [28]

    2023 , eprint=

    Concerto Grosso for Sessions: Fair Termination of Sessions , author=. 2023 , eprint=

    work page 2023

  29. [29]

    Computer Science , author =

    Type-driven. Computer Science , author =. doi:10.7494/csci.2017.18.3.1413 , number =

    work page doi:10.7494/csci.2017.18.3.1413 2017

  30. [30]

    Proceedings of the 14th ACM SIGPLAN International Symposium on Haskell , pages =

    Kokke, Wen and Dardha, Ornela , title =. Proceedings of the 14th ACM SIGPLAN International Symposium on Haskell , pages =. 2021 , isbn =. doi:10.1145/3471874.3472979 , abstract =

    work page doi:10.1145/3471874.3472979 2021

  31. [31]

    Embedding session types in

    Lindley, Sam and Morris, J Garrett , journal=. Embedding session types in. 2016 , publisher=

    work page 2016

  32. [32]

    Proceedings of the first ACM SIGPLAN symposium on Haskell , pages=

    Haskell session types with (almost) no class , author=. Proceedings of the first ACM SIGPLAN symposium on Haskell , pages=. 2008 , doi=

    work page 2008

  33. [33]

    Proceedings of the ACM on Programming Languages , volume=

    Actris: Session-type based reasoning in separation logic , author=. Proceedings of the ACM on Programming Languages , volume=. 2019 , publisher=

    work page 2019

  34. [34]

    Journal of Functional Programming , volume=

    Iris from the ground up: A modular foundation for higher-order concurrent separation logic , author=. Journal of Functional Programming , volume=. 2018 , doi=

    work page 2018

  35. [35]

    Proceedings of the ACM on Programming Languages , volume=

    Deadlock-free separation logic: Linearity yields progress for dependent higher-order message passing , author=. Proceedings of the ACM on Programming Languages , volume=. 2024 , publisher=

    work page 2024

  36. [36]

    Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming , pages =

    Wadler, Philip , title =. Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming , pages =. 2012 , isbn =. doi:10.1145/2364527.2364568 , abstract =

    work page doi:10.1145/2364527.2364568 2012

  37. [37]

    SIGPLAN Not

    Wadler, Philip , title =. SIGPLAN Not. , month = sep, pages =. 2012 , issue_date =. doi:10.1145/2398856.2364568 , abstract =

    work page doi:10.1145/2398856.2364568 2012

  38. [38]

    Multiparty

    Jacobs, Jules and Balzer, Stephanie and Krebbers, Robbert , journal=. Multiparty. 2022 , publisher=

    work page 2022

  39. [39]

    Lee, Dongjae and Cho, Minki and Kim, Jinwoo and Moon, Soonwon and Song, Youngju and Hur, Chung-Kil , title =. Proc. ACM Program. Lang. , month = jun, articleno =. 2023 , issue_date =. doi:10.1145/3591253 , abstract =

    work page doi:10.1145/3591253 2023

  40. [40]

    ACM Trans

    D’Osualdo, Emanuele and Sutherland, Julian and Farzan, Azadeh and Gardner, Philippa , title =. ACM Trans. Program. Lang. Syst. , month = nov, articleno =. 2021 , issue_date =. doi:10.1145/3477082 , abstract =

    work page doi:10.1145/3477082 2021

  41. [41]

    Proceedings of the ACM on Programming Languages , volume=

    Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness , author=. Proceedings of the ACM on Programming Languages , volume=. 2025 , doi=

    work page 2025

  42. [42]

    Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming , articleno =

    Thiemann, Peter , title =. Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming , articleno =. 2019 , isbn =. doi:10.1145/3354166.3354184 , abstract =

    work page doi:10.1145/3354166.3354184 2019

  43. [43]

    Completeness of

    Ekici, Burak and Yoshida, Nobuko , editor =. Completeness of. 15th. 2024 , note =. doi:10.4230/LIPIcs.ITP.2024.13 , urldate =

    work page doi:10.4230/lipics.itp.2024.13 2024

  44. [44]

    Generalizing

    Ancona, Davide and Dagnino, Francesco and Zucca, Elena , editor =. Generalizing. Programming. 2017 , pages =

    work page 2017

  45. [45]

    Ciccone, Luca and Padovani, Luca , title =. Proc. ACM Program. Lang. , month = jan, articleno =. 2022 , issue_date =. doi:10.1145/3498666 , abstract =

    work page doi:10.1145/3498666 2022

  46. [46]

    Padovani, Luca and Vasconcelos, Vasco Thudichum and Vieira, Hugo Torres , editor =. Typing. Coordination. 2014 , doi=

    work page 2014

  47. [47]

    16th International Conference on Interactive Theorem Proving (ITP 2025) , pages =

    Ekici, Burak and Kamegai, Tadayoshi and Yoshida, Nobuko , title =. 16th International Conference on Interactive Theorem Proving (ITP 2025) , pages =. 2025 , volume =. doi:10.4230/LIPIcs.ITP.2025.19 , annote =

    work page doi:10.4230/lipics.itp.2025.19 2025

  48. [48]

    2013 , issue_date =

    Hur, Chung-Kil and Neis, Georg and Dreyer, Derek and Vafeiadis, Viktor , title =. 2013 , issue_date =. doi:10.1145/2480359.2429093 , journal =

    work page doi:10.1145/2480359.2429093 2013

  49. [49]

    Letouzey, Pierre and Appel, Andrew W. , url=

    work page

  50. [50]

    and Leiserson, Charles E

    Cormen, Thomas H. and Leiserson, Charles E. and Rivest, Ronald L. and Stein, Clifford , title =. 2009 , isbn =

    work page 2009

  51. [51]

    2025 , organization =

    work page 2025

  52. [52]

    2013 , isbn =

    Chlipala, Adam , title =. 2013 , isbn =. doi:10.7551/mitpress/9153.001.0001 , abstract =

    work page doi:10.7551/mitpress/9153.001.0001 2013

  53. [53]

    Progress, Justness, and Fairness , volume=

    Glabbeek, Rob van and Höfner, Peter , year=. Progress, Justness, and Fairness , volume=. ACM Computing Surveys , publisher=. doi:10.1145/3329125 , number=

    work page doi:10.1145/3329125

  54. [54]

    Fairness , copyright =

    Francez, Nissim , year =. Fairness , copyright =. doi:10.1007/978-1-4612-4886-6 , keywords =

    work page doi:10.1007/978-1-4612-4886-6

  55. [55]

    2008 , isbn =

    Baier, Christel and Katoen, Joost-Pieter , title =. 2008 , isbn =

    work page 2008

  56. [56]

    18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 1977 , pages =

    Amir Pnueli , title =. 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 1977 , pages =. 1977 , doi =

    work page 1977

  57. [57]

    1999 , isbn =

    Milner, Robin , title =. 1999 , isbn =

    work page 1999

  58. [58]

    In: POPL (2008)

    Honda, Kohei and Yoshida, Nobuko and Carbone, Marco , title =. Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages , pages =. 2008 , isbn =. doi:10.1145/1328438.1328472 , abstract =

    work page doi:10.1145/1328438.1328472 2008

  59. [59]

    SIGPLAN Not

    Honda, Kohei and Yoshida, Nobuko and Carbone, Marco , title =. SIGPLAN Not. , month = jan, pages =. 2008 , issue_date =. doi:10.1145/1328897.1328472 , abstract =

    work page doi:10.1145/1328897.1328472 2008

  60. [60]

    ACM Transactions on Programming Languages and Systems (TOPLAS) , volume=

    Proving liveness properties of concurrent programs , author=. ACM Transactions on Programming Languages and Systems (TOPLAS) , volume=. 1982 , publisher=

    work page 1982

  61. [61]

    2010 , isbn =

    Bertot, Yves and Castran, Pierre , title =. 2010 , isbn =

    work page 2010

  62. [62]

    Top-down or bottom-up?

    Udomsrirungruang, Thien and Yoshida, Nobuko , journal=. Top-down or bottom-up?. 2025 , publisher=

    work page 2025

  63. [63]

    In: 2021 36th Annual ACM/IEEE Sym- posium on Logic in Computer Science (LICS)

    Glabbeek, Rob van and H\". Assuming just enough fairness to make session types complete for lock-freedom , year =. Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science , articleno =. doi:10.1109/LICS52264.2021.9470531 , abstract =

    work page doi:10.1109/lics52264.2021.9470531 2021

  64. [64]

    Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation , pages =

    Castro-Perez, David and Ferreira, Francisco and Gheri, Lorenzo and Yoshida, Nobuko , title =. Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation , pages =. 2021 , isbn =. doi:10.1145/3453483.3454041 , abstract =

    work page doi:10.1145/3453483.3454041 2021

  65. [65]

    Filters on CoInductive Streams, an Application to Eratosthenes' Sieve

    Bertot, Yves. Filters on CoInductive Streams, an Application to Eratosthenes' Sieve. Typed Lambda Calculi and Applications. 2005

    work page 2005