POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States

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.