Towards Quantum Multiparty Session Types

TL;DR

This paper introduces Quantum Multiparty Session Types (QMPSTs), a formal framework for specifying and verifying quantum communication protocols that ensure properties like deadlock-freedom and qubit ownership.

Contribution

It extends classical MPSTs with quantum data and operations, enabling formal specification, type-checking, and verification of quantum protocols.

Findings

Successfully verified four quantum protocols: Teleportation, Secret Sharing, Bit-Commitment, and Key Distribution.

Ensured qubits are owned by a single process at any time, respecting quantum no-cloning and no-deleting theorems.

Provided a formal notation for describing quantum protocols at both global and local levels.

Abstract

Multiparty Session Types (MPSTs) offer a structured way of specifying communication protocols and guarantee relevant communication properties, such as deadlock-freedom. In this paper, we extend a minimal MPST system with quantum data and operations, enabling the specification of quantum protocols. Quantum MPSTs (QMPSTs) provide a formal notation to describe quantum protocols, both at the abstract level of global types, describing which communications can take place in the system and their dependencies, and at the concrete level of local types and quantum processes, describing the expected behavior of each participant in the protocol. Type-checking relates these two levels formally, ensuring that processes behave as prescribed by the global type. Beyond usual communication properties, QMPSTs also allow us to prove that qubits are owned by a single process at any time, capturing the quantum no-cloning and no-deleting theorems. We use our approach to verify four quantum protocols from the literature, respectively Teleportation, Secret Sharing, Bit-Commitment, and Key Distribution.