# Towards Quantum Multiparty Session Types

Ivan Lanese, Ugo Dal Lago, Vikraman Choudhury

► To cite this version:

Ivan Lanese, Ugo Dal Lago, Vikraman Choudhury. Towards Quantum Multiparty Session Types. SEFM 2024 - 22nd International Conference on Software Engineering and Formal Methods, Nov 2024, Aveiro (Portugal), Portugal. pp.385-403, 10.1007/978-3-031-77382-2_22. hal-04832740

HAL Id: hal-04832740

https://inria.hal.science/hal-04832740v1

Submitted on 12 Dec 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
<figure><img src="image_2.png" /></figure>

# Towards Quantum Multiparty Session Types

Ivan Lanese(✉)ID, Ugo Dal Lago(✉)ID, and Vikraman Choudhury(✉)ID

OLAS Team, University of Bologna and INRIA, Bologna, Italy
{ivan.lanese,vikraman.choudhury}@gmail.com, ugo.dallago@unibo.it

**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:** Multiparty Session Types · Linear Types · Quantum Protocols · Quantum Processes · Quantum Computing

## 1 Introduction

Quantum protocols involve the exchange of (quantum) information between multiple parties in (quantum) networks, giving rise to complex interaction patterns, interleaved with manipulations of quantum states. This raises the need for tools and techniques to specify, analyse, and verify such protocols. However, while many languages, notations, and formal calculi exist to describe quantum circuits, fewer options exist for formally describing quantum multiparty protocols (see the discussion in the recent systematic survey [15]). In fact, there does

<footnote>Partially supported by the EU Marie Skłodowska-Curie action ReGraDe-CS (№: 101106046), by French ANR project SmartCloud ANR-23-CE25-0012, by INdAM - GNCS 2024 project MARVEL, code CUP E53C23001670001, and by the Italian Ministry of University and Research under PNRR - M4C2 - I1.4 Project CN00000013 "National Centre for HPC, Big Data and Quantum Computing".</footnote>

<footnote>© The Author(s), 2025</footnote>

<footnote>A. Madeira and A. Knapp (Eds.): SEFM 2024, LNCS 15280, pp. 385–403, 2025.</footnote>

<footnote>https://doi.org/10.1007/978-3-031-77382-2_22</footnote>
not exist a mainstream formal way to describe quantum protocols. This is wit-
nessed by the fact that the Quantum Protocol Zoo [32], a well-known library of
quantum protocols, relies on natural language—hence ambiguous—descriptions,
paired with Python implementations.

Existing formalisms for quantum protocols include imperative languages such as LanQ [27] and QMCLANG [14,29], and process calculi such as CQP [16], CCSq [2] and lqCCS [10]. The former do not allow for an abstract representation of the protocol, while the latter are not easy to understand (see the discussion in Sect. 6 for details). The analysis in [16] on the shortcomings of their CQP approach reports: “The proliferation of channels is a consequence of the fact that our type system associates a unique type with each channel. Introducing session types would allow a single channel to be used for the entire protocol”.

Following this hint in [16], we propose a quantum extension to Multiparty Session Types (MPSTs) [22,24], dubbed Quantum MPSTs (QMPSTs), as a formal session-typed language to describe quantum protocols. QMPSTs provide both an abstract view—the *global type*, and a concrete view—a multiparty system made of named *quantum processes*. The global type describes the expected pattern of interactions from a global viewpoint, clarifying which communications take place, between which participants, and in which order. QMPST processes describe the sequence of actions taken by each participant inside the protocol, including quantum actions such as the application of unitary transformations or the measurement of qubits. The two views are formally related—*type checking* ensures that processes actually behave as prescribed by the global type (Theorem 3). The framework of MPSTs also ensures relevant communication properties by construction, such as progress (Theorem 5). Further, in our approach, messages will directly target participants, denoted by their name, avoiding the proliferation of channels (as in CQP), and clarifying the expected sender and receiver of each message (cf. Example 5).

***Outline and Contributions.*** The main contribution of this paper is a novel
framework for specifying quantum protocols using MPSTs, building on classi-
cal approaches, but extending them with quantum features. There is no other
extension of MPSTs for quantum protocols in the literature, to the best of our
knowledge.

- In Sect. 2, we introduce our calculus for QMPSTs. At the level of types, the main novelty is that data include references to qubits, and such references need to be treated in a linear way (cf. Theorem 7) due to the no-cloning and no-deleting theorems [34] of quantum computing. At the level of processes, as mentioned before, we introduce quantum operations such as unitary transformations and measurement.

- In Sect. 3, we provide a concrete operational semantics for QMPSTs. We define a labelled transition system for quantum multiparty systems, that is both non-deterministic and probabilistic, to account for multiparty system communication, and the probabilistic nature of quantum measurements.
- In Sect. 4, we establish meta-theoretical results for our calculus. We prove the usual communication safety properties of MPSTs, namely, subject reduction (Theorem 3), session fidelity (Theorem 4), progress (Theorem 5), and type safety (Theorem 6), and quantum safety properties, namely, unique ownership of qubits (Theorem 7) and qubit safety (Theorem 8).

- In Sect. 5, we show the expressive power and clarity of our approach by applying it to four quantum protocols from the literature, namely Teleportation (used as a running example), Secret Sharing (Example 5, in Sect. 5), Bit-Commitment (Example 6, in Sect. 5), and Key Distribution (see technical report [26]).

We remark that some familiarity with quantum computing is needed to understand the paper—for standard notions, we refer to [28]. For details of proofs, auxiliary results, and additional examples, we refer the reader to the extended technical report [26].

## 2 Type System

We start from a minimal MPSTs paradigm (such as the one in [35]) to avoid clustering the work with technicalities that are not related to the interplay between MPSTs and quantum computing and which would spoil the cleanliness of the language. This approach is also useful in understanding which advanced features of MPSTs are useful in the quantum setting, and which ones are unnecessary.

We follow the usual top-down approach to MPSTs, whereby we first give a global type describing the interactions in the system from a global point of view. We then project the global type into local types, describing the required behavior of each participant. Local types are used to type check the processes describing participants. The main novelty of our type system is that basic types include qubits (qbit), and qubit variables are treated linearly.

Amongst the common features in approaches to MPSTs (such as [22,30]), we drop support for multiple sessions and delegation, and only use a single channel. These features are not useful for our case studies in Sect. 5, nor in other examples of quantum protocols we have looked at (see, e.g., the library of quantum protocols mentioned above [32]). The most important feature of MPSTs that we use is the notion of internal and external choice (or send and receive, respectively), and selection and branching constructs in processes, which allows processes to exchange both classical and quantum data. Hence, following Selinger’s famous slogan “quantum data + classical control” for quantum lambda-calculus [31], the slogan for our quantum process calculus is “quantum data + classical control + classical choice”.

We first define the syntax of types. In the following definition, $(q_i)_{i \in I}$ and $\{q_i\}_{i \in I}$ denote indexed tuples and indexed sets, respectively. We also denote tuples as $\tilde{q}$, leaving the indexing implicit. We also write $x:B$ to mean a tuple $\tilde{x}$ of typed variables, each of type $B$.
<figure><img src="image_3.png" /><figcaption>Fig. 1. Syntax of types.</figcaption></figure>

**Definition 1 (Syntax of Types).** The syntax of global types, local types, and basic types, ranged over respectively by *G*, *T* and *B*, is defined in Fig. 1, where *p*, *q* are participants (or roles) and *l*<sub>*i*</sub> denote labels. Labels in a global type are assumed to be disjoint, and label sets are non-empty. Basic types include at least **bits**, **unit**, integers, and references to qubits.

