Multiparty Dependent Session Types (Extended Abstract)

TL;DR

This paper introduces the first formal multiparty dependent session types, providing a practical type discipline for verifying communication protocols in distributed and concurrent programs, ensuring deadlock-freeness and communication fidelity.

Contribution

It formalizes multiparty dependent session types within a multi-threaded lambda calculus, inspired by multirole logic, and proves their soundness through a novel deadlock-freeness reducibility technique.

Findings

Proves communication fidelity and deadlock-freeness of the type system.

Formalizes a new expressive type discipline for distributed programs.

Demonstrates soundness via a novel proof technique.

Abstract

Programs are more distributed and concurrent today than ever before, and structural communications are at the core. Constructing and debugging such programs are hard due to the lack of formal specification/verification of concurrency. This work formalizes the first multiparty dependent session types as an expressive and practical type discipline for enforcing communication protocols. The type system is formulated in the setting of multi-threaded $\lambda$-calculus with inspirations from multirole logic, a generalization of classical logic we discovered earlier. We prove its soundness by a novel technique called deadlock-freeness reducibility. The soundness of the type system implies communication fidelity and absence of deadlock.