Towards Quantum Multiparty Session Types

conference
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

November 26, 2024

Doi

10.1007/978-3-031-77382-2_22

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.

Keywords

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

Back to top

Citation

BibTeX citation:
@inproceedings{lanese2024,
  author = {Lanese, Ivan and Dal Lago, Ugo and Choudhury, Vikraman},
  title = {Towards {Quantum} {Multiparty} {Session} {Types}},
  booktitle = {Software Engineering and Formal Methods},
  date = {2024},
  url = {https://doi.org/10.1007/978-3-031-77382-2_22},
  doi = {10.1007/978-3-031-77382-2_22},
  langid = {en},
  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.}
}
For attribution, please cite this work as:
Lanese, Ivan, Ugo Dal Lago, and Vikraman Choudhury. 2024. “Towards Quantum Multiparty Session Types.” Software Engineering and Formal Methods, accepted. https://doi.org/10.1007/978-3-031-77382-2_22.