# Combining quantum and classical control: syntax, semantics and adequacy

Kinnari Dave, Louis Lemonnier, Romain Péchoux, Vladimir Zamdzhiev

► To cite this version:

Kinnari Dave, Louis Lemonnier, Romain Péchoux, Vladimir Zamdzhiev. Combining quantum and classical control: syntax, semantics and adequacy. FoSSaCS 2025 - 28th International Conference on Foundations of Software Science and Computation Structures, May 2025, Hamilton, Canada. pp.155-175, 10.1007/978-3-031-90897-2_8. hal-05093249

HAL Id: hal-05093249

https://hal.science/hal-05093249v1

Submitted on 2 Jun 2025

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
# Combining quantum and classical control: syntax, semantics and adequacy

Kinnari Dave<fnref n="1" />,<fnref n="2" />, Louis Lemonnier<fnref n="3" />, Romain Péchoux<fnref n="2" />, and
Vladimir Zamdzhiev<fnref n="1" />

**Abstract.** The two main notions of control in quantum programming languages are often referred to as “quantum” control and “classical” control. With the latter, the control flow is based on classical information, potentially resulting from a quantum measurement, and this paradigm is well-suited to mixed state quantum computation. Whereas with quantum control, we are primarily focused on pure quantum computation and there the “control” is based on superposition. The two paradigms have not mixed well traditionally and they are almost always treated separately. In this work, we show that the paradigms may be combined within the same system. The key ingredients for achieving this are: (1) syntactically: a modality for incorporating pure quantum types into a mixed state quantum type system; (2) operationally: an adaptation of the notion of “quantum configuration” from quantum lambda-calculi, where the quantum data is replaced with pure quantum primitives; (3) denotationally: suitable (sub)categories of Hilbert spaces, for pure computation and von Neumann algebras, for mixed state computation in the Heisenberg picture of quantum mechanics.

## 1 Introduction

There are two important paradigms in the design of quantum programming languages – “classical control” and “quantum control”. In the classical control approach (e.g., [19,21,20,6,17,13]) the control flow of a program is conditioned on classical information that may result from quantum measurements. Type systems for quantum programming languages that are based on classical control are able to represent a variety of effects, e.g., quantum state preparation, state evolution through the application of unitary operators, and probabilistic effects induced by quantum measurements. Because of this, it is natural to conceptualise such lambda-calculi using quantum structures and models that are suited to describing mixed-state quantum computation and information (e.g., density matrices, superoperators). In the quantum control approach (e.g., [18,10,11,1,23]), one usually places an emphasis on pure state quantum computation and more specifically on superposition of terms, pure quantum states and unitary operators. In approaches that utilise classical control, one often starts with a selection

<footnote n="1">¹ Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, Laboratoire Méthodes Formelles, 91190, Gif-sur-Yvette, France</footnote>

<footnote n="2">² Université de Lorraine, CNRS, Inria, LORIA, F-54000 Nancy, France</footnote>

<footnote n="3">³ University of Edinburgh</footnote>
<figure><img src="image_2.png" /><figcaption>Fig. 1: A program and the corresponding circuit</figcaption></figure>

of constants that represent some unitary operators (e.g., Hadamard, CNOT) and more complex unitary operations can be described in a circuit-like fashion by composing the atomic unitaries in a suitable way. Whereas in the quantum control approach, unitary operators are defined through more fundamental prim- itives that do not require the programmer to specify a circuit-like decomposition of the unitary operation. Because of this, a considerable economy in terms of syntax can be achieved with quantum control. For example, consider the cir- cuit in Figure 1. It uses the well-known Toffoli gate, which would have to be decomposed as a large circuit like the one in the figure. However, the program representing this circuit can instead be written as a simple lambda term in our language given in Figure 1, where $Tof \triangleq \mathcal{B}(\text{ctrl CNOT})$. To highlight this further note that the controlled Hadamard can be defined similarly to the Toffoli in our language, but a typical classically controlled quantum programming language would require two *H* gates, six *T* gates and one *CNOT* gate. Thus, our lan- guage offers an ease of writing programs by abstracting away quantum circuits. We aim to shift focus from drawing quantum circuits, which is a more low-level approach to writing code, to writing programs directly using syntax, which is a more high-level approach. In classical (non-quantum) programming, we can use high-level languages to write algorithms without having to specify boolean cir- cuits or to encode integers using tuples of bits/booleans. With our paper, we are trying to advance quantum programming abstractions towards such a direction. For example, an individual qnat $|n\rangle$ can be used instead of a tensor of qubits $|q_1q_2...q_k\rangle$ whose binary encoding corresponds to *n*. We view boolean circuits and binary encodings of integers as low-level and likewise for their quantum counterparts. Our aim is to develop higher-level quantum abstractions.

