POPL 2025 (series) / PLanQC 2025 (series) / PLanQC 2025 / Towards Quantum Multiparty Session Types
Towards Quantum Multiparty Session TypesTalk
Multiparty Session Types (MPSTs) are a typing discipline for message-passing protocols that guarantee communication safety properties, such as deadlock-freedom. We propose a quantum extension of MPSTs, called Quantum MPSTs (QMPSTs), with the aim of specifying quantum protocols. QMPSTs guarantee usual communication safety properties, in addition to safety properties specific to quantum information, such as no-cloning and no-deleting. We exhibit the use of QMPSTs to verify Quantum Teleportation. The full paper (to appear in SEFM’24 proceedings) with complete details, metatheoretic results, and examples of other quantum protocols is available at: https://arxiv.org/abs/2409.11133.