In choices we may drop braces when the index set is a singleton. References to qubits are needed since, due to entanglement, allowing values of distinct qubits to be related (indeed measuring one of them may impact the value of the other), it is not possible to provide separate descriptions of single qubits. Following [13, 31], we hence rely on a global qubit register, abstracting away from the actual physical location of the qubits, to describe the whole quantum state of a system. References are pointers (or names) to quantum states inside this register.

Labels are used as usual to communicate which branch is taken in a choice. We drop labels when the choice has a single branch, and the type of it, if it is **unit**. Global recursive types are contractive, that is, each occurence of the recursive type variable inside the body of the recursive definition is guarded. We also assume the equi-recursive equation: $\mu t.G = G\{\mu t.G/t\}$ holds.

*Example 1 (Quantum Teleportation [2, Fig. 14] - Description and Global Type).* The quantum teleportation protocol [7] allows one to transmit a quantum state via a non-quantum medium. A slightly different version of the protocol is reported in [16, Fig. 5] under the name of “Quantum teleportation with EPR source”.

In order to more easily model the example we extend our data types with *n*-uples of bits, denoted **bit**<sup>*n*</sup>. We can then write the global type below. We use a dedicated participant called **Env**, for environment, where other participants can take input from and send output to. This avoids the need for specific input and output primitives as in [2].

$$
G = \text{Env} \to \text{Alice} : (\text{qbit}) . \text{Source} \to \text{Alice} : (\text{qbit}) . \text{Source} \to \text{Bob} : (\text{qbit}) . \\
\text{Alice} \to \text{Bob} : (\text{bit}^2) . \text{Bob} \to \text{Env} : (\text{qbit}) . \text{end}
$$

The idea is that **Alice** takes a **qbit** from **Env**, and wants to send it to **Bob** via a classical communication channel (indeed **Alice** only sends to **Bob** two classical
**bits**). Bob can then give the **qbit** to Env. In order to do so, **Alice** and **Bob** take from some **Source** two entangled qubits.
◇

The set of roles or participants in a global type $G$ is given by $pt(G)$:

$$ 
\begin{align*}
pt(\mathbf{p} \to \mathbf{q}: \{\ell_i(B_i) \cdot G_i\}_{i \in I}) &= \{\mathbf{p}, \mathbf{q}\} \cup \bigcup_{i \in I} pt(G_i) \\
pt(\mu \mathbf{t} \cdot G) &= pt(G) \\
pt(\mathbf{t}) &= pt(\mathbf{end}) = \emptyset
\end{align*}
$$

Projection allows one to derive which local type each participant needs to follow in order for their composition to behave as prescribed by the global type. We take the notion of projection below from [30].

**Definition 2 (Global Type Projection).** The projection of a global type $G$ onto a role $\mathbf{p}$, written $G \upharpoonright \mathbf{p}$, is:

