Towards Quantum Multiparty Session Types

workshop
Linear Types
Multiparty Session Types
Quantum Computing
Quantum Processes
Quantum Protocols
Authors
Affiliation

Ivan Lanese

Università di Bologna, Bologna, Italy

Ugo Dal Lago

Università di Bologna, Bologna, Italy

Vikraman Choudhury

Università di Bologna, Bologna, Italy

Published

January 1, 2025

Abstract

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 QMP-STs 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 arXiv:2409.11133 [Lanese et al. 2024].

Keywords

Linear Types, Multiparty Session Types, Quantum Computing, Quantum Processes, Quantum Protocols

Back to top

Citation

BibTeX citation:
@inproceedings{lanese2025,
  author = {Lanese, Ivan and Dal Lago, Ugo and Choudhury, Vikraman},
  title = {Towards {Quantum} {Multiparty} {Session} {Types}},
  booktitle = {Fifth International Workshop on Programming Languages for
    Quantum Computing (PLanQC 2025)},
  date = {2025},
  url = {https://vikraman.org/papers/lanese-lago-choudhury-2025a/},
  langid = {en},
  abstract = {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 QMP-STs 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
    arXiv:2409.11133 {[}Lanese et al. 2024{]}.}
}
For attribution, please cite this work as:
Lanese, Ivan, Ugo Dal Lago, and Vikraman Choudhury. 2025. “Towards Quantum Multiparty Session Types.” Fifth International Workshop on Programming Languages for Quantum Computing (PLanQC 2025), accepted. https://vikraman.org/papers/lanese-lago-choudhury-2025a/.