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 .

翻译：多方会话类型（MPST）为描述涉及多个参与者的基于通信的协议提供了一种框架。在MPST的自顶向下方法中，会话的通信模式使用全局类型来描述。然后，全局类型被投影为每个参与者的局部类型，组成会话的各个进程将根据这些投影进行类型检查。经过类型检查的会话具有某些理想属性，例如安全性、无死锁性和活性。在这项工作中，我们在Rocq证明助手中提出了首个针对同步多方会话类型活性的机械化证明。基于近期的研究，我们使用paco库将全局类型和局部类型表示为共归纳树。我们在局部类型上使用共归纳定义的子类型关系，以及另一个共归纳定义的、关联局部类型与全局类型的plain-merge投影关系。然后，我们将局部类型的集合（或称局部类型上下文）与全局类型通过这种投影和子类型关系关联起来，并证明了局部类型上下文与其关联全局类型之间的操作对应关系。我们利用这种关联关系来证明关联的局部类型上下文的安全性及活性，进而证明由这些上下文进行类型检查的多方会话的相应属性。除了澄清MPST文献中通常不够正式的证明外，我们的Rocq机械化实现还支持对通信协议活性属性的认证。我们的贡献约为14,000行Rocq代码，代码位于https://github.com/omerskeskin/mpstlive。