$$ (\mathbf{q} \to \mathbf{r}: \{\ell_i(B_i) \cdot G_i\}_{i \in I}) \mid \mathbf{p} = \left\{ \begin{array}{ll} \mathbf{r} \oplus \{\ell_i(B_i) \cdot (G_i \upharpoonright \mathbf{p})\}_{i \in I} & \text{if } \mathbf{p} = \mathbf{q} \\ \mathbf{q} \land \{\ell_i(B_i) \cdot (G_i \upharpoonright \mathbf{p})\}_{i \in I} & \text{if } \mathbf{p} = \mathbf{r} \\ \bigcap_{i \in I} G_i \mid \mathbf{p} & \text{if } \mathbf{p} \neq \mathbf{q} \text{ and } \mathbf{p} \neq \mathbf{r} \end{array} \right. \\ (\mu \mathbf{t} \cdot G) \mid \mathbf{p} = \begin{cases} \mu \mathbf{t} \cdot (G \mid \mathbf{p}) & \text{if } \mathbf{p} \in pt(G) \text{ or } \mathbf{f}v(\mu \mathbf{t} \cdot G) \neq \emptyset \\ \mathbf{end} & \text{otherwise} \end{cases} \quad \begin{array}{l} \mathbf{t} \mid \mathbf{p} = \mathbf{t} \\ \mathbf{end} \mid \mathbf{p} = \mathbf{end} \end{array} $$

where $\bigcap$ is the full-merging operation, defined as:

$$ 
\begin{align*}
\mathbf{p} \oplus \{\ell_i(B_i) \cdot T_i\}_{i \in I} \cap \mathbf{p} \oplus \{\ell_i(B_i) \cdot T'_i\}_{i \in I} &= \mathbf{p} \oplus \{\ell_i(B_i) \cdot (T_i \cap T'_i)\}_{i \in I} \\
\mu \mathbf{t} \cdot T \cap \mu \mathbf{t} \cdot T' &= \mu \mathbf{t} \cdot (T \cap T') \quad \mathbf{t} \cap \mathbf{t} = \mathbf{t} \quad \mathbf{end} \cap \mathbf{end} = \mathbf{end} \\
\mathbf{p} \land \{\ell_i(B_i) \cdot T_i\}_{i \in I} \cap \mathbf{p} \land \{\ell_j(B_j) \cdot T'_j\}_{j \in J} &= \mathbf{p} \land \{\ell_k(B_k) \cdot T''_k\}_{k \in I \cup J} \\
\text{where } T_k'' &= \begin{cases} T_k \cap T_k' & \text{if } k \in I \cap J \\ T_k & \text{if } k \in I \setminus J \\ T_k' & \text{if } k \in J \setminus I \end{cases}
\end{align*}
$$

Intuitively, participants involved in a choice act as prescribed by the choice. Participants which are not involved need either to behave the same in the two branches, or to receive messages with distinct labels telling them how to behave.

**Example 2 (Quantum Teleportation - Local types).** We can obtain the local types by projecting the global type in Example 1 on the different participants:

$$ 
\begin{align*}
G \upharpoonright \text{Alice} &= \text{Env} \oplus (\text{qbit}) \cdot \text{Source} \oplus (\text{qbit}) \cdot \text{Bob} \oplus (\text{bit}^2) \cdot \text{end} \\
G \upharpoonright \text{Bob} &= \text{Source} \oplus (\text{qbit}) \cdot \text{Alice} \oplus (\text{bit}^2) \cdot \text{Env} \oplus (\text{qbit}) \cdot \text{end} \\
G \upharpoonright \text{Source} &= \text{Alice} \oplus (\text{qbit}) \cdot \text{Bob} \oplus (\text{qbit}) \cdot \text{end} \\
G \upharpoonright \text{Env} &= \text{Alice} \oplus (\text{qbit}) \cdot \text{Bob} \oplus (\text{qbit}) \cdot \text{end}
\end{align*}
\diamond $$

A global type is well-formed if it is contractive, and can be projected onto all its roles. We implicitly assume that all global types are well-formed.
$$ \frac{j \in I}{\substack{\mathbf{p} \to \mathbf{q}: \{\ell_i(B_i) \cdot G'_i\}_{i \in I} \\ \mathbf{p} \to \mathbf{q}: \ell_j(B_j) \to G'_j}} \quad [\text{GT-}\oplus\&] \\ \\ \frac{\forall i \in I \ G'_i \xrightarrow{\alpha} G''_i \quad \text{pt}(\alpha) \cap \{\mathbf{p}, \mathbf{q}\} = \emptyset}{\mathbf{p} \to \mathbf{q}: \{\ell_i(B_i) \cdot G'_i\}_{i \in I} \xrightarrow{\alpha} \mathbf{p} \to \mathbf{q}: \{\ell_i(B_i) \cdot G''_i\}_{i \in I}} \quad [\text{GT-CTX}] $$

<caption>Fig. 2. Global type transitions</caption>

**Definition 3 (Global Type Transitions).** The global type transition relation $\xrightarrow{\alpha}$ is defined in Fig. 2. We write $G \to G'$ if there exists $\alpha$ such that $G \xrightarrow{\alpha} G'$. We also write $G \to$ if there exists $G'$ such that $G \to G'$; $\to^*$ denotes the reflexive and transitive closure of $\to$.

Rule GT-⊕& in Fig. 2 just allows one to execute the first interaction. Rule GT-CTx allows one to execute an interaction $\alpha$ available in all the continuations provided that it has disjoint participants from the first one. Sets of local types projected from a global type can be used to type programs. We extend the type system in [2, Fig. 12], which however requires channels to carry uniform values. Like in [16], qubits are treated linearly.

The syntax of systems, processes and expressions is in Fig. 3. We take inspiration from the syntax in [2, Fig. 11], with a few changes to fit MPSTs. First, for us a system is a parallel composition of processes with roles, and, send and receive actions explicitly refer to the target role p. This makes the protocol clearer than using channels, and helps the technical development as well. Then, as customary for session types, we have input choice to allow a participant to wait for several input messages, and accept the first one that arrives. We use labels to clarify which branch of a choice is selected. Finally, we avoid the input/output constructs in [2, Fig. 11] (we model them as interactions with some Environment role, as done in our running example).

We assume a set $\mathcal{V}$ for variables, which may contain either classical values, or references to the qubit register which contains actual quantum information. We assume that operators in expressions only work on classical data, operations on qbits are explicitly modeled as unitary operations. We assume to have a library of unitary operations (e.g., controlled not, Hadamard, ...), ranged over by $\mathcal{U}$. Process $0_{\tilde{q}}$ is labelled with the tuple $\tilde{q}$ of qbits it owns. This is needed to ensure linearity of qbits, and to clarify which participant owns which qbit. This is relevant since due to entanglement (s)he (in a follow up protocol) may influence other qbits entangled with its own. We write just $0$ when $\tilde{q}$ is empty.

Note that $\prod_{i \in I} p_i \triangleright P_i$ is shorthand for $p_1 \triangleright P_1 | \dots | p_n \triangleright P_n$, where $| \dots |$ is the parallel composition operator, which is associative and commutative. For simplicity, we frequently assume that the tuples of formal parameters $\tilde{x}$ in process definitions and the tuples of expressions for actual parameters $\tilde{e}$ in process calls are split into standard and quantum ones.
<table><caption>**Fig. 3.** Syntax of expressions, processes, and systems</caption><tr><td>e</td><td>::= x</td><td>(variable)</td></tr><tr><td></td><td>q</td><td>(reference inside the qubit register)</td></tr><tr><td></td><td>c</td><td>(constant)</td></tr><tr><td></td><td>e<br>ope</td><td>(operation)</td></tr><tr><td>z</td><td>::= x</td><td>(variable)</td></tr><tr><td></td><td>q</td><td>(reference inside the qubit register)</td></tr><tr><td>P, Q</td><td>::= 0<sub>z</sub></td><td>(inaction, owning qubits in z)</td></tr><tr><td></td><td>p ⊕ ℓ⟨e⟩.P</td><td>(selection/send towards role p)</td></tr><tr><td></td><td>p&{ℓ<sub>i</sub>(x<sub>i</sub>), P<sub>i</sub>}<sub>i∈I</sub></td><td>(branching/receive from role p with I ≠ ∅)</td></tr><tr><td></td><td>def X(̃x) = P in Q</td><td>(process definition)</td></tr><tr><td></td><td>X⟨̃e⟩</td><td>(process call)</td></tr><tr><td></td><td>if e then P else Q</td><td>(conditional)</td></tr><tr><td></td><td>x := meas z.P</td><td>(measurement)</td></tr><tr><td></td><td>new x.P</td><td>(new qubit generation)</td></tr><tr><td></td><td>U(̃z).P</td><td>(unitary operation)</td></tr><tr><td>M</td><td>::= ∏<sub>i∈I</sub> p<sub>i</sub>▷P<sub>i</sub></td><td>(multiparty system)</td></tr></table>

*Example 3 (Quantum Teleportation - Processes)*. We can now write an actual system implementing the quantum teleportation protocol:

$$M = \textcolor{red}{\text{Alice} \triangleright P_A} | \textcolor{blue}{\text{Bob} \triangleright P_B} | \textcolor{green}{\text{Source} \triangleright P_S} | \textcolor{purple}{\text{Env} \triangleright P_E}$$

where:

$P_A = \text{Env} \& (w). \text{Source} \& (x). \text{CNot}(w, x). \text{H}(w). \tilde{r} := \text{meas}(w, x). \text{Bob} \oplus \langle \tilde{r} \rangle. 0$

$P_B = \text{Source} \& (y). \text{Alice} \& (\tilde{r}). \boldsymbol{\sigma}_{\tilde{r}}(y). \text{Env} \oplus \langle y \rangle. 0$

$P_S = \text{new } x_s, y_s. \text{H}(x_s). \text{CNot}(x_s, y_s). \text{Alice} \oplus \langle x_s \rangle. \text{Bob} \oplus \langle y_s \rangle. 0$

$P_E = \text{Alice} \oplus \langle q \rangle. \text{Bob} \& (y). 0_y$

Alice takes the desired **qbits**, then applies to them two unitary transformations: a controlled not **CNot** (which negates the second **qbit** if the first one is true, just propagates it otherwise—and acts linearly if the states of the qubits are not classical states but a superposition of them) and a Hadamard gate **H** (which turns classical states into a superposition), measures the two resulting **qbits** obtaining two classical **bits** in *r* (here we extended the **meas** operator to work on pairs) and sends them to **Bob**.

**Bob** gets the two **bits** and uses them to select which of the 4 Pauli transformations $\sigma_0, \dots, \sigma_3$ to apply to $y$, where $\sigma_0$ is the identity matrix, and $\sigma_1, \sigma_2, \sigma_3$
are the three 2 × 2 Pauli matrices<fnref n="1" />. Source just creates a pair of entangled **qbits**, and sends its components to, respectively, **Alice** and **Bob**. Env just gives the initial **qbit** to **Alice** and gets the result from **Bob**.

Now we describe the typing of processes and systems.

**Definition 4 (Typing Contexts).** $\Theta$ (used for process definitions and calls) maps process variables to session types prefixed by the types of the parameters, $\Gamma$ maps variables to basic types (except **qbits**), and $\Delta$ maps variables and references to (only) the **qbit** type.

$$ \Theta ::= \emptyset \mid \Theta, X:(\tilde{B};T) \quad \Gamma ::= \emptyset \mid \Gamma, x:B (B \neq \textbf{qbit}) \quad \Delta ::= \emptyset \mid \Delta, z:\textbf{qbit} $$

Notably, following DILL [5], we use dual contexts for intuitionistic (classical data) variables and linear (quantum data) variables. Since we omit delegation, there are no channel variables in contexts $\Gamma$ or $\Delta$. We write $\Delta_q$ when $\Delta$ contains only qubit references, and omit contexts in judgements when empty and unambiguous.

**Definition 5 (Typing Judgements).** Typing judgements are of the form:

$$ \Gamma; \Delta \vdash e : B \qquad \Theta \cdot \Gamma; \Delta \vdash P : T \qquad \Gamma; \Delta \vdash \mathcal{M} : G $$

**Definition 6 (Typing Rules).** The typing rules are defined in Fig. 4. Typing rules for operators and constants are standard and omitted (but for 0 and 1). The $\Delta$ used in the conclusion of each typing rule in Fig. 4 is the concatenation of the (different) $\Delta_i$ used in the premises.

The rules are mostly self-explanatory. Notably, due to linearity of **qbits**, when a process sends a **qbit** (rule T-⊕) it loses the ownership (indeed, $\Delta$ is split into $\Delta_1$ used to type the payload of the message and $\Delta_2$ used to type the continuation). Dually, when a process receives a **qbit** (rule T-&) it gains ownership on it. Indeed, it can be used to type the continuation. Note that the two sets of premises are needed to cover two cases depending on whether the received value is classical (first case, added to $\Gamma$) or quantum (second case, added to $\Delta$). We have two rules for conditional, T-if applies when the two branches follow the same local type while T-⊕-if when they contribute with different message send. In both the cases, both the premises use the same $\Delta_2$ since in each computation only one of the branches is executed. In rule T-def, $\Theta$ stores the type of the defined function so that it can then be checked against the invocation in rule T-Call. There $\tilde{B}$ is shorthand for $B_1, \dots, B_n$, and $\tilde{e}$ is shorthand for $e_1, \dots, e_n$.

*Example 4 (Quantum Teleportation - Typing).* Using the typing rules we can derive the judgment:

$$ q:\textbf{qbit} \vdash \mathcal{M} : G $$

We show the typing of **Alice** as an example in Fig. 5.

◇

<footnote n="1">¹ We slightly abuse notation here, we could have modeled this choice in more details using conditionals to actually select one of the transformations.</footnote>
<figure><img src="image_4.png" /><figcaption>Fig. 4. Typing rules for expressions, processes, and systems</figcaption></figure>

<figure><img src="image_5.png" /><figcaption>Fig. 5. Typing for Alice in Quantum Teleportation</figcaption></figure>

## 3 Semantics

The semantics that we present combines the management of quantum state following the approach in [13,31] (for a quantum λ-calculus), with classical semantics for MPST systems, such as in [30,35]. A main novelty is that we need to combine non-determinism (typical of process calculi but absent in λ-calculi) with probabilities originating from measurements of quantum states.

Given a finite set of qubit variables $Q$, called a quantum register, we denote with $\mathcal{H}[Q]$ the Hilbert space generated by all functions $Q \to \{0, 1\}$, denoted as $\mathcal{B}[Q]$, which is the computational basis for $\mathcal{H}[Q]$. Elements of $\mathcal{B}[Q]$, are of the form
$|q_1 \leftarrow b_1, \dots, q_n \leftarrow b_n\rangle$ and ranged over by $|\eta\rangle$, for every $q_i \in \mathbb{Q}$ and $b_i \in \{0, 1\}$. Hence, elements of $\mathcal{H}[\mathbb{Q}]$ are elements of Hilbert spaces with a chosen basis, that is, linear combinations of elements of $\mathcal{B}[\mathbb{Q}]$, written $\mathcal{Q} = \sum_{|\eta\rangle \in \mathcal{B}[\mathbb{Q}]} \alpha_\eta |\eta\rangle$, where $\alpha_\eta \in \mathbb{C}$ are complex probability amplitudes satisfying $\sum_{|\eta\rangle \in \mathcal{B}[\mathbb{Q}]} |\alpha_\eta|^2 = 1$. The probability operator $\mathbb{P}_b^q: \mathcal{H}[\mathbb{Q}] \to [0, 1]$ is given by $\mathbb{P}_b^q(\mathcal{Q}) = \sum_{\eta(q)=b} |\alpha_\eta|^2$. For $q \in \mathbb{Q}$, the projection operator $\hat{\mathbb{P}}_b^q: \mathcal{H}[\mathbb{Q}] \to \mathcal{H}[\mathbb{Q}\setminus\{q\}]$ is given by $\hat{\mathbb{P}}_b^q(\mathcal{Q}) = \frac{1}{\sqrt{\mathbb{P}_b^q(\mathcal{Q})}} \sum_{|\eta\rangle \in \mathcal{B}[\mathbb{Q}\setminus\{q\}]} \alpha_\eta \{q-b\} |\eta\rangle$. For $q \notin \mathbb{Q}$, the new operator $N_q: \mathcal{H}[\mathbb{Q}] \to \mathcal{H}[\mathbb{Q} \cup \{q\}]$ is given by $N_q(\mathcal{Q}) = \mathcal{Q} \otimes |q \leftarrow 0\rangle$ which assigns $|0\rangle$ to $q$. Qubits can be modified by unitary operations, written as $U_{\tilde{q}}: \mathcal{H}[\mathbb{Q}] \to \mathcal{H}[\mathbb{Q}]$, where $\tilde{q}$ is a sequence of distinct qubit variables.

The semantics, defined in Fig. 6, is a transition system over configurations of the form $\langle \mathcal{Q}, \mathcal{M} \rangle$, where $\mathcal{Q}$ is the quantum state associated to the underlying quantum register $\mathbb{Q}$, and $\mathcal{M}$ is a multiparty session-typed system. The semantics is both non-deterministic and probabilistic (it forms a GPLTS, in the sense of [8, Definition 2.5])—the multiparty process behavior is non-deterministic (in the choice of redex for single processes which do some computation, or pairs of processes that communicate), and the quantum operations are probabilistic (in the choice of measurement outcome). The transition relation is: $\rightarrow \subseteq \langle \mathcal{Q}, \mathcal{M} \rangle \times \mathbb{L} \times [0, 1] \times \langle \mathcal{Q}, \mathcal{M} \rangle$, where $\mathbb{L}$ is the set of labels: either $p \rightarrow q: v$ denoting a communication step, or $p$ denoting a computation step (for role names $p$ and $q$). We use $\pi$ to range over probabilities. The semantics relies on a semantics of expressions as well. We do not present it since it is classical, and write $e \downarrow v$ to denote that expression $e$ evaluates to value $v$. The evaluation relation on tuples $\tilde{e} \downarrow \tilde{d}$ is taken pointwise.

Rule [R-COMM] allows processes to communicate. Rules [R-MEAS-0] and [R-MEAS-1] define measurements, and are the only rules defining transitions with non-1 probability. They also consume the measured qubit. Dually, rule [R-NEW] extends the register with a new qubit. Note that there are no transitions for $\mathbf{0}_{\tilde{q}}$ processes.

The transition system satisfies the following properties (expected for GPLTS):

**Proposition 1.** For any $\mathcal{Q}, \mathcal{M}, \mathcal{Q}', \mathcal{M}', \alpha$,

1. if $\langle \mathcal{Q}, \mathcal{M} \rangle \xrightarrow{\alpha} \pi_1 \langle \mathcal{Q}', \mathcal{M}' \rangle$ and $\langle \mathcal{Q}, \mathcal{M} \rangle \xrightarrow{\alpha} \pi_2 \langle \mathcal{Q}', \mathcal{M}' \rangle$, then $\pi_1 = \pi_2$, and

2. it holds that $\sum \{ \pi \in [0, 1] \mid \langle \mathcal{Q}, \mathcal{M} \rangle \xrightarrow{\alpha} \pi \langle \mathcal{Q}', \mathcal{M}' \rangle \} = 1$.

*Proof.* One can notice that the only probabilities which are not 1 originate from measurements. However, the first part holds since the two transitions corresponding to the two outcomes of a given measurement always lead to different states. This is also the only case where there are two transitions from the same state with the same label, and since the probabilities sum up to 1 also the second part holds.

We remark that labels in our semantics are just decorations to simplify the statement of the results in the next section, hence the semantics can be seen as an annotated reduction semantics.
<figure><img src="image_6.png" /><figcaption>Fig. 6. Semantic Rules</figcaption></figure>

Note that we could also give a more abstract description of the semantics, disregarding the qubit register and probabilities. In this setting, actions from a single participant are to be considered as invisible $\tau$ steps. This allows one to more easily relate with MPSTs which indeed only describe communications, but we choose to work with the more concrete quantum semantics, showing the quantum state and probabilities.

**Definition 7 (Multiparty System Transitions).** We say $M \xrightarrow{\alpha} M'$ if $\exists \mathcal{Q}, \mathcal{Q}', \pi \neq 0$ such that $\langle \mathcal{Q}, M \rangle \xrightarrow{\alpha} \pi \langle \mathcal{Q}, M' \rangle$. We say $M \xrightarrow{\tau} M'$ if $\exists p$, such that $M \xrightarrow{p} M'$. We say $M \stackrel{\alpha}{\Rightarrow} M'$ if $M (\xrightarrow{\tau})^* \xrightarrow{\alpha} (\xrightarrow{\tau})^* M'$.

# 4 Results

We prove two kinds of results—the first kind are classical results adapted from MPSTs theory, such as Subject Reduction and Session Fidelity (see, e.g., [9, 30, 35]), to the quantum extension. Such results hold for closed terms, namely terms with no free variables, but, notably, they can have references to the qubit register. Hence the judgments in these statements have the form $\Delta_q \vdash M : G$. The other kind of results show that qbits are treated correctly, linearly in particular.

First, any global type which is not end can perform at least a transition.

**Lemma 2 (Progress for Global Types).** If $G \neq \text{end}$, then $G \to$.

Subject reduction, stated below, ensures that transitions preserve typability for systems with no free variables (which may however have references to the qubit register). We write $\exists \Delta \supseteq \Delta'$ to mean that there exists a context $\Delta'$ such that $\Delta$ is a weakening of $\Delta'$.
**Theorem 3 (Subject Reduction).**

1. If $\Delta_q \vdash \mathcal{M} : G$ and $\mathcal{M} \xrightarrow{\mathbf{p}} \mathcal{M}'$, then $\exists \Delta'_q$ such that $\Delta'_q \vdash \mathcal{M}' : G$.

2. If $\Delta_q \vdash \mathcal{M} : G$ and $\mathcal{M} \xrightarrow{\mathbf{p} \to \mathbf{q} : \ell(v)} \mathcal{M}'$, then $\exists \Delta_q \supseteq \Delta'_q, B, G'$ such that $\Delta'_q \vdash v : B, G \xrightarrow{\mathbf{p} \to \mathbf{q} : \ell(B)} G'$, and $\Delta_q \vdash \mathcal{M}' : G'$.

Note that the environment $\Delta_q$ never changes during communication steps: ownership can move from one process to the other, but **qbits** are neither created nor destroyed. They can only be created and destroyed in computational steps, using, respectively, new qubit generation and measurement.

Session fidelity shows that transitions of global types and of systems do agree. Notice however that global types abstract away from non-communication steps, which are instead present in systems.

**Theorem 4 (Session Fidelity).**

1. If $\Delta_q \vdash \mathcal{M} : G$ and $G \xrightarrow{\mathbf{p} \to \mathbf{q} : \ell(B)} G'$, then $\exists \Delta'_q, \Delta''_q, \mathcal{M}', v$, such that $\Delta'_q \vdash v : B, \mathcal{M} \xrightarrow{\mathbf{p} \to \mathbf{q} : \ell(v)} \mathcal{M}',$ and $\Delta''_q \vdash \mathcal{M}' : G'$.

2. If $\Delta_q \vdash \mathcal{M} : G, \mathcal{M} \xrightarrow{\mathbf{p} \to \mathbf{q} : \ell(v)} \mathcal{M}',$ and $G \xrightarrow{\mathbf{p} \to \mathbf{q} : \ell(B)} G'$, then $\exists \Delta'_q, \Delta''_q$, such that $\Delta'_q \vdash v : B, \text{ and } \Delta''_q \vdash \mathcal{M}' : G'$.

We can now show that well-typed systems have progress and never get stuck.

**Theorem 5 (Progress).** If $\Delta_q \vdash \mathcal{M} : G$, then either $G = \text{end}$, or $\mathcal{M} \longrightarrow \mathcal{M}$.

**Definition 8.** A system $\mathcal{M}$ is stuck if it is not of the form $\prod_{i \in I} \mathbf{P}_i \triangleright \mathbf{0}_{\tilde{z}_i}$, and $\mathcal{M} \not\longrightarrow$. A system $\mathcal{M}$ gets stuck, written $\mathcal{M} \triangleright$, if it reduces to a stuck system.

**Theorem 6 (Type Safety).** If $\Delta_q \vdash \mathcal{M} : G$, then $\mathcal{M} \triangleright$ does not hold.

Given a well-typed process $\Gamma$; $\Delta \vdash P : T$, the free qubits of $p$, written $\text{fq}(P)$ are exactly the qubit variables in $\Delta$. The typing rule $[\text{T-Sys}]$ ensures unique ownership of qubits in a multiparty system. Alternatively, given a well-typed multiparty system $\Gamma$; $\Delta \vdash \prod_{\mathbf{P}_i \in \text{pt}(G)} \mathbf{P}_i \triangleright \mathbf{P}_i : G$, $\text{fq}(\mathbf{P}_i)$ can be computed as $\Delta \cap \text{fv}(\mathbf{P}_i)$, which is exactly $\Delta_i$, by inverting the typing rule $[\text{T-Sys}]$. We can rephrase in our setting the result in [16, Theorem 2].

**Theorem 7 (Unique Ownership of Qubits).** If $\Gamma$; $\Delta \vdash \prod_{i \in I} \mathbf{P}_i \triangleright \mathbf{P}_i : G$, then for any $j, k \in I$ such that $j \neq k$, we have $\text{fq}(\mathbf{P}_j) \cap \text{fq}(\mathbf{P}_k) = \emptyset$.

By safety, we can extend the transitions to typed systems as follows.

**Definition 9 (Typed Multiparty System Transitions).** We say that $\Delta_q \vdash \mathcal{M} : G \stackrel{\alpha}{\Rightarrow} \Delta'_q \vdash \mathcal{M}' : G'$ if $\mathcal{M} \stackrel{\alpha}{\Rightarrow} \mathcal{M}'$ and $G \xrightarrow{\beta} G'$ and $\Delta'_q \vdash \mathcal{M}' : G'$.

We can thus show that the **qbits** needed at runtime are only the ones prescribed by the typing judgment.

**Theorem 8 (Qubit Safety).** If $\Delta_q \vdash \mathcal{M} : G \stackrel{\alpha}{\Rightarrow} \Delta'_q \vdash \mathcal{M}' : G'$, then $\langle \mathcal{H}[\text{qu}(\Delta_q)], \mathcal{M} \rangle \stackrel{\alpha}{\Rightarrow} \langle \mathcal{H}[\text{qu}(\Delta'_q)], \mathcal{M}' \rangle$, where $\text{qu}(\Delta) = \{q | \text{q:qbit} \in \Delta\}$.
# 5 Case Studies