**Our Contributions** Because of the potential presence of quantum entangle- ment, it is impossible (in general) to decompose a quantum state into a non- trivial tensor product of two smaller quantum states. Indeed, in the quantum lambda-calculus (QLC) [15], which is based on classical control, the type **qbit** of qubits is an opaque type in the sense that there are no closed values of such a type. Program states may be described via quantum configurations which are triples ($|\psi\rangle$, $\ell$, $M$), where $|\psi\rangle \in \mathbb{C}^2$ is a pure quantum state (possibly entan- gled); $M$ is a program possibly containing free variables of type **qbit**; $\ell$ is a linking function that maps the free quantum variables of $M$ to appropriate com- ponents of the state $|\psi\rangle$. It is possible to also view $\ell$ as a unitary permutation acting on $|\psi\rangle$ and this view is important for our development. Such configura- tions, even though they are not part of the user-facing syntax, allow us to reason
about entangled states and the operational semantics are described via a relation ($|\psi\rangle$, $\ell$, $M$) $\rightarrow_p$ ($|\psi'\rangle$, $\ell'$, $M'$), with $p$ the probability of reduction.

The main idea that allows us to combine both quantum and classical control is to modify the quantum configurations described above by replacing the quantum state $|\psi\rangle$ with a suitable *pure quantum term t* and to replace the linking function $\ell$ with a suitable *unitary permutation u*$_{σ}$, where both *t* and $u_σ$ are syntactic constructs from our pure quantum language that may be assigned types.

In order to accurately model the situation with the QLC, the term *t* has to correspond to a *normalised* vector and we replace the unitary constants from the QLC with programmable unitary constructs, so the pure subsystem also has to ensure their *unitarity*. Our pure subsystem is based on ideas described in [3,18], but we further build on this by introducing an *equational theory* for our pure subsystem, which has unique normal forms and we describe a *denotational semantics* for it that is *sound and complete* with respect to the equational theory.

Next, we integrate the pure quantum subsystem into our main calculus, which allows us to describe both quantum and classical information and, therefore also classical control. This is a variant of the QLC with the addition of a modality $\mathcal{B}(Q)$ which allows us to view pure quantum types $Q$ as types of mixed state quantum operations in the Heisenberg picture. The intuition behind this is the following: mixed states in the Schrödinger picture can be seen as CPTP maps$^4$ $(1 \mapsto \rho): \mathbb{C} \to \mathcal{T}(H)$ whereas mixed states in the Heisenberg picture are given by functionals of the form $\text{tr}(\rho-): \mathcal{B}(H) \to \mathbb{C}$, both of which are determined by a choice of density operator $\rho: H \to H$ (see [5, Section 7] for detail on this matter). This modality allows us to replace the *constants* for state preparation and unitaries acting on qubits in the QLC with *terms and expressions* from the pure subsystem acting on more general quantum types beyond qubits. The operational semantics are described via a suitable adaptation of the aforementioned quantum configurations. The denotational semantics follows previous work on quantum programming semantics based on von Neumann algebras [6, 17, 13] and we show, in addition, that the assignment $\mathcal{B}(-)$ may be extended to a strict monoidal functor (between the relevant categories of Hilbert spaces and von Neumann algebras) that is crucial for our denotational semantics.

Overall, the two main contributions of our work are: (1) we show that quantum and classical control can be combined in a syntactic, operational and denotational sense by integrating a pure quantum control subsystem as part of the meta-theory and syntax of a quantum lambda-calculus; (2) an equational theory for a (sub)system for quantum control with unique normal forms and a sound and complete denotational semantics. Some supplementary material including extra examples, proofs, and complete figures for formation rule predicates are provided in Appendix.

**Related Work** We begin by commenting on semantic approaches to classical control. In [15], the authors describe a QLC where the higher-order primitives are interpreted using techniques from the semantics of quantitative models of linear

<footnote n="4">⁴ CPTP stands for ‘completely positive trace preserving’ and $\mathcal{T}(H)$ and $\mathcal{B}(H)$ stand for the trace-class and bounded linear operators, respectively, on a Hilbert space $H$.</footnote>
<table><caption>Fig. 2: A comparison of some quantum programming languages.</caption><thead><tr><th></th><th>Our work</th><th>Qunity [25]</th><th>λ-S<sub>1</sub> [11]</th><th>Sym [18]</th><th>Quipper [12]</th><th>QWIRE [16]</th><th>Q.λ-calculus [15]</th><th>[8,7,24] [22]</th></tr></thead><tbody><tr><td>Quantum control</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>Classical control</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>Infinite dimensional quantum type</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>Unitary function spaces</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>Normalised quantum terms</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>Denotational semantics</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>Adequacy</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>Termination</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td></tr></tbody></table>

logic. In [8,7,24], the author(s) work with QLCs whose denotational semantics is given via game semantics. More recently, in [22], the authors have shown how to interpret a QLC with recursive types using presheaves that are enriched over a suitable base category and they also prove full abstraction. The approach that we use in this paper is based on von Neumann algebras which have been previously used for the semantics of quantum programming languages [6,13,17]. In particular, if we disregard the interaction between the pure subsystem and the main calculus, then our denotational model for the main calculus coincides with the one in [6]. The reason that we choose von Neumann algebras over the other approaches is because we think this gives the model which is the closest to mathematical physics out of the ones mentioned. Furthermore, our primary focus is not on developing the semantics of the classical paradigm; instead it is on the *interaction* between the pure quantum control subsystem and the main calculus based on classical control. Another distinguishing feature of our system, compared to the ones above, is the addition of types such as $\mathcal{B}(\mathbf{qnat})$ which allow us to describe states in infinite-dimensional Hilbert spaces, such as $\ell^2(\mathbb{N})$, and which we do not think can be easily included using the other approaches.

For the quantum control paradigm, relevant work includes [10,11,1,9,2]. What all these approaches have in common is that they have specific terms in their syntax for representing superposition. However, these approaches do not ensure unitarity of the relevant function spaces, in general. Our approach, instead, is based on related work first described in [18] and then later in [3]. One of the most distinctive features of this approach to quantum control is that the terms that introduce superposition are subject to strict formation conditions that ensure (linear algebraic) normalisation of the corresponding vectors. Furthermore, this approach to quantum control also imposes strict admissibility criteria on the unitary function spaces that can be formed through the type system and this ensures unitarity of the relevant expressions. Because of these considerations, we choose this approach to model quantum control in our pure subsystem. However, we have made some changes, in particular, we replace the operational semantics from these works with an equational theory instead. This works better for

<footnote>* These languages admit general recursion.</footnote>
our approach to *combining* quantum and classical control within the quantum
configurations (in QLCs the quantum data is considered modulo equality). We
continue building on this development by describing a denotational semantics
that is sound and complete with respect to the equational theory. This is the
first such result for languages with quantum control.

Another paper which combines quantum and classical control is Qunity [25]. However, compared to our work, Qunity does not have an operational semantics, but instead there is a compilation procedure to quantum circuits. Furthermore, the denotational semantics of Qunity: (1) does not ensure unitarity and normalisation of the pure primitives in its language, whereas ours does; (2) does not ensure trace-preservation of the mixed primitives in the Schrödinger picture, whereas ours does indeed ensure unitality of the mixed primitives in the Heisenberg picture (which corresponds to trace-preservation under the Heisenberg-Schrödinger duality). Other differences include that Qunity is restricted to finite-dimensional quantum data and they do not have higher-order lambda abstractions for dealing with mixed-state primitives. Instead, Qunity relies on a try-catch mechanism to combine quantum and classical control, whereas our approach is based on quantum configurations. The table in Figure 2 gives a comparison of our work with other quantum programming languages. *Normalised quantum terms* refers to the property that terms representing pure/mixed quantum states always correspond to complex vectors with norm one/density operators with trace one. *Adequacy* refers to the property that two observationally distinct programs have distinct denotational interpretations.

## 2 Quantum Control

This part is adapted from one of the authors’ PhD thesis [14, Chapter 3], to
which we refer the readers for full detail and proofs.

We write **Unitary** ⊆ **Isometry** ⊆ **Hilb** for the (sub)categories whose objects are the Hilbert spaces and whose morphisms are the unitaries (resp. isometries, bounded linear maps) between them.

### 2.1 Pure Quantum Syntax

We begin by describing a subsystem for quantum control. The syntax is based on symmetric pattern-matching [18]. The *pure quantum types* are given by the following grammar: $Q ::= I | Q_1 \otimes Q_2 | Q_1 \oplus Q_2 | \mathbf{qnat}$.

We interpret every quantum type as a separable Hilbert space: the unit type
is interpreted as [[I]] ≜ C; pair types are interpreted as tensor products; (quant-
tum) sum types are interpreted as direct sums; finally, [[qnat]] ≜ ℓ²(N). The type
of qubits may be defined as **qbit** ≜ **I** ⊕ **I**. We write **qbit**n for the n-fold tensor
product **qbit** ⊗ ... ⊗ **qbit**. The Hilbert space ℓ²(N) allows us to form superposi-
tions with respect to a countable orthonormal basis (e.g., 1/√2 |3⟩ + 1/√2 |7⟩). We
may think of ℓ²(N) as a quantum analogue of the natural numbers, to abstract
from qubit-level computation. The addition of **qnat** allows us to reason about
pure quantum computation while abstracting away from quantum circuits.
$$b ::= x \mid * \mid \text{inl } b \mid \text{inr } b \mid b_1 \otimes b_2 \mid 0 \mid S b$$

$$v ::= \sum_{i \in \mathcal{I}} \alpha_i \cdot b_i$$

$$u ::= \{ | b_1 \mapsto v_1 \dots | b_n \mapsto v_n \} | u_1 \oplus u_2 | u_1 \otimes u_2 | u_2 \circ u_1 | u^* | \text{ctrl } u$$

$$t ::= x \mid * \mid \text{inl } t \mid \text{inr } t \mid t_1 \otimes t_2 \mid 0 \mid S t \mid u t \mid \sum_{i \in \mathcal{I}} \alpha_i \cdot t_i$$

<caption>Fig. 3: Term grammar for the pure quantum subsystem.</caption>

The *unitary types*, written as $U(Q_1, Q_2)$, represent the unitary function spaces of our language. They are not interpreted as Hilbert spaces, but as sets of unitary operators: $[[U(Q_1, Q_2)]] \triangleq \{u: [[Q_1]] \to [[Q_2]] | u \text{ is a unitary operator}\}$.

We now describe the language of the pure quantum subsystem whose grammar is given in Figure 3. (Pure) *Terms* $t$ are written in bold notation in order to distinguish with other syntactic constructs. The symbols $x, y, z$ denote pure quantum variables. We write $\text{inl}_{Q_1 \oplus Q_2} t$ and $\text{inr}_{Q_1 \oplus Q_2} t$ for sum type injections, and, for brevity, we often omit writing the subscripts. The term $t_1 \otimes t_2$ is used for forming pairs of terms. The terms $0$ and $S t$ represent the qnat $|0\rangle$ and the qnat $|n+1\rangle$, provided that $t$ represents the qnat $|n\rangle$. We define $|\underline{n}\rangle \triangleq \mathbf{S}^n 0$ and $|t+\underline{n}\rangle \triangleq \mathbf{S}^n t$, for $\mathbf{n} \in \mathbb{N}$. The term $ut$ represents the application of a unitary $u$ to a term $t$. Superpositions are represented by the term $\sum_{i \in \mathcal{I}} \alpha_i \cdot t_i$. We impose strict conditions on these terms that ensure normalisation in §2.2.

In Figure 3, the *Basis Terms* (ranged over by symbols $b, b_i$) are the simplest kind of pure terms. The (pure) *Values*, ranged over by $v$ and defined in Figure 3, are the normal forms in this subsystem. They are of the form $\sum_{i \in \mathcal{I}} \alpha_i \cdot b_i$, where $\alpha_i \in \mathbb{C}$, $b_i$ are basis terms, and $\mathcal{I}$ is a finite index set. We consider $\mathcal{I}$ as a totally ordered set so that we can work with unique normal forms. We also write $\alpha_1 \cdot b_1 + \dots + \alpha_n \cdot b_n$ for $\sum_{i \in \{1, \dots, n\}} \alpha_i \cdot b_i$. The formation conditions (§2.2) ensure that all terms in the sums are pairwise distinct, orthogonal, and of the same type, and thus well-formed values correspond to *normalised vectors*. In our equational theory, every quantum term $t$ can be rewritten to a normalised pure value $v$ (Proposition 3). The values are the canonical forms of this subsystem.

**Example 1.** The basis term $*: \mathcal{I}$ represents the complex scalar $1 \in \mathbb{C}$. The basis terms that represent the computational basis for qubits can be defined by $|0\rangle \triangleq \text{inl}*: \text{qbit}$ and $|1\rangle \triangleq \text{inr}*: \text{qbit}$. Other basis terms that can be defined include $|00\rangle \triangleq |0\rangle \otimes |0\rangle: \text{qbit}^2$ and $|11\rangle \triangleq |1\rangle \otimes |1\rangle: \text{qbit}^2$. If $b$ is a basis term, we often write it as $|b\rangle$ to distinguish it from other (non-basis) terms, e.g., $|2\rangle: \text{qnat}$ represents the qnat $|2\rangle \in \ell^2(\mathbb{N})$. Single-qubit states may be defined by $|\pm\rangle \triangleq (1/\sqrt{2} \cdot |0\rangle \pm 1/\sqrt{2} \cdot |1\rangle): \text{qbit}$. (Entangled) quantum states can be defined, e.g., $\text{Bell} \triangleq (1/\sqrt{2} \cdot |00\rangle + 1/\sqrt{2} \cdot |11\rangle): \text{qbit}^2$. Linear combinations of qnats can also be written in the language, i.e. $(1/\sqrt{2} \cdot |0\rangle + 1/\sqrt{2} \cdot |1\rangle + 1/\sqrt{3} \cdot |2\rangle): \text{qnat}$.

Next, we describe the *Unitaries* $u$ of Figure 3. *Unitary pattern-matching* $\{ | b_1 \mapsto v_1 \dots | b_n \mapsto v_n \}$ allows us to build unitary maps out of basis terms and values: every *closed* basis term $b_i$ is mapped to the closed value $v_i$; basis terms with free variables $b_i$ determine a mapping through the use of substitution with respect to the corresponding value $v_i$, wherein both $b_i$ and $v_i$
have the same free variables occurring within them, and the induced mapping is determined by performing all possible substitutions of the free variables on both sides with the same closed basis terms. The formation conditions (§2.2) ensure that the basis terms $b_i$ (resp. the values $v_i$) determine an ONB for the type $Q_1$ (resp. $Q_2$) and therefore $\{|b_1 \mapsto v_1 \dots |b_n \mapsto v_n\}$ determines a unitary map. We introduce syntactic sugar for quantum if statements, written **qif**. If $u_1$ is of the form $\{|b_1 \mapsto v_1 \dots |b_n \mapsto v_n\}$ and $u_2$ of the form $\{|b'_1 \mapsto v'_1 \dots |b'_m \mapsto v'_m\}$ then **qif x then x $\otimes u_2$ else x $\otimes u_1$** is short for the unitary:

$$ \left\{ \begin{array}{c} |0\rangle \otimes b_1 \mapsto |0\rangle \otimes v_1 \\ \vdots \\ |0\rangle \otimes b_n \mapsto |0\rangle \otimes v_n \end{array} , \begin{array}{c} |1\rangle \otimes b'_1 \mapsto |1\rangle \otimes v'_1 \\ \vdots \\ |1\rangle \otimes b'_m \mapsto |1\rangle \otimes v'_m \end{array} \right\} $$

**Example 2.** The unitaries Had and CNOT below encode the standard Hadamard and CNOT gates, respectively. CNOT makes use of some simple pattern-matching on its last line: it can match either with $|0\rangle \otimes |0\rangle$ or with $|0\rangle \otimes |1\rangle$. The unitary Had$_{qnat}$ defines an extension of the Hadamard gate on the space $\ell^2(\mathbb{N})$.

$$ \text{Had} : U(\text{qbit}, \text{qbit}) \qquad \text{CNOT} : U(\text{qbit}^2, \text{qbit}^2) \\ \text{Had}^{\triangleq} \left\{ \begin{array}{c} | |0\rangle \mapsto 1/\sqrt{2} \cdot |0\rangle + 1/\sqrt{2} \cdot |1\rangle \\ | |1\rangle \mapsto 1/\sqrt{2} \cdot |0\rangle - 1/\sqrt{2} \cdot |1\rangle \end{array} \right\} \qquad \text{CNOT}^{\triangleq} \left\{ \begin{array}{c} | |1\rangle \otimes |0\rangle \mapsto |1\rangle \otimes |1\rangle \\ | |1\rangle \otimes |1\rangle \mapsto |1\rangle \otimes |0\rangle \\ | |0\rangle \otimes |x\rangle \mapsto |0\rangle \otimes |x\rangle \end{array} \right\} $$

$$ \text{Had}_{\text{qnat}} : U(\text{qnat}, \text{qnat}) \\ \text{Had}_{\text{qnat}}^{\triangleq} \left\{ \begin{array}{c} | |0\rangle \mapsto 1/\sqrt{2} \cdot |0\rangle + 1/\sqrt{2} \cdot |1\rangle \\ | |1\rangle \mapsto 1/\sqrt{2} \cdot |0\rangle - 1/\sqrt{2} \cdot |1\rangle \\ | |x+2\rangle \mapsto |x+2\rangle \end{array} \right\} $$

The remaining expressions for forming unitaries are easy to understand: $u_2 \circ u_1$ represents composition of unitaries, $u^*$ represents the adjoint of a unitary, $u_1 \otimes u_2$ and $u_1 \oplus u_2$ represent tensor products and direct sums of unitaries, and finally, ctrl u represents a qubit-controlled unitary operator. For simplicity, we sometimes write $\{|b_i \mapsto v_i \dots \}$ as a shorthand notation for the unitary $\{|b_1 \mapsto v_1 \dots |b_n \mapsto v_n\}$, when n is clear from context or unimportant. We also point out that unitaries depend only on values and basis terms and that general pure terms cannot be used for the construction of unitaries.

## 2.2 Formation Conditions

In order to guarantee (linear-algebraic) normalisation for quantum terms and unitarity for functions, we rely on formulating: (1) a suitable orthogonality relation $\perp \subseteq \text{Terms} \times \text{Terms}$, which is used as part of the formation condition of some terms; (2) additional predicates ONB$_Q$ and ONB$_Q^{\text{val}}$ which ensure that a set of basis terms/values of type $Q$ determines an ONB which is used as part of the formation conditions for the atomic introduction rule of unitaries.

The relation $\perp$ is defined as the smallest binary relation $\perp \subseteq \text{Terms} \times \text{Terms}$ that is closed under the rules in Figure 4. Quantum terms that are orthogonal via this relation are orthogonal in a denotational sense as well (§2.3).
$$ \frac{\text{inl } t_1 \perp \text{inr } t_2}{\text{inl } t_1 \perp \text{inr } t_2} \quad \frac{0 \perp S t}{0 \perp S t} \quad \frac{t_1 \perp t_2}{u t_1 \perp u t_2} \quad \frac{j \neq k. \ t_j \perp t_k}{\sum_{j \in \mathcal{J}} (\alpha_j \cdot t_j) \perp \sum_{k \in \mathcal{K}} (\beta_k \cdot t_k)} \quad \overline{\sum_{i \in \mathcal{I}} \alpha_i \beta_i} = 0 $$

<caption>Fig. 4: Rules for the orthogonality relation (excerpt).</caption>

$$ \frac{\text{ONB}_Q(\{x\}) \qquad \text{ONB}_I(\{*\})}{\text{ONB}_{Q_1}(\pi_i(S)) \qquad \text{ONB}_{Q_2}(\{\text{inl } b \mid b \in S\} \cup \{\text{inr } b \mid b \in T\})} \qquad \frac{\text{ONB}_{Q_1}(S) \qquad \text{ONB}_{Q_2}(T)}{\text{ONB}_{Q_1 \oplus Q_2}(\{\text{inl } b \mid b \in S\} \cup \{\text{inr } b \mid b \in T\})} \\ \frac{\text{ONB}_{Q_i}(\pi_i(S)) \qquad \forall b \in \pi_i(S), \text{ONB}_{Q_j}(S_b^i)}{\text{ONB}_{Q_1 \otimes Q_2}(S)} \qquad i, j \in \{1, 2\}, i \neq j \\ \frac{\text{ONB}_{\text{qnat}}(S)}{\text{ONB}_{\text{qnat}}(\{0\} \cup \{S b \mid b \in S\})} \qquad \frac{(\alpha_{b,b'})(b,b') \in S \times S \text{ is a unitary matrix}}{\text{ONB}_Q(S)} \qquad \text{ONB}_Q^{\text{val}}(\{\sum_{b' \in S} \alpha_{b,b'} \cdot b' \mid b \in S\}) $$

<caption>Fig. 5: Orthonormal basis predicates.</caption>

This relation allows us to enforce the orthogonality of terms appearing within a superposition $\sum_{i \in \mathcal{I}} (\alpha_i \cdot t_i)$. Under the assumption that all terms $t_i$ represent normalised vectors that are pairwise orthogonal, the norm of the superposition is easy to calculate (statically), and it is given by $\sum_{i \in \mathcal{I}} |\alpha_i|^2$. This justifies the formulation of the introduction rule for superposition (Figure 6) and guarantees that the vector represented by this superposition of terms is normalised.

**Example 3.** The rules for the orthogonality relation are not restricted to closed quantum terms, e.g., $0 \perp S x$ and $\text{inl } x \perp \text{inr } y$. One can also show that $|+\rangle \perp |-\rangle$ (defined in Example 1). However, we cannot show that $\text{Had } |0\rangle \perp |-\rangle$ even though $\text{Had } |0\rangle$ is equal to $|+\rangle$ with respect to our equational logic and also with respect to our denotational semantics (both introduced later). The reason for this is that we wish to define the orthogonality relation statically.

In order to determine whether a finite set $S$ of (potentially open) basis terms determines an ONB for a type $Q$, we introduce the *orthonormal basis predicates* ONB$_Q(S)$ in Figure 5, originally known as *orthogonal decomposition* [18]. Note that there is a mistake with the rule for the tensor product in the original paper, e.g. it does not allow for the typing of a CNOT.

Given a type $Q$ and a finite set of basis terms $S$, we say that $S$ determines an *orthonormal basis of $Q$*, which we write as $\text{ONB}_Q(S)$, if this can be derived via the rules in Figure 5. We now explain some of the notation used therein. If $S$ is a set of the form $\{b_1 \otimes b'_1, \dots, b_n \otimes b'_m\}$ then we define $\pi_1(S) \triangleq \{b_1, \dots, b_n\}$ and $\pi_2(S) \triangleq \{b'_1, \dots, b'_m\}$. In this situation, we also define $S_b^1 \triangleq \{b' \mid b \otimes b' \in S\}$ and $S_{b'}^2 \triangleq \{b \mid b \otimes b' \in S\}$. Furthermore, the ONB predicate implies pairwise orthogonality of the associated values. Note that the predicate $\text{ONB}_Q(S)$ is defined for a finite set $S$ consisting of *basis* terms. But, in order to be able to define unitaries that make use of superposition, we also work with other ONBs. Given a finite set $S$ consisting of *values*, we say that $S$ determines an ONB of type $Q$, and we write $\text{ONB}_Q^{\text{val}}(S)$ to indicate this, whenever this can be derived via the rules in Figure 5. We also introduce syntactic sugar: the value $\sum_{i \in \mathcal{I}} \alpha_i \cdot b_i$ is
<figure><img src="image_3.png" /><figcaption>Fig. 6: Formation rules for terms and unitaries (excerpt).</figcaption></figure>

the finite linear combination where elements with scalar 0 are omitted. In other words, the indices $i \in \mathcal{I}$ such that $\alpha_i = 0$ are ignored, e.g., if $\alpha_1 = 1$ and $\alpha_2 = 0$, $\sum_{i \in \{1, 2\}} \alpha_i \cdot b_i$ is the value $\sum_{i \in \{*\}} 1 \cdot b_i$.

**Example 4.** For qbit, the rules from Figure 5 show that $\text{ONB}_{\text{qbit}}(\{|0\rangle, |1\rangle\})$ and that $\text{ONB}_{\text{qbit}}(\{|+\rangle, |-\rangle\})$ hold (with $|\pm\rangle$ defined in Example 1). We also have that $\text{ONB}_{\text{qbit}}(\{x\})$, where $x$ is a variable. In other words, we determine an ONB for the type qbit by substituting $x$ with all possible closed computational basis terms of type qbit (see Figure 3). For qnat, any set $S$ with the property that $\text{ONB}_{\text{qnat}}(S)$ holds, must contain a term that is not closed. We have that $\text{ONB}_{\text{qnat}}(\{|\underline{x}\rangle\})$, $\text{ONB}_{\text{qnat}}(\{|0\rangle, |\underline{x}+1\rangle\})$, and $\text{ONB}_{\text{qnat}}(\{|0\rangle, |1\rangle, |\underline{x}+2\rangle\})$ hold true and determine the same ONB for the type qnat (it represents the computational basis of $\ell^2(\mathbb{N})$). The set used in the last predicate allows us to conclude that $\text{ONB}_{\text{qnat}}(\{1/\sqrt{2} \cdot |0\rangle + 1/\sqrt{2} \cdot |1\rangle, 1/\sqrt{2} \cdot |0\rangle - 1/\sqrt{2} \cdot |1\rangle, |\underline{x}+2\rangle\})$ holds. This last set of values is used to type Had$_{qnat}$ from Example 2.

Judgements for pure quantum terms have the form $\Gamma \vdash t: Q$ where $\Gamma$ stands for a linear context of the form $\Gamma \triangleq x_1: Q_1, \dots, x_n: Q_n$. The formation rules for terms are presented in Figure 6; the first two lines are standard for a linearly-typed term calculus. The rule for superposition depends on the orthogonality relation $\perp$, and the premise ensures that the resulting superposition corresponds to a normalised vector. This is made precise later (Theorem 1). Finally, the formation rule for $ut$, i.e. the application of a unitary $u$ to a term $t$, is akin to function application in lambda-calculi. However, the complexity is primarily relegated to the judgement $\vdash u: U(Q_1, Q_2)$, which ensures the unitarity of $u$.

The formation rules for unitaries are presented in Figure 6. In the introduction rule for atomic unitaries $\{|b_1 \mapsto v_1 \dots |b_n \mapsto v_n\}$, we have that the potentially open basis terms $\{b_1, \dots, b_n\}$ (resp. values $\{v_1, \dots, v_n\}$) determine an ONB for $Q_1$ (resp. $Q_2$) in the sense explained above. Then the resulting bijective mapping that associates $b_i$ to $v_i$ uniquely determines a unitary. The formation rules for the remaining unitaries are straightforward, and they align easily with the mathematical intuition that motivates them. We also wish to note that unitaries do not depend on general terms (see Figure 3).
## 2.3 Denotational Semantics for Pure Quantum System

Recall (§2.1) that the interpretation of a pure quantum type $\mathcal{Q}$ is a Hilbert space $[[\mathcal{Q}]]$, i.e., an object of the category **Isometry**, and the interpretation of a unitary type $U(\mathcal{Q}_1, \mathcal{Q}_2)$ is the set $[[U(\mathcal{Q}_1, \mathcal{Q}_2)]]$ of unitaries in $[[\mathcal{Q}_1]] \to [[\mathcal{Q}_2]]$.

A linear context is interpreted in the usual way $[[\Gamma]] \triangleq [[\mathcal{Q}_1]] \otimes \cdots \otimes [[\mathcal{Q}_n]]$. The interpretation of a judgement $\Gamma \vdash t: Q$ is given by a morphism $[[\Gamma \vdash t: Q]] \in \text{Isometry}([\Gamma], [[Q]])$. We also sometimes abuse notation and write $[[t]]$ for brevity instead of $[[\Gamma \vdash t: Q]]$. For closed quantum terms $\cdot \vdash t: Q$, we interpret the empty context as $\mathbb{C}$ (the tensor unit in **Isometry**) and so we can identify $[[\cdot \vdash t: Q]](1)$ with a normalised vector.

Every value $v$ is of the form $\sum_{i \in \mathcal{I}} \alpha_i \cdot b_i$, but the sum is subject to strict admissibility conditions imposed by the orthogonality relation $\perp$ from §2.2. The denotational significance of this relation is provided by the statement: given $\Gamma_1 \vdash t_1: Q$ and $\Gamma_2 \vdash t_2: Q$, if $t_1 \perp t_2$ then $[[t_1]]^*[[t_2]] = 0_{[[\Gamma_2]], [[\Gamma_1]]}$; which is central in proving that the interpretation of values is well-defined as isometries.

The most challenging unitaries to interpret are the unitary pattern-matchings, constructed through the use of basis terms and values (but not general terms). Another key role is played by the $\text{ONB}_Q$ and $\text{ONB}^{\text{valの}}_Q$ predicates: they can be understood as determining suitable ONBs of the corresponding types. The denotational significance of these predicates is that they give us a resolution of the identity at type $\mathcal{Q}$, as made precise by the following proposition.

**Proposition 1.** Let $\Gamma_1 \vdash v_1: Q, \dots, \Gamma_n \vdash v_n: Q$ be well-formed values. If $\text{ONB}^{\text{val}}_Q\{v_1, \dots, v_n\}$, then $\text{id}_{[[Q]]} = \sum_{i=1}^n [[v_i]] \circ [[v_i]]^*$.

Pattern-matching is then interpreted by $[[\vdash \{ \dots | b_i \mapsto v_i \dots \}]] \triangleq \sum_i [[v_i]] \circ [[b_i]]^*$, and the previous proposition ensures it is unitary. Finally, we can show that the interpretation of all pure quantum terms is well-defined as isometries.

**Theorem 1.** If $\Gamma \vdash t: Q$, then $[[t]] \in \text{Isometry}([\Gamma], [[Q]])$.

Moreover, any canonical symmetric monoidal isomorphism can be represented by the unitaries of our language. The canonical symmetric monoidal isomorphisms are simply those that can be defined using the structure of a symmetric monoidal category only, i.e. isomorphisms that are given by: left and right unitors, symmetric swaps, associators, closed under composition and tensor products. We use this result later for quantum configurations.

**Proposition 2.** Let $\mathcal{Q}_1$ and $\mathcal{Q}_2$ be two pure types, and let $f: [[\mathcal{Q}_1]] \to [[\mathcal{Q}_2]]$ be a canonical symmetric monoidal isomorphism. Then, there exists a unitary $\vdash u: U(\mathcal{Q}_1, \mathcal{Q}_2)$ such that $[[u]] = f$.

## 2.4 Equational Theory

We now describe the equational theory of the pure quantum subsystem. Given two pure quantum terms $t_1$ and $t_2$, we write $\Gamma \vdash t_1 = t_2: Q$ to indicate that $t_1$ equals $t_2$ as terms of type $Q$ in context $\Gamma$. As usual if $\Gamma \vdash t_1 = t_2: Q$, the rules imply that $\Gamma \vdash t_1: Q$ and $\Gamma \vdash t_2: Q$. We now explain some of the more
interesting rules in greater detail. The rules of the equational theory are divided into four groups. The first one is concerned with the usual rules for reflexivity, symmetry and transitivity. Secondly, we provide rules to handle linear algebraic identities, such as exchanging sums and the linearity of injections and unitaries; this also contains the rule $\Gamma \vdash \sum_{i=1}^{n} 1 \cdot t = t: Q$. A small excerpt is found below.

$$ \frac{\Gamma \vdash \sum_i \alpha_i \cdot (\sum_j \beta_{i,j} \cdot t_j) : Q}{\Gamma \vdash \sum_i \alpha_i \cdot (\sum_j \beta_{i,j} \cdot t_j) = \sum_j (\sum_i \alpha_i \beta_{i,j}) \cdot t_j : Q} \qquad \frac{\vdash u: U(Q_1, Q_2)}{\Gamma \vdash u (\sum_i \alpha_i \cdot t_i) = \sum_i \alpha_i \cdot (u t_i) : Q_2} $$

Congruence rules comprise the third group, e.g., $\Gamma \vdash S t_1 = S t_2$: **qnat** given that $\Gamma \vdash t_1 = t_2$: **qnat**. Last but not least are the computational rules, which, read left to right, can be seen as providing an operational semantics. The most important rule and our version of $\beta$-reduction, is the rule for unitary pattern-matching applied to a basis term.

$$ \frac{\cdot \vdash b': Q_1 \qquad \vdash \{ | b_1 \mapsto v_1 \dots | b_n \mapsto v_n \} : U(Q_1, Q_2) \qquad s(b_j) = b' \cdot \vdash \{ | b_1 \mapsto v_1 \dots | b_n \mapsto v_n \} b' = s(v_j) : Q_2}{\cdot \vdash \{ | b_1 \mapsto v_1 \dots | b_n \mapsto v_n \} b' = s(v_j) : Q_2} $$

The formation conditions on unitary pattern-matching ensure that $\text{ONB}_{Q_1}(\{b_i\}_{i=1}^n)$. With the latter, and given $\cdot \vdash b'$: $Q_1$, there exists a unique substitution $s$ and a unique $b_j$ such that $s(b_j) = b'$. The resulting term of the rule is then the same substitution applied to the corresponding output $v_j$. Such substitutions were first defined in [18], and can be deduced via an inference system.

**Proposition 3.** Given $\cdot \vdash t: Q$, there is a unique value $v$ s.t. $\cdot \vdash t = v: Q$.

This proposition shows that pure terms have a unique normal form. It is crucial for the proof of the completeness theorem, and comes in handy in the rest of the paper, especially to define the reduction system for the main calculus (§3).

**Theorem 2 (Completeness).** $\cdot \vdash t_1 = t_2: Q \iff [\cdot \vdash t_1: Q] = [\cdot \vdash t_2: Q]$.

### 3 Combining Classical and Quantum Control

This section lays down the syntax and semantics of the main calculus, which combines the quantum control fragment with a classically controlled layer, a variant of a call-by-value linear lambda-calculus. The subsystem which we presented in the previous section is designed to represent pure quantum information and computation, whereas in this section, we are concerned with mixed quantum information and computation. Our denotational approach towards this uses von Neumann algebras, which provide an appropriate mathematical setting to achieve this treatment. Operationally, this is achieved by adapting the configurations (also called closures) ($|\psi\rangle$, $\ell$, $M$) from an effectful quantum lambda-calculus, e.g., [6,21], by replacing the quantum state $|\psi\rangle$ with a pure term $t$, replacing the linking function $\ell$ with a unitary $u$ that can be described via our syntax and which represents a suitable permutation, and finally by defining suitable formation conditions for the configuration.
<figure><img src="image_4.png" /><figcaption>Fig. 7: Syntax of the classically controlled system.</figcaption></figure>

## 3.1 Syntax and Typing Rules

The types of the main calculus, ranged over by capital Latin letters (e.g., A, B) are given in Figure 7. All types except Nat and $\mathcal{B}(Q)$ are standard in a system for a classical call-by-value linear lambda-calculus. Nat is a ground type representing classical natural numbers and $\mathcal{B}(Q)$ is the type that represents mixed state quantum computation on the Hilbert space determined by the type $Q$. As we see later, this type plays an important role by introducing quantum and probabilistic effects into the system. The modality $\mathcal{B}$ is inspired from the denotational model, where $\mathcal{B}(H)$ represents the von Neumann algebra of bounded operators on the Hilbert space $H$.

Terms (and values) of the calculus are described in Figure 7. The term $\mathit{pure}(t)$ models the preparation of a pure quantum state represented by the quantum term $t$. Measurement is modelled by the term $\mathit{meas}(M)$. The term $\mathcal{B}(u)(M)$ represents the application of the unitary $u$ to a term $M$. Additionally, we have two syntactic constructs to model the isomorphism between the types $\mathcal{B}(Q_1) \otimes Q_2)$ and $\mathcal{B}(Q_1) \otimes \mathcal{B}(Q_2)$: the term $\mathit{let} \ \mathcal{B}(z) = M \ in \ N$ allows one to construct a term of type $\mathcal{B}(Q_1) \otimes Q_2)$ from a term of type $\mathcal{B}(Q_1) \otimes \mathcal{B}(Q_2)$ and the term $\mathit{let} \ \mathcal{B}(x \otimes y) = M \ in \ N$ deals with the opposite direction. This isomorphism arises because the functor $\mathcal{B}(\cdot)$ used in the denotational model is strict monoidal. Both constructs are necessary to allow the language to manipulate composed quantum systems and also terms possibly representing entangled states.

Typing contexts (ranged over by symbols $\Delta, \Sigma_1, \Sigma_2$) are finite sequences $\Delta \triangleq x_1 : A_1, \dots, x_n : A_n$ mapping variables to types. We use the notation $!\Delta$ for contexts of the form $x_1 : !A_1, \dots, x_n : !A_n$. Typing judgements have the form $\Delta \vdash M : A$ and follow a linear typing discipline to deal with quantum data. The typing rules are given in Figure 8 where, as usual, $\Sigma_1, \Sigma_2$ denotes the disjoint union of $\Sigma_1$ and $\Sigma_2$. Classical bits correspond to the type $bit \triangleq I+I$ and mixed state qubits have type $qbit \triangleq \mathcal{B}(qbit)$. The rule for the term $\mathit{pure}(t)$ introduces a state $t$ from the quantum control fragment as a term of type $\mathcal{B}(Q)$ into the main calculus. The typing rule for measurement maps a term $M$ of quantum type $\mathcal{B}(Q)$ to a term $\mathit{meas}(M)$ of classical type $\overline{Q}$, where the type $\overline{Q}$ is defined inductively on the structure of the pure quantum type $Q$:

$\overline{I} \triangleq I, \quad \overline{Q_1} \otimes \overline{Q_2} \triangleq \overline{Q_1} \otimes \overline{Q_2}, \quad \overline{Q_1} \oplus \overline{Q_2} \triangleq \overline{Q_1} + \overline{Q_2}, \quad \overline{qnat} \triangleq \text{Nat.}$
$$
\begin{array}{l@{\qquad}l@{\qquad}l}
\begin{array}{c}
\begin{array}{c|c}
\Delta, \Sigma_1 \vdash L : A + B & \Delta, \Sigma_2, x : A \vdash M : C \\
\Delta, \Sigma_1, \Sigma_2 \vdash \text{case } L \text{ of } \{\text{inl}(x) \to M, \text{ inr}(y) \to N\} : C
\end{array} \\
\\
\begin{array}{c}
\begin{array}{c|c}
\Delta, x : A \vdash M : B & \Delta, \Sigma_1 \vdash M : A \neg B \quad \Delta, \Sigma_2 \vdash N : A \\
\Delta \vdash \lambda x.M : A \neg B & \Delta, \Sigma_1, \Sigma_2 \vdash M N : B
\end{array} \\
\\
\begin{array}{c}
\begin{array}{c|c}
\Delta, \Sigma_1 \vdash L : \text{Nat} \quad \Delta, \Sigma_2 \vdash M : A & \Delta, \Sigma_2, x : \text{Nat} \vdash N : A \\
\Delta, \Sigma_1, \Sigma_2 \vdash \text{match } L \text{ with } \{\text{zero} \to M, \text{ succ}(x) \to N\} : A
\end{array} \\
\\
\begin{array}{c}
\begin{array}{c|c}
\Delta \vdash M : \mathcal{B}(Q) & \vdash u : U(Q_1, Q_2) \quad \Delta, \Sigma_1 \vdash M : \mathcal{B}(Q_1) \\
\Delta \vdash \text{meas}(M) : \overline{Q} & \Delta, \Sigma_1 \vdash \mathcal{B}(u)(M) : \mathcal{B}(Q_2)
\end{array} \\
\\
\begin{array}{c}
\begin{array}{c|c}
\Delta, \Sigma_1 \vdash M : \mathcal{B}(Q_1) \otimes \mathcal{B}(Q_2) & \Delta, \Sigma_2, z : \mathcal{B}(Q_1) \otimes Q_2 \vdash N : A \\
\Delta, \Sigma_1, \Sigma_2 \vdash \text{let } \mathcal{B}(z) = M \text{ in } N : A
\end{array} \\
\\
\begin{array}{c}
\begin{array}{c|c}
\Delta, \Sigma_1 \vdash M : \mathcal{B}(Q_1 \otimes Q_2) & \Delta, \Sigma_2, x : \mathcal{B}(Q_1), y : \mathcal{B}(Q_2) \vdash N : A \\
\Delta, \Sigma_1, \Sigma_2 \vdash \text{let } \mathcal{B}(x \otimes y) = M \text{ in } N : A
\end{array} \\
\end{array}
\end{array}
\end{array}
\end{array}
$$

<caption>Fig. 8: Typing rules for terms (excerpt).</caption>

This gives the classical analogue of the type $\mathcal{Q}$, e.g., $\overline{\mathbf{qbit}} = \mathbf{bit}$. For a quantum basis term $\mathbf{b}$ of type $\mathcal{Q}$, $\overline{\mathbf{b}}$ (defined below) denotes its translation to a classical value of type $\overline{\mathcal{Q}}$, which we use to represent measurement outcomes.

$$ \overline{\ast} \triangleq \ast, \quad \overline{\mathbf{b}}_1 \otimes \overline{\mathbf{b}}_2 \triangleq \overline{\mathbf{b}}_1 \otimes \overline{\mathbf{b}}_2, \quad \overline{\text{inl}} \overline{\mathbf{b}} \triangleq \text{inl}(\overline{\mathbf{b}}), \quad \overline{\mathbf{0}} \triangleq \text{zero}, \quad \overline{\mathbf{S}} \overline{\mathbf{b}} \triangleq \text{succ}(\overline{\mathbf{b}}). $$

## 3.2 Operational Semantics

*Quantum configurations.* We lay down the operational semantics of the calculus using an adaptation of the notion of a *quantum configuration*.

**Definition 1 (Quantum Configuration).** Let Conf be the set of quantum configurations $C \triangleq (t, u_\sigma, M)$, where:

- $t \in \textit{Terms}$ represents a pure quantum state;

- $u_\sigma \in \textit{Unitaries}$ represents a symmetric monoidal isomorphism;

- $M \in \textit{TERMS}$ is a term from the main calculus.

In the above definition, we can think of the quantum term $t$ as representing a quantum state, because the quantum control fragment ensures that $t$ can be rewritten (in its equational theory) to a unique quantum value (Proposition 3). Next, $u_\sigma$ permutes the components of $t$ so that they appear in the same order as variables that represent them in $M$. We slightly abuse terminology and refer to $u_\sigma$ as a permutation, but it is meant to be understood as a canonical symmetric monoidal isomorphism (see Proposition 2). If we fix the domain and codomain of $u_\sigma$, then the essential data is given by a choice of permutation $\sigma$ and this makes it easier to understand how each unitary acts on the coordinates, and the contextual rules formulation becomes precise. Note that, thanks to Proposition 2, the pure quantum syntax is expressive enough to represent all the monoidal permutations that we need in the sequel.

**Example 5.** Consider the quantum configuration $(t, u_{id}, x \otimes y)$, where we have $t \triangleq \ast \otimes (1/\sqrt{2} \cdot |0\rangle \otimes |0\rangle + 1/\sqrt{2} \cdot |1\rangle \otimes |1\rangle)$ and $u_{id} \triangleq \{|\ast \otimes w \otimes z \mapsto w \otimes z\}$
is a unitary with type $|\vdash u_{id}: U(I \otimes qbit \otimes qbit, qbit \otimes qbit)$. It conveys the information that the variable $x$ in $x \otimes y$ keeps track of the first qubit in $t$ and that the variable $y$ keeps track of the second one. Whereas in the configuration $(t, u_{swap}, x \otimes y)$ with $u_{swap} \triangleq \{|* \otimes w \otimes z \mapsto z \otimes w\}$, the variable $x$ keeps track of the second qubit and $y$ of the first one. Note that, due to quantum entanglement, the term $t$ cannot be decomposed into a non-trivial tensor product, and the variables $x$ and $y$ should be thought of as identifying qubit components of $t$, instead of storing quantum data themselves.

A quantum configuration $\mathcal{V} = (v, u_\sigma, V)$, when both the quantum term $v$ and term $V$ are values, is called a *value configuration*. For example, $(|0\rangle, u_{id}, x)$ is a value configuration. A quantum configuration $\mathcal{SV} = (v, u_\sigma, M)$, where $v$ is a quantum value, is a *semi-value configuration*. We write $\mathcal{VConf}$ (resp. $\mathcal{SVConf}$) for the set of (resp. semi-)value configurations. The reason we introduce semi-value configurations, is because they allow us to define our operational semantics for the main calculus modulo equality of the pure quantum terms $t$ (analogous to the quantum lambda-calculus). We already proved that values $v$ are normal forms for the pure terms (Proposition 3), so this makes them a natural choice.

**Definition 2.** A quantum configuration $(t, u_\sigma, M)$ is well-formed with type A, written as $(t, u_\sigma, M)$: A if the following judgments can be derived:

$$ - \vdash t: Q_1 \otimes \dots \otimes Q_n; $$

$$ - \vdash u_\sigma: U(Q_1 \otimes \dots \otimes Q_p, Q'_1 \otimes \dots \otimes Q'_m); $$

$$ - x_1: \mathcal{B}(Q'_1), \dots, x_m: \mathcal{B}(Q'_m) \vdash M: A. $$

We write $\text{WF}_X(A)$ for the set of well-formed configurations in $X$ with type A, where $X \in \{\text{Conf}, \text{VConf}, \text{SVConf}\}$.

**Example 6.** The configuration $((1/\sqrt{2} \cdot |00\rangle + 1/\sqrt{2} \cdot |11\rangle) \otimes |0\rangle, u_{id}, x \otimes y)$ with:

$$ - \vdash (1/\sqrt{2} \cdot |00\rangle + 1/\sqrt{2} \cdot |11\rangle) \otimes |0\rangle : \text{qbit}^3; $$

$$ - \vdash u_{id}: U(\text{qbit}^3, \text{qbit}^3); $$

$$ - x: \mathcal{B}(\text{qbit}^2), y: \text{qbit} \vdash x \otimes y: \mathcal{B}(\text{qbit}^2) \otimes \text{qbit}. $$

In this configuration, $u_{id}$ is just the identity, $x$ points to the Bell state in $t$ whereas $y$ points to $|0\rangle$. We have $n = 3, m = 2$, with $Q_1 = Q_2 = Q_3 = \text{qbit}$, $Q'_1 = \text{qbit}^2$ and $Q'_2 = \text{qbit}$. The configuration is well-formed.

The above example highlights the need for $m$ and $n$ (from Definition 2) to be different values. The intuition behind this difference is that the unitary $u_\sigma$ partitions the $n$ quantum types into $m$ blocks, where each block is represented by a variable in $M$. Furthermore, in situations where we wish to combine two such blocks which are not next to each other in the tensor expression of the $n$ types, we allow the possibility of permuting these blocks and merging them so that now two blocks that were initially represented by two variables are represented by one. This is formally expressed in the reduction rules we define next. The role of $u_\sigma$ in a well-formed configuration is illustrated in Figure 9. The small-step reduction $\cdot \to \cdot \subseteq \text{Conf} \times [0, 1] \times \text{Conf}$ is the relation defined by the rules of Figure 10: the reduction $C \to_p C'$ holds when the quantum configuration $C$ reduces to $C'$ with probability $p \in [0, 1]$.
<figure><img src="image_5.png" /><figcaption>Fig. 9: Graphical representation of a well-formed quantum configuration.</figcaption></figure>

The reduction rules along with the unitaries required to state them are given in Figure 10. {$b_{ij}$}$_{i,j}$ stand for basis terms and s in the reduction rule for meas(x) corresponds to the position of $b_i$ in the tensor product appearing in the quantum term. All sums are finite. The unitary $u_{\sigma_{gather}}$ appearing in the reduction rule for the term $let \mathcal{B}(z) = x \otimes y$ in N merges two consecutive variables into one block, so that now a single variable can represent it. Similarly, in the reduction

rule for the term $let \mathcal{B}(x \otimes y) = z$ in N, the unitary $u_{\sigma_{divide}}$ partitions a block into two, so that two variables can represent them. The two rules are symmetric as expected, since these terms only allow switching between types $\mathcal{B}(Q_1 \otimes Q_2)$ and $\mathcal{B}(Q_1) \otimes \mathcal{B}(Q_2)$. The last rule of Figure 10 is a contextual rule which holds for any evaluation context E. Evaluation contexts are defined by the following grammar:

$$
\begin{align*}
E &:= [\dots] \mid E \otimes N \mid V \otimes E \mid \text{let } x \otimes y = E \text{ in } N \mid \text{inl}(E) \mid \text{inr}(E) \\
  &\quad | \text{case } E \text{ of } \{\text{inl}(x) \to M, \text{ inr}(y) \to N\} \mid \text{force}(E) \mid \text{succ}(E) \mid E N \\
  &\quad | V E \mid \text{meas}(E) \mid \mathcal{B}(u)(E) \mid \text{let } \mathcal{B}(z) = E \text{ in } N \mid \text{let } \mathcal{B}(x \otimes y) = E \text{ in } N
\end{align*}
$$

One of the premises of the contextual rule states that if $\sigma$ is a permutation which does not act on the same set of indices as $\sigma_1, \sigma_2$, then we can form a “union” of these permutations by composing an extension of the two. For a permutation $\sigma: S \to S$, we can define its extension $\sigma^{\text{ext}}: S \sqcup S' \to S \sqcup S'$ by $\sigma^{\text{ext}}(s) \triangleq \sigma(s)$, if $s \in S$, $\sigma^{\text{ext}}(s') \triangleq s'$, if $s' \in S'$. We now introduce the reduction relation we use to define the operational semantics.

**Definition 3.** The reduction relation $\cdot \rightsquigarrow \cdot$ ⊆ SVConf × [0, 1] × SVConf is defined in the following way: we write $(v, u_\sigma, M) \rightsquigarrow_p (v', u_{\sigma'}, M')$ whenever

$$
\frac{\cdot \vdash v = t : Q \qquad (t, u_\sigma, M) \to_p (t', u_{\sigma'}, M') \qquad \cdot \vdash t' = v' : Q'}{(v, u_\sigma, M) \rightsquigarrow_p (v', u_{\sigma'}, M')}
$$

The intuition behind the above definition is that it allows us to reason modulo equality of the pure terms $t$, as a consequence of Proposition 3.

3.3 Main properties

We show that well-formedness is preserved by the reduction relation $\cdot \rightsquigarrow \cdot$.

**Theorem 3 (Subject Reduction).** For a configuration $C_1 \in \text{WF}_{\text{svconf}}(A)$, if $C_1 \rightsquigarrow_p C_2$ for some probability $p \in [0, 1]$, then $C_2 \in \text{WF}_{\text{svconf}}(A)$.

Next, we show that progress and strong normalisation hold. More specifically, a well-formed semi-value configuration $C$ is either a value configuration or it reduces to a finite number of semi-value configurations with total probability 1, i.e. if we have not reached a normal form then the probability to be stuck is 0.
<figure><img src="image_6.png" /></figure>

$$ (\mathbf{t}, u_{\sigma}, \text{case inl}(V) \text{ of } \{\text{inl}(x) \to M, \text{ inr}(y) \to N\}) \to_1 (\mathbf{t}, u_{\sigma}, M[V/x]) $$

$$ (\mathbf{t}, u_{\sigma}, \text{case inr}(V) \text{ of } \{\text{inl}(x) \to M, \text{ inr}(y) \to N\}) \to_1 (\mathbf{t}, u_{\sigma}, N[V/y]) $$

$$ (\mathbf{t}, u_{\sigma}, \text{let } x \otimes y = V \otimes W \text{ in } M) \to_1 (\mathbf{t}, u_{\sigma}, M[V/x, W/y]) $$

$$ (\mathbf{t}, u_{\sigma}, \text{force}(\text{lift}(M))) \to_1 (\mathbf{t}, u_{\sigma}, M) $$

$$ (\mathbf{t}, u_{\sigma}, (\lambda x.M)V) \to_1 (\mathbf{t}, u_{\sigma}, M[V/x]) $$

$$ (\mathbf{t}, u_{\sigma}, \text{match zero with } \{\text{zero} \to M, \text{succ}(x) \to N\}) \to_1 (\mathbf{t}, u_{\sigma}, M) $$

$$ (\mathbf{t}, u_{\sigma}, \text{match succ}(V) \text{ with } \{\text{zero} \to M, \text{succ}(x) \to N\}) \to_1 (\mathbf{t}, u_{\sigma}, N[V/x]) $$

$$ (\mathbf{t}, u_{\sigma}, \text{pure}(\mathbf{t}')) \to_1 (\mathbf{t} \otimes \mathbf{t}', u_{\sigma_{swap}} \circ (u_{\sigma} \otimes u_{id}), x) $$

$$ (\Sigma_i p_i \cdot \Sigma_j \alpha_{ij} \cdot \mathbf{b}'_{ij} \otimes \cdots \otimes \mathbf{b}_i \otimes \cdots, u_{\sigma_s}, \text{meas}(x)) \to_{|p_k|^2} (\Sigma_j \alpha_{kj} \cdot \mathbf{b}'_{kj} \otimes \cdots, u_{id}, \bar{\mathbf{b}}_k) $$

$$ (\mathbf{t}, u_{\sigma}, \mathcal{B}(u)(z)) \to_1 ((u_{\sigma}^{*} \circ (u \otimes id) \circ u_{\sigma}) \mathbf{t}, u_{\sigma}, z) $$

$$ (\mathbf{t}, u_{\sigma}, \text{let } \mathcal{B}(z) = x \otimes y \text{ in } N) \to_1 (\mathbf{t}, u_{\sigma_{gather}} \circ u_{\sigma}, N) $$

$$ (\mathbf{t}, u_{\sigma}, \text{let } \mathcal{B}(x \otimes y) = z \text{ in } N) \to_1 (\mathbf{t}, u_{\sigma_{divide}} \circ u_{\sigma}, N) $$

$$ (\mathbf{t}_1, u_{\sigma_1^{\text{ext}}, M_1}) \to_p (\mathbf{t}_2, u_{\sigma_2^{\text{ext}}, M_2}) \quad \text{dom}(\sigma) \cap (\text{dom}(\sigma_1) \cup \text{dom}(\sigma_2)) = \emptyset $$

$$ (\mathbf{t}_1, u_{\sigma^{\text{ext}} \circ \sigma_1^{\text{ext}}, E[M_1]}) \to_p (\mathbf{t}_2, u_{\sigma^{\text{ext}} \circ \sigma_2^{\text{ext}}, E[M_2]}) $$

<caption>Fig. 10: Reduction rules and their unitary permutations.</caption>

**Theorem 4 (Progress).** If $C \in \text{WF}_{\text{svconf}}(A)$, then either $C \in \text{VConf}$, or there exists $C_i \in \text{WF}_{\text{svconf}}(A)$ such that $C \rightsquigarrow_{p_i} C_i$. Moreover, if $\{C_i\}_{i \in I}$ is the set of all such distinct (not $\alpha$-equivalent) configurations, then $I$ is finite, and $\sum_i p_i = 1$.

**Theorem 5 (Strong Normalisation).** For a configuration $C \in \text{WF}_{\text{svconf}}(A)$, there is no infinite sequence of reductions $C \rightsquigarrow_{p_0} C_1 \rightsquigarrow_{p_1} C_2 \rightsquigarrow_{p_2} \cdots$.
## 3.4 Illustrating Example: Quantum Walk Search

Given a graph with some marked vertices, a quantum walk search is the quantum analogue of a random walk [4], which looks for these marked vertices. Each node in the graph represents the state of two quantum registers. A condition on the application of a coin operator on the first register decides the direction in which a walker should take the next step. A step in this direction is represented by the application of a unitary on the second register. After a given number of steps, measurement is performed on the second register to reveal whether the walker has arrived on a marked node. Here, we present a k-step quantum walk on a cycle with 10 nodes for simplicity in our language. Representing the second register with qubits, in this case, would require 4 qubits, whereas we represent the state of the second register with a single qnat. In the unitary CNOT$_{qnat}$ below, we use some (hopefully obvious) syntactic sugar with the expressions involving n in order to avoid writing all the cases; the letter n here should not be seen as a variable.

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

We define the unitary S corresponding to one step of the walk as $S \triangleq \text{CNOT}_{\text{qnat}} \circ (\text{Had} \otimes \text{Id})$. Finally, the k-step walk can be represented in our language as follows, where $S^k$ represents k compositions of S with itself:

$$ \text{walk} : (\mathcal{B}(\text{qbit} \otimes \text{qnat}) \to \text{qbit} \otimes \text{Nat}) \\ \text{walk} \triangleq \lambda z.\text{let } \mathcal{B}(x_1 \otimes x_2) = \mathcal{B}(S^k)(z) \text{ in } x_1 \otimes \text{meas}(x_2) $$

## 3.5 Denotational Semantics: Soundness and Adequacy

In this section we describe the denotational semantics of the main calculus. Figure 11 succinctly describes the interaction between the pure fragment and the mixed fragment. We present the functor which facilitates the main contribution of the paper, i.e combining quantum and classical control.

The $\mathcal{B}$ functor. In order to model the interaction between the pure quantum subsystem and the main calculus, we define the functor $\mathcal{B}: \text{Isometry} \to \text{NCPSU}$, mapping a Hilbert space $H$ to $\mathcal{B}(H)$. For an isometry $f: H_1 \to H_2$, the map $(f^* \circ (-) \circ f)$ is an NCPSU morphism $\mathcal{B}(H_2) \to \mathcal{B}(H_1)$, so by defining $\mathcal{B}(f) \triangleq (f^* \circ (-) \circ f)^{op}$, we get that $\mathcal{B}(f): \mathcal{B}(H_1) \to \mathcal{B}(H_2)$ in NCPSU. We remark that this functor restricts to a functor $\mathcal{B}: \text{Unitary} \to \text{NMIU}$ and we show that the functor $\mathcal{B}: \text{Isometry} \to \text{NCPSU}$ is strict monoidal.

<figure><img src="image_8.png" /><figcaption>Fig. 11: Categorical relations.</figcaption></figure>
$$ 
\begin{align*}
& [[!\Delta \vdash \text{pure}(t) : \mathcal{B}(Q)]] \triangleq \mathcal{B}[t] \circ \diamond!\Delta \\
& [[\Delta \vdash \text{meas}(M) : \bar{Q}]] \triangleq m^Q \circ [[\Delta \vdash M : \mathcal{B}(Q)]] \\
& [[\Delta \vdash \mathcal{B}(u)(M) : \mathcal{B}(Q_2)]] \triangleq \mathcal{B}[u] \circ [[\Delta \vdash M : \mathcal{B}(Q_1)]
\end{align*}
$$

<caption>Fig. 12: Interpretation of typing judgements (an excerpt).</caption>

**Interpretation of Types.** We interpret types as von Neumann algebras. The types corresponding to a linear call-by-value lambda-calculus are interpreted in the standard way: $[[I]] \triangleq \mathbb{C}$, $[[A+B]] \triangleq [[A]] \oplus [[B]]$, $[[A \otimes B]] \triangleq [[A]] \otimes [[B]]$, $[[!A]] \triangleq [[!A]]$ and $[[A \to B]] \triangleq [[A]] \to [[B]]$. The type for natural numbers is interpreted as the commutative von Neumann algebra $\ell^\infty(\mathbb{N})$, i.e $[[\text{Nat}]] \triangleq \ell^\infty(\mathbb{N})$. Finally, the interpretation of the type $\mathcal{B}(Q)$ uses the $\mathcal{B}$ functor that allows us to incorporate pure quantum primitives into our semantics, i.e $[[\mathcal{B}(Q)]] \triangleq \mathcal{B}[Q]$.

**Interpretation of Typing judgements.** A typing judgment of the form $\Delta \vdash M : A$ is interpreted as a morphism $[[\Delta \vdash M : A]] : [[\Delta]] \to [[A]]$ in NCPSU and we often abbreviate this by writing $[[M]]$. An excerpt of the interpretation is defined in Figure 12.

**Theorem 6.** For every pure quantum type $Q$, there exist a set $X$, an NMIU isomorphism $\alpha_{\bar{Q}} : [[\bar{Q}]] \cong \ell^\infty(X)$, and an isometric isomorphism $\beta_Q : [[Q]] \cong \ell^2(X)$. Moreover, $\forall \mathbf{b} \in \mathbf{Basis \ Terms}$, $\exists x \in X \text{ s.t. } \beta_Q(\llbracket \mathbf{b} \rrbracket) = \alpha_{\bar{Q}}(\llbracket \bar{\mathbf{b}} \rrbracket) = |x\rangle$.

Using the above theorem, measurement is interpreted as the map $m^Q : \mathcal{B}([Q]) \to [Q]$ defined as $m^Q \triangleq \alpha_{\bar{Q}}^{op} \circ m_X^{op} \circ \mathcal{B}(\beta_Q)$.

**Interpretation of Configurations.** A well-formed configuration $(t, u_\sigma, M)$ with $\vdash t : Q, \vdash u_\sigma : (Q, Q'_1 \otimes \dots \otimes Q'_m)$, and $x_1 : \mathcal{B}(Q'_1), \dots, x_m : \mathcal{B}(Q'_m) \vdash M : A$ is interpreted as the NCPSU morphism

$$ [[(t, u_\sigma, M) : A]] \triangleq \left( \mathbb{C} \xrightarrow{\mathcal{B}([u_\sigma t])} \begin{array}{c} \mathcal{B}(Q'_1 \otimes \dots \otimes Q'_m) \\ \parallel \\ \mathcal{B}(Q'_1) \otimes \dots \otimes \mathcal{B}(Q'_m) \end{array} \xrightarrow{[[M]]} A \right). $$

We can now show that our semantic interpretation is sound with respect to single-step reduction.

**Theorem 7 (Soundness).** For $C \in \text{WF}_{svconf}(A)$, if $C \notin \text{VConf}$, then

$$ [[C : A]] = \sum_{C \rightsquigarrow_p C'} p[[C' : A]], $$

where the sum ranges over all possible reducts $C \rightsquigarrow_p C'$.

Next, we can show that our interpretation is sound in a big-step sense as well, which follows easily using the previous result and strong normalisation.
**Theorem 8 (Strong Adequacy).** For $C \in \text{WF}_{\text{SVconf}}(A)$,

$$ \llbracket C \rrbracket = \sum_{V \in \text{VConf}} P(C \to_* V) \llbracket V \rrbracket, $$

where $P(C \to_* V)$ indicates the overall probability that $C$ reduces to $V$.

This implies that, for any well-formed configuration $C$, its interpretation $\llbracket C \rrbracket$ is an NCPU map (i.e., it is not merely subunitary) and therefore it corresponds to a quantum channel in the Heisenberg picture of quantum mechanics.

# 4 Conclusion and Perspectives

We described a programming language which has support for both pure state quantum computation and mixed state quantum computation. We began by describing the pure quantum subsystem (§2), for which we introduced an equational theory and proved its completeness w.r.t. the denotational semantics (§2.4). Then, we described the main calculus (§3.1) which uses a new adaptation of quantum configurations (§3.2), which we used to define the operational semantics of the language. Here, the interaction between the pure quantum subsystem and the main calculus becomes apparent. We showed that our denotational semantics (§3.5) has a clear and appropriate interpretation as channels in the Heisenberg picture of quantum mechanics and we showed it is sound and adequate with respect to the operational semantics (§3.5).

Although our language has support for Nat, an inductive type, an obvious extension would be to include more general inductive types. Additionally, support for higher-order pure quantum computation is another feature that would be interesting to add in a future work.

Another matter that could be tackled as future work is recursion. In the pure system, adding general recursion is an open and difficult problem [14, Section 5.2]. In the main calculus, our denotational model supports recursion for first-order quantum functions [17,13]. However, our model does not support general recursion when quantum lambda abstractions are involved. There are other denotational models that support general recursion and quantum lambda abstractions, but they do not support types like qnat that correspond to $\ell^2(\mathbb{N})$, instead they support recursive types that intuitively correspond to infinite classical combinations of spaces involving finite-dimensional Hilbert spaces, which is not the same as $\ell^2(\mathbb{N})$. A model for quantum lambda abstractions, qnat and general recursion is an open problem to the best of our knowledge.

# Acknowledgements

The authors would like to thank Benoît Valiron for helpful comments and discussions. Louis Lemonnier's research was funded by the Engineering and Physical Sciences Research Council (EPSRC) under project EP/X025551/1 "Rubber DUQ: Flexible Dynamic Universal Quantum programming". This work is also supported by the HORIZON 2020 project NEASQC, by the Inria associate team TC(Pro)³, by the PEPR integrated project EPiQ ANR-22-PETQ-0007, and by the HQI initiative ANR-22-PNCQ-0002.
References

1. Andrés-Martínez, P.: Unbounded loops in quantum programs: categories and weak-while loops. Ph.D. thesis, Laboratory for Foundations of Computer Science, School of Informatics, University of Edinburgh (2022). https://doi.org/https://doi.org/10.48550/arXiv.2212.05371

2. Arrighi, P., Dowek, G.: Linear-algebraic lambda-calculus. Log. Methods Comput. Sci. 13(1) (2017). https://doi.org/10.23638/LMCS-13(1:8)2017, https://doi.org/10.23638/LMCS-13(1:8)2017

3. Chardonnet, K.: Towards a Curry-Howard Correspondence for Quantum Computation. (Vers une correspondance de Curry-Howard pour le calcul quantique). Ph.D. thesis, Université Paris-Saclay, France (2023), https://tel.archives-ouvertes.fr/tel-03959403

4. Childs, A.M., Cleve, R., Deotto, E., Farhi, E., Gutmann, S., Spielman, D.A.: Exponential algorithmic speedup by a quantum walk. In: Proceedings of the thirty-fifth annual ACM symposium on Theory of computing. pp. 59–68 (2003)

5. Cho, K.: Semantics for a quantum programming language by operator algebras. Electronic Proceedings in Theoretical Computer Science 172, 165–190 (Dec 2014). https://doi.org/10.4204/eptcs.172.12, http://dx.doi.org/10.4204/EPTCS.172.12

6. Cho, K., Westerbaan, A.: Von Neumann Algebras form a Model for the Quantum Lambda Calculus (2016). https://doi.org/https://doi.org/10.48550/arXiv.1603.02133

7. Clairambault, P., de Visme, M.: Full abstraction for the quantum lambda-calculus. Proc. ACM Program. Lang. 4(POPL), 63:1–63:28 (2020). https://doi.org/10.1145/3371131, https://doi.org/10.1145/3371131

8. Clairambault, P., de Visme, M., Winskel, G.: Game semantics for quantum programming. PACMPL 3(POPL), 32:1–32:29 (2019). https://doi.org/10.1145/3290345

9. Díaz-Caro, A., Malherbe, O.: Semimodules and the (syntactically-)linear lambda calculus. CoRR abs/2205.02142 (2022). https://doi.org/10.48550/ARXIV.2205.02142, https://doi.org/10.48550/arXiv.2205.02142

10. Díaz-Caro, A., Guillermo, M., Miquel, A., Valiron, B.: Realizability in the unitary sphere. In: LICS 2019. IEEE (jun 2019). https://doi.org/10.1109/lics.2019.8785834, https://doi.org/10.1109/2Flics.2019.8785834

11. Díaz-Caro, A., Malherbe, O.: Quantum control in the unitary sphere: Lambdals1 and its categorical model. Logical Methods in Computer Science Volume 18, Issue 3 (2022). https://doi.org/10.46298/lmcs-18(3:32)2022, https://doi.org/10.46298/2Flmcs-18%283%3A32%292022

12. Green, A.S., Lumsdaine, P.L., Ross, N.J., Selinger, P., Valiron, B.: Quipper: a scalable quantum programming language. In: Proceedings of the 34th ACM SIGPLAN conference on Programming language design and implementation. pp. 333–342 (2013)

13. Jia, X., Kornell, A., Lindenhovius, B., Mislove, M.W., Zamdzhiev, V.: Semantics for variational quantum programming. In: POPL 2022. vol. 6, pp. 1–31. ACM (2022). https://doi.org/10.1145/3498687

14. Lemonnier, L.: The Semantics of Effects : Centrality, Quantum Control and reversible Recursion. Theses, Université Paris-Saclay (Jun 2024), https://theses.hal.science/tel-04625771
15. Pagani, M., Selinger, P., Valiron, B.: Applying quantitative semantics to higher-order quantum computing. In: POPL 2014. pp. 647–658. ACM (2014). https://doi.org/10.1145/2535838.2535879

16. Paykin, J., Rand, R., Zdancewic, S.: Qwire: a core language for quantum circuits. ACM SIGPLAN Notices 52(1), 846–858 (2017)

17. Péchoux, R., Perdrix, S., Rennela, M., Zamdzhiev, V.: Quantum programming with inductive datatypes: Causality and affine type theory. In: FoSSaCS 2020. Lecture Notes in Computer Science, vol. 12077, pp. 562–581. Springer (2020). https://doi.org/10.1007/978-3-030-45231-5_29

18. Sabry, A., Valiron, B., Vizzotto, J.K.: From symmetric pattern-matching to quantum control. In: FoSSaCS 2018). Lecture Notes in Computer Science, vol. 10803, pp. 348–364. Springer (2018). https://doi.org/10.1007/978-3-319-89366-2_19

19. Selinger, P.: Towards a quantum programming language. Mathematical Structures in Computer Science 14(4), 527–586 (2004). https://doi.org/10.1017/S0960129504004256

20. Selinger, P., Valiron, B.: A lambda calculus for quantum computation with classical control. Mathematical Structures in Computer Science 16(3), 527–552 (2006). https://doi.org/10.1017/S0960129506005238

21. Selinger, P., Valiron, B., et al.: Quantum lambda calculus. Semantic techniques in quantum computation pp. 135–172 (2009)

22. Tsukada, T., Asada, K.: Enriched presheaf model of quantum FPC. Proc. ACM Program. Lang. 8(POPL), 362–392 (2024). https://doi.org/10.1145/3632855, https://doi.org/10.1145/3632855

23. Valiron, B.: Semantics of quantum programming languages: Classical control, quantum control. Journal of Logical and Algebraic Methods in Programming 128 (2022). https://doi.org/10.1016/j.jlamp.2022.100790

24. de Visme, M.: Quantum Game Semantics. (Sémantique des Jeux Quantique). Ph.D. thesis, University of Lyon, France (2020), https://tel.archives-ouvertes.fr/tel-03045844

25. Voichick, F., Li, L., Rand, R., Hicks, M.: Qunity: A unified language for quantum and classical computing. Proc. ACM Program. Lang. 7(POPL), 921–951 (2023). https://doi.org/10.1145/3571225, https://doi.org/10.1145/3571225