We now put the theory developed in the previous sections to work on some sample quantum protocols from the literature, to complement Quantum Teleportation described in the previous sections. All the protocols mix communications of classical values and communications of references to qubits.

*Example 5 (Quantum Secret Sharing [2, Fig. 21]).* The problem of secret sharing [21] involves an agent **Alice** sending a **qbit** to two agents **Bob** and **Charlie**, one of whom is dishonest. **Alice** does not know which is the dishonest agent, so she encodes the **qbit** in a way that requires **Bob** and **Charlie** to collaborate to retrieve it. In order to do this, they need to have each a **qbit** which is part of a maximally entangled triple, provided by **Source**. As in the running example, we introduce **Env** to model input/output operations.

<figure><img src="image_7.png" /></figure>

We can now write an actual system implementing this multiparty global type:

<figure><img src="image_8.png" /></figure>

where

<figure><img src="image_9.png" /></figure>

<figure><img src="image_10.png" /></figure>

<figure><img src="image_11.png" /></figure>

<figure><img src="image_12.png" /></figure>

<figure><img src="image_13.png" /></figure>

We sometimes use conditional (if *e* then *P*). *Q* as prefix. This can be seen as a shortcut for if *e* then *P*{*Q*/*o*} else *Q* or easily added to the theory. We also consider tuples as data types.

We refer to [2] for a detailed description of the protocol, while we prefer to contrast the clarity of our notation against theirs. For instance, the process for **Charlie** in [2, Fig. 21] is as follows:

<figure><img src="image_14.png" /></figure>

While there is a direct correspondence between the two terms, we argue that the use of participant names instead of channel names makes our notation easier to
understand. Also, local and global types provide abstract descriptions with no correspondence in their framework.

The typing of the participants is very close to the one of the running example, hence we do not detail it.

*Example 6 (Quantum Bit-Commitment [16, Fig. 6]).* The quantum bit-commitment problem [6] requires *Alice* to choose a **bit** value which *Bob* then attempts to guess. The key issue is that *Alice* must evaluate *Bob*'s guess with respect to her original choice of **bit**, without changing her mind. Similarly, *Bob* must not find out *Alice*'s choice before making his guess.

The code in [16, Fig. 6] would roughly correspond to the QMPST below:

$$ \begin{align*} \text{Alice} &\to \text{Bob} : (\text{int}) . \mu t . \\ (\text{Alice} &\to \text{Bob} : (\text{qbit}) . \text{Rnd} \to \text{Bob} : (\text{bit}) . t) + \\ (\text{Rnd} &\to \text{Bob} : (\text{bit}) . \text{Bob} \to \text{Alice} : (\text{bit}) . \\ \text{Alice} &\to \text{Bob} : (\text{bit}) . \text{Alice} \to \text{Bob} : ([\text{bit}])) \end{align*} $$

The key idea is that *Alice* in order to encode a **bit** *x* chooses a sequence of **bits** *xs*, and encodes each of them into a **qbit** using the standard basis if *x* is 0, and the diagonal basis otherwise. *Bob* measures each **qbit** using a random basis (he gets random values from a random number generator *Rnd*). If the random basis matches *Alice* base, it will get the corresponding bit from *xs*, otherwise a random bit (evenly distributed). After having done this, *Bob* sends to *Alice* his guess *g*, and *Alice* checks whether *Bob* guessed correctly. In order to certify her answer, she sends *xs* to *Bob*.

The global type above will not capture the fact that the number of iterations of the recursive behavior depends on the integer value sent by *Alice* to *Bob* in the first interaction, namely the length of *xs*. To capture this dependency one would need to introduce dependent types, which are outside the scope of the present work (we will come back to this point in the final discussion, in Sect. 6).

Additionally, *Rnd* does not know when the protocol should end (*Alice* and *Bob* both know the desired number of iterations), indeed actually the code for *Rnd* in [16, Fig. 6] is just an infinite loop. Since this may be a problem (*Rnd* is not of the form $O_{\tilde{q}}$ for some $\tilde{q}$ when the protocol ends, falsifying type safety (Theorem 6)), most MPST approaches forbid this behavior (we will come back to this point as well in the final discussion, in Sect. 6).

We can instead formalize the protocol in a different form, that does not require dependent types, by having *Alice* telling *Bob* using distinct labels *data* and *stop* whether there are further data or not. We also solve the issue of *Rnd* by having *Bob* telling him when the protocol is about to finish. This results in the global type in Fig. 7.

We can then write the corresponding system (participants are defined in Fig. 8):

$$ \mathcal{M} = \text{Alice} \triangleright P_A \mid \text{Bob} \triangleright P_B \mid \text{Rnd} \triangleright P_R $$
$$ \mu t. \left\{ \begin{array}{l} \text{Rnd} \to \text{Bob}(\text{bit}). \text{Alice} \to \text{Bob}: \left\{ \begin{array}{@{}l@{}} \text{data}(\text{qbit}). \text{Bob} \to \text{Rnd:loop}. t, \\ \text{stop}. \text{Bob} \to \text{Rnd:stop}. \text{Bob} \to \text{Alice}(\text{bit}). \\ \text{Alice} \to \text{Bob}(\text{bit}, [\text{bit}]). \text{Bob} \to \text{Env}: \left\{ \begin{array}{@{}l@{}} \text{verified}, \\ \text{notVerified} \end{array} \right\} \end{array} \right\} \end{array} \right. $$

<caption>Fig. 7. Global type for Quantum Bit Commitment</caption>

$$
\begin{align*}
P_A &= \mathbf{def} \ X(x, xs, ys) = \\
    &\quad \mathbf{if} \ xs \neq \emptyset \ \mathbf{then} \ \mathbf{new}_{x_q}(\mathbf{if} \ \mathbf{hd}(xs) = \mathbf{1} \ \mathbf{then} \ \sigma_1(x_q)). \\
    &\quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \mathbf{(if} \ x = \mathbf{1} \ \mathbf{then} \ \mathbf{H}(x_q)). \mathbf{Bob} \oplus \mathbf{data}(x_q). \mathbf{X}(x, \mathbf{tl}(xs), ys) \\
    &\quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \mathbf{else} \ \mathbf{Bob} \oplus \mathbf{stop}. \mathbf{Bob} \ \& \ \{ (g). \mathbf{Bob} \oplus \langle (x, ys) \rangle \}. \mathbf{0} \\
    &\quad \quad \mathbf{in} \ X(x, xs, xs) \\
P_B &= \mathbf{def} \ X_V(ms, vs, a) = \\
    &\quad \mathbf{if} \ ms = \emptyset \ \mathbf{then} \ \mathbf{Env} \oplus \mathbf{verified}. \mathbf{0} \\
    &\quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \mathbf{else} \ \mathbf{if} \ \mathbf{fst}(\mathbf{hd}(ms)) \neq \mathbf{a} \ \vee \ \mathbf{snd}(\mathbf{hd}(ms)) = \mathbf{hd}(vs) \ \mathbf{then} \ X_V(\mathbf{tl}(ms), \mathbf{tl}(vs), a) \\
    &\quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \mathbf{else} \ \mathbf{Env} \oplus \mathbf{notVerified}. \mathbf{0} \\
    &\quad \mathbf{in} \ \mathbf{def} \ X(ms) = \\
    &\quad \quad \mathbf{Rnd} \ \& \ y. \mathbf{Alice} \ \& \ \left\{ \begin{array}{@{}l@{}} \mathbf{data}(x). \mathbf{Rnd} \oplus \mathbf{loop}. \mathbf{(if} \ y = \mathbf{1} \ \mathbf{then} \ \mathbf{H}(x)). z := \mathbf{meas} \ x. \mathbf{X}(\mathbf{ms}@\langle y, z \rangle) \\ \text{stop.} \ \mathbf{Rnd} \oplus \text{stop.} \ \mathbf{Alice} \oplus \langle g \rangle. \mathbf{Alice} \ \& \ (a, vs). X_V(\mathbf{ms}, vs, a) \end{array} \right\} \\
    &\quad \mathbf{in} \ X(\emptyset) \\
P_R &= \mathbf{def} \ X = \mathbf{new}_{x_q. \mathbf{H}}(x_q). r := \mathbf{meas}_{x_q} \ \mathbf{Bob} \oplus \langle r \rangle. \mathbf{Bob} \ \& \ \left\{ \begin{array}{@{}l@{}} \mathbf{loop}. \ X(\langle r \rangle) \\ \text{stop.} \ \mathbf{0} \end{array} \right\} \ \mathbf{in} \ X(\langle r \rangle)
\end{align*}
$$

<caption>Fig. 8. Processes for Quantum Bit-Commitment</caption>

$$
\begin{align*}
G | \text{Alice} &= \mu t. \text{Bob} \oplus \text{data}(\text{qbit}). t, \text{stop}. \text{Bob} \oplus (\text{bit}). \text{Bob} \oplus (\text{bit}, [\text{bit}]). \text{end} \\
G | \text{Bob} &= \mu t. \text{Rnd} \oplus (\text{bit}). \text{Alice} \oplus \left\{ \begin{array}{@{}l@{}} \text{data}(\text{qbit}). \text{Rnd} \oplus (\text{loop}). t \\ \text{stop}. \text{Rnd} \oplus (\text{stop}). \text{Alice} \oplus (\text{bit}). \text{Alice} \oplus (\text{bit}, [\text{bit}]). \text{Env} \oplus \left\{ \begin{array}{@{}l@{}} \text{verified}. \text{end} \\ \text{notVerified}. \text{end} \end{array} \right\} \end{array} \right\} \\
G | \text{Rnd} &= \mu t. \text{Bob} \oplus \left\{ (\text{bit}). \text{Bob} \oplus \begin{array}{@{}l@{}} \text{loop}. t \\ \text{stop}. \text{end} \end{array} \right\}
\end{align*}
$$

<caption>Fig. 9. Projections for Quantum Bit-Commitment</caption>

$$
\begin{align*}
X: (\emptyset, G | \text{Rnd}) \cdot r: \text{bit} \vdash X(\langle r \rangle) : G | \text{Rnd} \quad X: (\emptyset, G | \text{Rnd}) \cdot r: \text{bit} \vdash \mathbf{0} : \text{end} \\
\frac{X: (\emptyset, G | \text{Rnd}) \cdot r: \text{bit} \vdash \text{Bob} \oplus \left\{ \begin{array}{@{}l@{}} \text{loop}. X(\langle r \rangle) \\ \text{stop.} \mathbf{0} \end{array} \right\} : \text{Bob} \oplus \left\{ \begin{array}{@{}l@{}} \text{loop}. G | \text{Rnd} \\ \text{stop}. \text{end} \end{array} \right\}} \\
\frac{X: (\emptyset, G | \text{Rnd}) \cdot r: \text{bit} \vdash \text{Bob} \oplus \langle r \rangle . \text{Bob} \oplus \left\{ \begin{array}{@{}l@{}} \text{loop}. X(\langle r \rangle) \\ \text{stop.} \mathbf{0} \end{array} \right\} : G | \text{Rnd}} \\
\frac{X: (\emptyset, G | \text{Rnd}) \cdot \emptyset; x_q: \text{qbit} \vdash r : = \mathbf{meas}_{x_q} \ \text{Bob} \oplus \langle r \rangle . \text{Bob} \oplus \left\{ \begin{array}{@{}l@{}} \text{loop}. X(\langle r \rangle) \\ \text{stop.} \mathbf{0} \end{array} \right\} : G | \text{Rnd}} \\
X: (\emptyset, G | \text{Rnd}) \cdot \emptyset; x_q: \text{qbit} \vdash \mathbf{H}(x_q). r := \mathbf{meas}_{x_q} \ \text{Bob} \oplus \langle r \rangle . \text{Bob} \oplus \left\{ \begin{array}{@{}l@{}} \text{loop}. X(\langle r \rangle) \\ \text{stop.} \mathbf{0} \end{array} \right\} : G | \text{Rnd} \\
X: (\emptyset, G | \text{Rnd}) \cdot \emptyset \vdash \mathbf{new}_{x_q. \mathbf{H}}(x_q). r := \mathbf{meas}_{x_q} \ \text{Bob} \oplus \langle r \rangle . \text{Bob} \oplus \left\{ \begin{array}{@{}l@{}} \text{loop}. X(\langle r \rangle) \\ \text{stop.} \mathbf{0} \end{array} \right\} : G | \text{Rnd} \\
\emptyset \cdot \emptyset \vdash \mathbf{def} \ X = \mathbf{new}_{x_q. \mathbf{H}}(x_q). r := \mathbf{meas}_{x_q} \ \text{Bob} \oplus \langle r \rangle . \text{Bob} \oplus \left\{ \begin{array}{@{}l@{}} \text{loop}. X(\langle r \rangle) \\ \text{stop.} \mathbf{0} \end{array} \right\} \ \mathbf{in} \ X(\langle r \rangle) : G | \text{Rnd}
\end{align*}
$$

where $\Phi = X: (\emptyset, G | \text{Rnd}) \cdot \emptyset \vdash X(\langle r \rangle) : G | \text{Rnd}$.

<caption>Fig. 10. Typing of Rnd in Quantum Bit-Commitment</caption>

Using the typing rules we can derive: $\vdash \mathcal{M}: G$, provided that $x$ and $xs$ in the initial invocation of Alice recursive behavior are replaced by concrete values (to have a closed term). As first step, we project the global type on the different
participants, obtaining the result in Fig. 9. For simplicity, we show the typing of
`Rnd` only, in Fig. 10. ◇

A further case study, discussing Gottesman and Chuang's Quantum Digital
Signature [19], is available in the extended report [26].

# 6 Discussion

We have extended MPSTs so to provide a clean formalism to describe and reason
about quantum protocols. There are other languages for describing quantum
protocols, such as imperative languages like LanQ [27] and QMCLANG [14,
29], and process calculi such as CQP [16] and CCSq [2]. All of them rely on
named channels for communication, and channels are typed with the type of their
payload (and linear in some approaches), hence multiple channels are needed
between the same participants. We believe our approach of specifying in send
 resp. receive) operations the target (resp. sender) of the message makes for a
clearer description. All the approaches above are also based on classical types,
not behavioral types, hence do not provide a global type as abstract description
of the protocol.

*Quantum Session Types.* We purposefully based our approach on a mini-
mal MPST system (taking inspiration from [18,35]), to highlight the interplay
between MPSTs and quantum computing, and to understand which advanced
features of session types are useful to type protocols in the area. While we have
found no need for multiple sessions or delegation, Example 6 could be modeled
in a way closer to the specification in [16, Fig. 6] by relying on value-dependent
session types (see [33]). Indeed, one would like to specify that the number of
iterations depends on an integer exchanged beforehand.

The same example has also shown that sometimes requiring all the processes
to complete their program is too restrictive. In Example 6, `Rnd` could be more
easily modeled as an infinite loop generating random numbers, and the fact that
it could generate further random numbers after the end of the protocol is not an
issue from the practical point of view. However, to type such a formalisation of
the protocol one would need, beyond changing the typing rules, to weaken type
safety (Theorem 6). One could specify that some participants do not need to
terminate their behaviour. Such a kind of approach has been studied in [4]. Note
that selective participation (as discussed in [17, 20, 23]), allowing a participant to
join only in some branches of a protocol, would not be helpful here, since indeed
`Rnd` is needed in all the executions.

In the future we want to tackle the two limitations discussed above. It would
also be interesting to consider refinement types. While not needed from the
modeling point of view, they would allow proving stronger properties, e.g., about
possible results of measure operations. This would need however to combine
refinement types with probabilities (the result of a measurement operation is
probabilistic) and to capture the phenomenon of entanglement, which relates
the behavior of different qubits.

*Quantum Processes*. The particular abstraction of quantum processes we have chosen is based on CQP [16], where processes can perform quantum operations on quantum data, and exchange messages on *channels* with other processes—these channels allow for classical communication with *quantum* references, which are pointers to qubits in a *global* quantum register. Ergo, these are not *quantum channels* in the sense of quantum information theory (see [28, Ch.12]), because processes do not have *local* quantum state—however, having a global quantum state with local quantum references appears to be expressive enough—whether this is a limitation or a feature of our approach remains to be investigated.

There exist rigorous mathematical frameworks for quantum networks [11] and quantum protocols [1] (to name a few). We do not know any formal calculi for quantum processes and quantum channels based on these frameworks, and it is not yet clear how our approach of extending MPSTs to quantum computing could be related to them. Session types are a completely syntactic approach, but there are recent attempts to give them denotational semantics in terms of event structures [9], or using category theory [3, 12, 25]. In fact, the categorical structure of session types is the same as the categorical structure of quantum processes (compact closure or star-autonomy)—they both require a notion of strong duality. This suggests, on the one hand, a way to use session types to build a type theory for quantum processes, and on the other hand, a way to verify correctness of typed quantum processes using denotational semantics, which we hope to explore in future work.

References

1. Abramsky, S., Coecke, B.: A categorical semantics of quantum protocols. In: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004, pp. 415–425. IEEE (2004). https://doi.org/10.1109/LICS.2004.1319636

2. Ardeshir-Larijani, E., Gay, S.J., Nagarajan, R.: Automated equivalence checking of concurrent quantum systems. ACM Trans. Comput. Log. **19**(4), 28:1–28:32 (2018). https://doi.org/10.1145/3231597

3. Atkey, R.: Observed communication semantics for classical processes. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 56–82. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54434-1_3

4. Barbanera, F., Dezani-Ciancaglini, M.: Partially typed multiparty sessions. In: 16th Interaction and Concurrency Experience, ICE 2023. EPTCS, pp. 15–34 (2023). https://doi.org/10.4204/EPTCS.383.2

5. Barber, A., Plotkin, G.: Dual intuitionistic linear logic. University of Edinburgh, Laboratory for Foundations of Computer Science (1996)

6. Bennett, C.H., Brassard, G.: Quantum cryptography: public key distribution and coin tossing. Theoret. Comput. Sci. **560**, 7–11 (2014)

7. Bennett, C.H., et al.: Teleporting an unknown quantum state via dual classical and Einstein-Podolsky-Rosen channels. Phys. Rev. Lett. **70**(13), 1895 (1993)
8. Bernardo, M., De Nicola, R., Loreti, M.: A uniform framework for modeling non-deterministic, probabilistic, stochastic, or mixed processes and their behavioral equivalences. Inf. Comput. **225**, 29–82 (2013)

9. Castellani, I., Dezani-Ciancaglini, M., Giannini, P.: Event structure semantics for multiparty sessions. J. Logic. Algeb. Methods Program. **131**, 100844 (2023). https://doi.org/10.1016/j.jlamp.2022.100844

10. Ceragioli, L., et al.: Quantum bisimilarity via barbs and contexts: curbing the power of non-deterministic observers. Proc. ACM Program. Lang. **8** (POPL), 1269–1297 (2024). https://doi.org/10.1145/3632885

11. Chiribella, G., D'Ariano, G.M., Perinotti, P.: Theoretical framework for quantum networks. Phys. Rev. A **80**, 022339 (2009). https://doi.org/10.1103/PhysRevA.80.022339

12. Choudhury, V.: Classical processes in modern dress (ST30 - SPLASH 2023). https://2023.splashcon.org/details/st-anniversary-30-papers/9/Classical-Processes-in-modern-dress

13. Dal Lago, U., Rioli, A.: Applicative bisimulation and quantum λ-calculi. In: Das-tani, M., Sirjani, M.: FSEN 2015. LNCS, vol. 9392, pp. 54–68. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-319-24644-4_4

14. Davidson, T.A.S., et al.: Model checking for communicating quantum processes. Int. J. Unconv. Comput. **8**(1), 73–98 (2012)

15. Garhwal, S., Ghorani, M., Ahmad, A.: Quantum programming language: a systematic review of research topic and top cited languages. Archiv. Comput. Methods Eng. **28**, 289–310 (2021)

16. Gay, S.J., Nagarajan, R.: Communicating quantum processes. In: 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, pp. 145–157. ACM (2005). https://doi.org/10.1145/1040305.1040318

17. Gheri, L., et al.: Design-by-contract for flexible multiparty session protocols. In: Ali, K., Vitek, J.: 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), pp. 8:1–8:28. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Dagstuhl (2022). https://doi.org/10.4230/LIPIcs.ECOOP.2022.8

18. van Glabbeek, R., Höfner, P., Horne, R.: Assuming just enough fairness to make session types complete for lock-freedom. In: LICS, pp. 1–13. IEEE (2021). https://doi.org/10.1109/LICS52264.2021.9470531

19. MISCGottesman, D., Chuang, I.: Quantum digital signatures. arXiv preprint arXiv:quantph/0105032 (2001)

20. Harvey, P., et al.: Multiparty session types for safe runtime adaptation in an actor language. In: ECOOP, LIPIcs, pp. 10:1–10:30. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021). https://doi.org/10.4230/LIPICS.ECOOP.2021.10

21. Hillery, M., Bužek, V., Berthiaume, A.: Quantum secret sharing. Phys. Rev. A **59**(3), 1829 (1999)

22. Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. J. ACM **63**(1), 9:1–9:67 (2016). https://doi.org/10.1145/2827695

23. Hu, R., Yoshida, N.: Explicit connection actions in multiparty session types. In: FASE. LNCS, vol. 10202, pp. 116–133. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54494-5_7

24. Hüttel, H., et al.: Foundations of session types and behavioural contracts. ACM Comput. Surv. **49**(1), 3:1–3:36 (2016). https://doi.org/10.1145/2873052

25. Kavanagh, R.: A domain semantics for higher-order recursive processes. arXiv preprint arXiv:2002.01960 (2020)
26. Lanese, I., Dal Lago, U., Choudhury, V.: Towards quantum multiparty session types. arXiv preprint arXiv:2409.11133 (2024)

27. Mlnarik, H.: Introduction to LanQ-an Imperative quantum programming language (2006). https://lanq.sourceforge.net/doc/introToLanQ.pdf

28. Nielsen, M., Chuang, I.: Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press (2010)

29. Papanikolaou, N.: Model checking quantum protocols. Ph.D. thesis, University of Warwick, Coventry (2009)

30. Scalas, A., Yoshida, N.: Less is more: multiparty session types revisited. Proc. ACM Program. Lang. 3(POPL), 30:1–30:29 (2019). https://doi.org/10.1145/3290343

31. Selinger, P., Valiron, B.: A lambda calculus for quantum computation with classical control. MSCS 16(3), 527–552 (2006). https://doi.org/10.1017/S0960129506005238

32. The Quantum Protocol Zoo (2024). https://wiki.veriqloud.fr/

33. Toninho, B., Caires, L., Pfenning, F.: Dependent session types via intuitionistic linear type theory. In: PPDP, pp. 161–172. Association for Computing Machinery, New York (2011). https://doi.org/10.1145/2003476.2003499

34. Wootters, W.K., Zurek, W.H.: A single quantum cannot be cloned. Nature 299, 802–803 (1982). https://doi.org/10.1038/299802a0

35. Yoshida, N., Gheri, L.: A very gentle introduction to multiparty session types. In: ICDCIT. LNCS, vol. 11969, pp. 73–93. Springer, Heidelberg (2020). https://doi.org/10.1007/978-3-030-36987-3_5

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

<figure><img src="image_15.png" /></figure>