# Circuit Width Estimation via Effect Typing and Linear Dependency

Andrea Colledan, Ugo Dal Lago

► To cite this version:

Andrea Colledan, Ugo Dal Lago. Circuit Width Estimation via Effect Typing and Linear Dependency. ESOP 2024 - 33rd European Symposium on Programming, Apr 2024, Luxembourg, Luxembourg. pp.3 - 30, 10.1007/978-3-031-57267-8_1 . hal-04836016

HAL Id: hal-04836016

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

Submitted on 13 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
# Circuit Width Estimation via Effect Typing and Linear Dependency

Andrea Colledan<fnref n="1" />,<fnref n="2" />✉ and Ugo Dal Lago<fnref n="1" />,<fnref n="2" />✉

**Abstract.** Circuit description languages are a class of quantum programming languages in which programs are classical and produce a *description* of a quantum computation, in the form of a *quantum circuit*. Since these programs can leverage all the expressive power of high-level classical languages, circuit description languages have been successfully used to describe complex and practical quantum algorithms, whose circuits, however, may involve many more qubits and gate applications than current quantum architectures can actually muster. In this paper, we present *Proto-Quipper-R*, a circuit description language endowed with a linear dependent type-and-effect system capable of deriving parametric upper bounds on the width of the circuits produced by a program. We prove both the standard type safety results and that the resulting resource analysis is correct with respect to a big-step operational semantics. We also show that our approach is expressive enough to verify realistic quantum algorithms.

**Keywords:** Effect Typing · Lambda Calculus · Quantum Computing · Quipper

## 1 Introduction

With the promise of providing efficient algorithmic solutions to many problems [11,27,31], some of which are traditionally believed to be intractable [54], quantum computing is the subject of intense investigation by various research communities within computer science, not least that of programming language theory [24,43,51]. Various proposals for idioms capable of tapping into this new computing paradigm have appeared in the literature since the late 1990s. Some of these approaches turn out to be fundamentally new [1,49,52], while many others are strongly inspired by classical languages and traditional programming paradigms [44,48,53,63].

One of the major obstacles to the practical adoption of quantum algorithmic solutions is the fact that despite huge efforts by scientists and engineers alike, it seems that reliable quantum hardware, contrary to classical one, does not scale too easily: although quantum architectures with up to a couple hundred qubits have recently seen the light [9,10,38], it is not yet clear whether the so-called quantum advantage [45] is a concrete possibility, given the tremendous challenges posed by the quantum decoherence problem [50].

<footnote n="1">¹ University of Bologna, Bologna, Italy</footnote>

<footnote n="2">² INRIA Sophia Antipolis, Valbonne, France
{andrea.colledan,ugo.dallago}@unibo.it</footnote>
This entails that software which makes use of quantum hardware must be designed with great care: whenever part of a computation has to be run on quantum hardware, the amount of resources it needs, and in particular the amount of qubits it uses, should be kept to a minimum. More generally, a fine control over the low-level aspects of the computation, something that we willingly abstract from when dealing with most forms of classical computation, should be exposed to the programmer in the quantum case. This, in turn, has led to the development and adoption of many domain-specific programming languages and libraries in which the programmer explicitly manipulates qubits and quantum circuits, while still making use of all the features of a high-level classical programming language. This is the case of the Qiskit and Cirq libraries [17], but also of the Quipper language [25,26].

At the fundamental level, Quipper is a circuit description language embedded in Haskell. Because of this, Quipper inherits all the expressiveness of the high level, higher-order functional programming language that is its host, but for the same reason it also lacks a formal semantics. Nonetheless, over the past few years, a number of calculi, collectively known as the Proto-Quipper language family, have been developed to formalize interesting fragments and extensions of Quipper in a type-safe manner [46,48]. Extensions include, among others, dynamic lifting [8,21,35] and dependent types [20,22], but resource analysis is still a rather unexplored research direction in the Proto-Quipper community [56].

The goal of this work is to show that type systems indeed enable the possibility of reasoning about the size of the circuits produced by a Proto-Quipper program. Specifically, we show how linear dependent types in the style of Gaboardi and Dal Lago [12,14,15,23] can be adapted to Proto-Quipper, allowing to derive upper bounds on circuit widths that are parametric on the number of input wires to the circuit, be they classical or quantum. This enables a form of static analysis of the resource consumption of circuit families and, consequently, of the quantum algorithms described in the language. Technically, a key ingredient of this analysis, besides linear dependency, is a novel form of effect typing in which the quantitative information coming from linear dependency informs the effect system and allows it to keep circuit widths under control.

The rest of the paper is organized as follows. Section 2 informally explores the problem of estimating the width of circuits produced by Quipper, while also introducing the language. Section 3 provides a more formal definition of the Proto-Quipper language. In particular, it gives an overview of the system of simple types due to Rios and Selinger [46], which however is not meant to reason about the size of circuits. We then move on to the most important technical contribution of this work, namely the linear dependent and effectful type system, which is introduced in Section 4 and proven to guarantee both type safety and a form of total correctness in Section 5. Section 6 is dedicated to an example of a practical application of our type and effect system, that is, a program that builds the Quantum Fourier Transform (QFT) circuit [11,39] and which is verified to do so without any ancillary qubits.
To conclude this introduction, we wish to emphasize that while it is true
that quantum computing can be a difficult and intimidating subject, the class
of languages analyzed in this work focuses on circuit construction, which is an
entirely classical process, paying little to no concern to the actual quantum
semantics of circuit execution. Because of this, and due to space constraints,
we refrain from providing a general introduction to quantum computing in this
paper. Instead, we refer the interested reader to the excellent works of Nielsen
and Chuang [39], Yanofsky and Mannucci [60], and Mingsheng [61].

## 2 An Overview on Circuit Width Estimation

Quipper allows programmers to describe quantum circuits in a high-level and elegant way, using both gate-by-gate and circuit transformation approaches. Quipper also supports hierarchical and parametric circuits, thus promoting a view in which circuits become first-class citizens. Quipper has been shown to be scalable, in the sense that it has been effectively used to describe complex quantum algorithms that easily translate to circuits involving trillions of gates applied to millions of qubits. The language allows the programmer to optimize the circuit, e.g. by using ancilla qubits for the sake of reducing the circuit depth, or recycling qubits that are no longer needed.

One feature that Quipper lacks is a methodology for statically proving that important parameters — such as the width — of the underlying circuit are below certain limits, which of course would need to be parametric on the input size of the circuit. If this kind of analysis were available, then it would be possible to derive bounds on the number of qubits needed to solve any instance of a problem, and ultimately to know in advance how big of an instance can be possibly solved given a fixed amount of qubits.

In order to illustrate the kind of scenario we are reasoning about, this section offers some simple examples of Quipper programs, showing in what sense we can think of capturing the quantitative information that we are interested in through types and effect systems and linear dependency. We proceed at a very high level for now, without any ambition of formality.

Let us start with the example of Figure 1. The Quipper function on the left builds the structure on the right, which we call a *quantum circuit*. For the purposes of this work, it suffices to say that horizontal lines represent qubits, while other symbols represent elementary operations applied to them, e.g. initializations, gate applications, and so on. Time flows from left to right. The specific circuit in Figure 1 consists in an (admittedly contrived) implementation of the quantum not operation. The `dumbNot` function implements negation using a controlled not gate and an ancillary qubit `a`, which is initialized and discarded within the body of the function. This qubit does not appear in the interface of the circuit, but it clearly adds to its overall width, which is 2.

Consider now the higher-order function in Figure 2. This function takes as input a circuit building function `f`, an integer `n` and describes the circuit obtained by applying `f`'s circuit `n` times to the input qubit `q`. It is easy to see that the
dumbNot :: Qubit -> Circ Qubit
dumbNot q = do
  a <- qinit True
  (q,a) <- controlled_not q a
  qdiscard a
return q

<figure><img src="image_2.png" /><figcaption>Fig. 1. A contrived implementation of the quantum not operation using an ancilla</figcaption></figure>

width of the circuit produced in output by *iter dumbNot* *n* is equal to 2, even though, overall, the number of qubits initialized during the computation is equal to *n*. The point is that each ancilla is created only *after* the previous one has been discarded, thus enabling a form of qubit recycling.

iter :: (Qubit -> Circ Qubit)
-> Int -> Qubit -> Circ Qubit
iter f 0 q = return q
iter f n q = do
  q <- f q
iter f (n-1) q

<figure><img src="image_3.png" /><figcaption>Fig. 2. A higher-order function which iterates a circuit-building function *f* on an input qubit *q* and the result of its application to the *dumbNot* function from Figure 1</figcaption></figure>

Is it possible to statically analyze the width of the circuit produced in output by *iter dumbNot* *n* so as to conclude that it is constant and equal to 2? What techniques can we use? Certainly, the presence of higher order types complicates an already non-trivial problem. The approach we propose in this paper is based on two ingredients. The first is the so-called effect typing [40]. In this context the effect produced by the program is nothing more than the circuit and therefore it is natural to think of an effect system in which the width of such circuit, and only that, is exposed. Therefore, the arrow type *A* → *B* should be decorated with an expression indicating the width of the circuit produced by the corresponding function when applied to an argument of type *A*. Of course, the width of an individual circuit is a natural number, so it would make sense to annotate the arrow with such a number. For technical reasons, however, it will also be necessary to keep track of another natural number, corresponding to the number of wire resources that the function captures from the surrounding environment. This necessity stems from a need to keep track of wires even in the presence of data hiding, and will be explained in further detail in Section 4.

Under these premises, the *dumbNot* function would receive type Qubit →<sub>2,0</sub> Qubit, meaning that it takes as input a qubit and produces a circuit of width 2 which outputs a qubit. Note that the second annotation is 0, since we do not capture anything from the function's environment, let alone a wire. Consequently,
because *iter* iterates in sequence and because the ancillary qubit in `dumbNot` can be reused, the type of *iter* `dumbNot n` would also be `Qubit →₂₀ Qubit`.

```
hadamardN :: [Qubit] -> Circ [Qubit]
hadamardN [] = return []
hadamardN (q:qs) = do
    q <- hadamard q
    qs <- hadamardN qs
return (q:qs)
```

```
q — [H] — q
qs₁ — [H] — qs₁
qs₂ — [H] — qs₂
```

<caption>**Fig. 3.** The `hadamardN` function implements a circuit family where circuits have width linear in their input size.</caption>

Let us now consider a slightly different situation, in which the width of the produced circuit is not constant, but rather increases proportionally to the circuit's input size. Figure 3 shows a `Quipper` function that returns a circuit on *n* qubits in which the Hadamard gate is applied to each qubit, a common preprocessing step in many quantum algorithms. It is obvious that this function works on inputs of arbitrary size, and therefore we can interpret it as a circuit family, parametrized on the length of the input list of qubits. This quantity, although certainly a natural number, is unknown statically and corresponds precisely to the width of the produced circuit. It is thus natural to wonder whether the kind of effect typing we briefly hinted at in the previous paragraph is capable of dealing with such a function. Certainly, the expressions used to annotate arrows cannot be, like in the previous case, mere *constants*, as they clearly depend on the size of the input list. Is there a way to reflect this dependency in types? Certainly, one could go towards a fully-fledged notion of dependent types, like the ones proposed in [22], but a simpler approach, in the style of Dal Lago and Gaboardi's linear dependent types [12,14,15,23] turns out to be enough for this purpose. This is precisely the route that we follow in this paper. In this approach, terms can indeed appear in types, but that is only true for a very restricted class of terms, disjoint from the ordinary ones, called *index terms*. As an example, the type of the function `hadamardN` above could become `List<Qubit> →<sub>i,0</sub> List<Qubit>`, where *i* is an *index variable*. The meaning of the type would thus be that `hadamardN` takes as input any list of qubits of length *i* and produces a circuit of width at most *i* which outputs *i* qubits. Indices are better explained in Section 4, but in general we can say that they consist of arithmetical expressions over natural numbers and index variables, and can thus express non-trivial dependencies between input sizes and corresponding circuit widths.
## 3 The Proto-Quipper Language

This section aims at introducing the Proto-Quipper family of calculi to the non-specialist, without any form of resource analysis. At its core, Proto-Quipper is a linear lambda calculus with bespoke constructs to build and manipulate circuits. Circuits are built as a side-effect of a computation, behind the scenes, but they can also appear and be manipulated as data in the language.

<table><caption>Fig. 4. The Proto-Quipper types</caption><tr><td>Types</td><td>TYPE A, B ::= 1 | w | !A | A ⊗ B | A ⊸ B | List A | Circ(T, U)</td></tr><tr><td>Parameter types</td><td>PTYPE P, R ::= 1 | !A | P ⊗ R | List P | Circ(T, U)</td></tr><tr><td>Bundle types</td><td>BTYPE T, U ::= 1 | w | T ⊗ U</td></tr></table>

The types of Proto-Quipper are given in Figure 4. Speaking at a high level, we can say that Proto-Quipper employs a linear-nonlinear typing discipline. In particular, $w \in \{\text{Bit}, \text{Qubit}\}$ is a wire type and is linear, while $\neg$ is the linear arrow constructor. A subset of types, called parameter types, represent the values of the language that are not linear and that can therefore be copied. Any term of type A can be lifted into a duplicable parameter of type $!A$ if its type derivation does not require the use of linear resources.

<table><caption>Fig. 5. The Proto-Quipper syntax</caption><tr><td>Terms</td><td>TERM M, N ::= V W | let ⟨x, y⟩ = V in M | force V | box<sub>T</sub> V<br>| apply(V, W) | return V | let x = M in N</td></tr><tr><td>Values</td><td>VAL V, W ::= * | x | ℓ | λx<sub>A</sub>.M | lift M | (ℓ, C, k) | ⟨V, W⟩<br>| nil | cons V W | fold V W</td></tr><tr><td>Wire bundles</td><td>BVAL ℓ, k ::= * | ℓ | ⟨ℓ, k⟩</td></tr></table>

The syntax of Proto-Quipper is given in Figure 5. At a very high level, we are dealing with an effectful lambda calculus with bespoke constructs for manipulating circuits. A return expression turns a value into a trivial computation, while a let expression is used to sequence computations. Note that let is associative and that return acts as its identity. Now, let us informally dissect the domain-specific aspects of this language, starting with the language of values. The constructs of greatest interest are labels and boxed circuits. A label $ℓ$ represents a reference to a free wire of the underlying circuit being built and is attributed a wire type $w \in \{\text{Bit}, \text{Qubit}\}$. Due to the no-cloning property of quantum states [39], labels have to be treated linearly. Arbitrary structures of labels form a subset of values which we call wire bundles and which are given bundle types. On the other hand, a boxed circuit $(\ell, C, k)$ represents a circuit object $C$ as
a datum within the language, together with its input and output interfaces $\bar{l}$ and $\bar{k}$. Such a value is given parameter type $\text{Circ}(T, U)$, where bundle types $T$ and $U$ are the input and output types of the circuit, respectively. Boxed circuits can be copied, manipulated by primitive functions and, more importantly, applied to the underlying circuit. This last operation, which lies at the core of Proto-Quipper's circuit-building capabilities, is possible thanks to the apply operator. This operator takes as first argument a boxed circuit $(\bar{l}, \bar{k})$ and appends $C$ to the underlying circuit $D$. How does apply know where exactly in $D$ to apply $C$? Thanks to a second argument: a bundle of wires $\bar{t}$ coming from the free output wires of $D$, which identify the exact location where $C$ is supposed to be attached.

The language is expected to be endowed with constant boxed circuits corresponding to fundamental gates and operations (e.g. Hadamard, CNOT, initialization, etc.), but the programmer can also introduce their own boxed circuits via the box operator. Intuitively, box takes as input a circuit-building function and executes it in a sandboxed environment, on dummy arguments, in a way that leaves the underlying circuit unchanged. Said function produces a standalone circuit $C$, which is then returned by the box operator as a boxed circuit $(\bar{l}, \bar{k})$.

Figure 6 shows the Proto-Quipper term corresponding to the Quipper program in Figure 1, as an example of the use of the language. Note that $\text{let } \langle x, y \rangle = M$ in $N$ is syntactic sugar for $\text{let } z = M$ in $\text{let } \langle x, y \rangle = z$ in $N$. The dumbNot function is given type Qubit $\to$ Qubit and builds the circuit shown in Figure 1 when applied to an argument.

$$ \begin{array}{l} \text{dumbNot} \triangleq \lambda q_{\text{Qubit}}. \text{let } a = \text{apply}(\text{INIT}_1, *) \text{ in} \\ \qquad \text{let } \langle q, a \rangle = \text{apply}(\text{CNOT}, \langle q, a \rangle) \text{ in} \\ \qquad \text{let } \_ = \text{apply}(\text{DISCARD}, a) \text{ in} \\ \qquad \text{return } q \end{array} $$

<caption>**Fig. 6.** An example Proto-Quipper program. $\text{INIT}_1$, CNOT and DISCARD are primitive boxed circuits implementing the corresponding elementary operations.</caption>

On the classical side of things, it is worth mentioning that Proto-Quipper as presented in this section does *not* support general recursion. A limited form of recursion on lists is instead provided via a primitive fold constructor, which takes as argument a (copiable) step function of type $!((B \otimes A) \to B)$, an initial value of type $B$, and constructs a function of type $\text{List } A \to B$. Although this workaround is not enough to recover the full power of general recursion, it appears that it is enough to describe many quantum algorithms. Figure 7 shows an example of the use of fold to reverse a list. Note that $\lambda \langle x, y \rangle_{A \otimes B}. M$ is syntactic sugar for $\lambda z_{A \otimes B}. \text{let } \langle x, y \rangle = z$ in $M$.
rev $\triangleq$ fold lift($\lambda\langle revList, q\rangle_{\text{List Qubit} \otimes \text{Qubit}}$.return (\text{cons } q \text{ revList})$) nil

**Fig. 7.** An example of the use of fold: the function that reverses a list

To conclude this section, we just remark how all of the **Quipper** programs shown in Section 2 can be encoded in **Proto-Quipper**. However, **Proto-Quipper**'s system of simple types in unable to tell us anything about the resource consumption of these programs. Of course, one could run **hadamardN** on a concrete input and examine the size of the circuit produced at run-time, but this amounts to *testing*, not *verifying* the program, and lacks the qualities of staticity and parametricity that we seek.

# 4 Incepting Linear Dependency and Effect Typing

We are now ready to expand on the informal definition of the **Proto-Quipper** language given in Section 3, to reach a formal definition of **Proto-Quipper-R**: a linearly and dependently typed language whose type system supports the derivation of upper bounds on the width of the circuits produced by programs.

## 4.1 Types and Syntax of **Proto-Quipper-R**

<table><caption>**Fig. 8.** **Proto-Quipper-R** syntax and types</caption><tr><td>Types</td><td>TYPE A, B ::= 1 | w | !A | A ⊗ B | A ↪<sub>I,J</sub> B | List<sup>I</sup> A | Circ<sup>I</sup>(T, U)</td></tr><tr><td>Param. types</td><td>PTYPE P, R ::= 1 | !A | P ⊗ R | List<sup>I</sup> P | Circ<sup>I</sup>(T, U)</td></tr><tr><td>Bundle types</td><td>BTYPE T, U ::= 1 | w | T ⊗ U | List<sup>I</sup> T</td></tr><tr><td>Terms</td><td>TERM M, N ::= V W | let ⟨x, y⟩ = V in M | force V | box<sub>T</sub> V<br>| apply(V, W) | return V | let x = M in N</td></tr><tr><td>Values</td><td>VAL V, W ::= * | x | ℓ | λx<sub>A</sub>.M | lift M | (ℓ, C, k) | ⟨V, W⟩<br>| nil | cons V W | fold<sub>i</sub> V W</td></tr><tr><td>Wire bundles</td><td>BVAL <sub>ℓ, k</sub> ::= * | ℓ | ⟨ℓ, k⟩ | nil | cons <sub>ℓ</sub> <sub>k</sub></td></tr><tr><td>Indices</td><td>INDEX I, J ::= i | n | I + J | I − J | I × J | max(I, J) | max<sub>i<i</sub></sub> J</td></tr></table>

The types and syntax of **Proto-Quipper-R** are given in Figure 8. As we mentioned, one of the key ingredients of our type system are the index terms with which we annotate standard **Proto-Quipper** types. These indices provide quantitative information about the elements of the resulting types, in a manner reminiscent of refinement types [18,47]. In our case, we are primarily concerned with
circuit width, which means that the natural starting point of our extension of Proto-Quipper is precisely the circuit type: $Circ^I(T, U)$ has elements the boxed circuits of input type $T$, output type $U$, and width bounded by $I$. Term $I$ is precisely what we call an index, that is, an arithmetical expression denoting a natural number. Looking at the grammar for indices, their interpretation is fairly straightforward, with a few notes: $n$ is a natural number, $i$ is an index variable, $I - J$ denotes *natural subtraction*, such that $I - J = 0$ whenever $I \le J$, and lastly $\max_{i < I} J$ is the maximum for $i$ going from 0 (included) to $I$ (excluded) of $J$, where $i$ can occur in $J$. Note that $I = 0$ implies $\max_{i < I} J = 0$. While the index in a circuit type denotes an upper bound, the index in a type of the form $List^I A$ denotes the *exact length* of the lists of that type. While this refinement might seem quite restrictive in a generic scenario, it allows us to include lists of labels among wire bundles, something that was not possible with simple lists. This is due to the fact that sized lists are effectively isomorphic to finite tensors, and therefore a sized list of labels represent a wire bundle of known size, whereas the same is not true for a simple list of labels. Lastly, as we anticipated in Section 2, an arrow type $A \stackrel{\circ}{\to}_{I,J} B$ is annotated with *two* indices: $I$ is an upper bound to the width of the circuit built by the function once it is applied to an argument of type $A$, while $J$ describes the exact number of wires captured in the function's closure. The utility of this last annotation will be clearer in Section 4.3.

The languages for terms and values are almost the same as in Proto-Quipper, with the minor difference that the fold operator now binds the index variable name $i$ within its first argument. This variable appears locally in the type of the step function, in such a way as to allow each iteration of the fold to contribute to the overall circuit width in a *different* way.

## 4.2 A Formal Language for Circuits

The type system of Proto-Quipper-R is designed to allow for reasoning about the width of circuits. Therefore, before we formally introduce the type system in Section 4.3, we ought to introduce circuits themselves in a formal way. So far, we have only spoken of circuits at a very high and intuitive level, and we have represented them only graphically. Looking at the circuits in Section 2, what do they have in common? At the fundamental level, they are made up of elementary operations applied to specific wires. Of course, the order of these operations matters, as does the order of wires that they are applied to. In the existing literature on Proto-Quipper, circuits are usually interpreted as morphisms in a symmetric monoidal category [46], but this approach makes it particularly hard to reason about their intensional properties, such as width. For this reason, we opt for a *concrete* model of wires and circuits, rather than an abstract one.

Luckily, we already have a datatype modeling ordered structures of wires, that is, the wire bundles that we introduced in the previous sections. We use them as the basis upon which we build circuits.

That being said, Figure 9 introduces the Circuit Representation Language (CRL) which we use as the target for circuit building in Proto-Quipper-R. Wire bundles are exactly as in Figure 8 and represent arbitrary structures of wires,
<table><caption>Fig. 9. CRL syntax and types</caption><tr><td>Wire bundles</td><td>BVAL</td><td>l&#773;, k&#773; ::= * | l | &lang;l&#773;, k&#773;&rang; | nil | cons l&#773; k&#773;</td></tr><tr><td>Bundle types</td><td>BTYPE T, U ::= 1 | w | T &otimes; U | List<sup>I</sup> T</td><td></td></tr><tr><td>Circuits</td><td>CIRC</td><td>C, D ::= id<sub>Q</sub> | C; g(l&#773;) &rarr; k&#773;</td></tr></table>

while circuits themselves are defined very simply as sequences of elementary operations applied to said structures. We call $Q$ a *label context* and define it as a mapping from label names to wire types. We use label contexts as a means to keep track of the set of labels available in a computation, alongside their respective types. Circuit $id_Q$ represents the identity circuit taking as input the labels in $Q$ and returning them unchanged, while $C; g(l&#773;)$ represents the application of the elementary operation $g$ to the wires identified by $l&#773;$ among the outputs of $C$. Operation $g$ outputs the wire bundle $k&#773;$, whose labels become part of the outputs of the overall circuit. Note that an “elementary operation” is usually the application of a gate, but it could also be a measurement, or the initialization or discarding of a wire. Although semantically very different, from the perspective of circuit building these operations are just elementary building blocks in the construction of a more complex structure, and it makes no sense to distinguish between them syntactically. Circuits are amenable to a form of concatenation. We write the *concatenation* of $C$ and $D$ as $C :: D$ and define it in the natural way, that is, as $C$ followed by all the operations occurring in $D$.

**Circuit Typing** Naturally, not all circuits built from the CRL syntax make sense. For example $id_{(l:Qubit)}; H(k) \rightarrow k$ and $id_{(l:Qubit)}; CNOT(\langle l, l \rangle) \rightarrow \langle k, t \rangle$ are both syntactically correct, but the first applies a gate to a non-existing wire, while the second violates the no-cloning theorem by duplicating $l$. To rule out such ill-formed circuits, we employ a rudimentary type system for circuits which allows us to derive judgments of the form $C: Q \rightarrow L$, which informally read “circuit $C$ is well-typed with input label context $Q$ and output label context $L$”.

The typing rules for CRL are given in Figure 10. We call $Q \vdash_w l&#773;: T$ a *wire judgment*, and we use it to give a structured type to an otherwise unordered label context, by means of a wire bundle. Most rules are straightforward, except those for lists, which rely on a judgment of the form $\vdash I = J$. This is to be intended as a semantic judgment asserting that $I$ and $J$ are closed and equal when interpreted as natural numbers. Within the rule, this reflects the idea that there are many ways to syntactically represent the length of a list. For example, `nil` can be given type `List<0 T>`, but also `List<1-1 T>` or `List<0×5 T>`. This kind of flexibility might seem unwarranted for such a simple language, but it is useful to effectively interface CRL and the more complex *Proto-Quipper-R*. Speaking of the actual circuit judgments, the `seq` rule tells us that the application of an elementary operation $g$ is well-typed whenever $g$ only acts on labels occurring in the outputs of $C$ (those in $l&#773;$, that is in $H$), produces in output labels that do not clash with the remaining outputs of $C$ (since $L, K$ denotes the disjoint
<figure><img src="image_4.png" /><figcaption>**Fig. 10.** The CRL type system</figcaption></figure>

union of the two label contexts) and is of the right type. This last requirement is expressed as $g \in \mathcal{G}(T, U)$, where $\mathcal{G}(T, U)$ is the subset of elementary operations that can be applied to an input of type $T$ to obtain an output of type $U$. For example, the Hadamard gate, which acts on a single qubit, is in $\mathcal{G}(\text{Qubit}, \text{Qubit})$.

**Circuit Width** Among the many properties of circuits, we are interested in width, so we conclude this section by giving a formal status to this quantity.

**Definition 1 (Circuit Width).** We define the width of a CRL circuit $C$, written width($C$), as follows

$$ width(id_Q) = |Q|, \qquad (1) $$

$$ width(C; g(\bar{l}) \to \bar{k}) = width(C) + \max(0, new(g) - discarded(C)), \quad (2) $$

where $|Q|$ is the number of labels in $Q$, $new(g)$ represents the net number of new wires initialized by $g$, and $discarded(C)$ is the number of wires that have been effectively discarded by the end of $C$, obtained as the difference between $C$'s width and the number of its outputs. Note that one expects $new(g)$ to be equal to the difference between the number of labels in $\bar{k}$ and those in $\bar{l}$. The overarching idea behind this definition is that whenever we require new wires in our computation, we first try to reuse as many previously discarded wires as possible. As long as we can do this ($new(g) \le$ discarded($C$)), the initializations do not add to the total width of the circuit. Otherwise ($new(g) >$ discarded($C$)) we must actually create new wires, increasing the overall width of the circuit.

Now that we have a formal definition of circuit types and width, we can state a fundamental property of the concatenation of well-typed circuits, which is illustrated in Figure 11 and proven in Theorem 1. We use this result pervasively in proving the correctness of **Proto-Quipper-R** in section 5.

**Theorem 1 (CRL).** Given $C: Q \to L, H$ and $D: H \to K$ such that the labels shared by $C$ and $D$ are all and only those in $H$, we have

$$ 1. C :: D : Q \to L, K, $$
2. width($C$ :: $D$) ≤ max(width($C$), width($D$) + $|L|$).

*Proof.* By induction of the derivation of $D: H \to K$.

<figure><img src="image_5.png" /><figcaption>Fig. 11. The kind of scenario described by Theorem 1</figcaption></figure>

## 4.3 Typing Programs

Going back to Proto-Quipper-R, we have already seen how the standard Proto-Quipper types are refined with quantitative information. However, decorating types is not enough for the purposes of width estimation. Recall that, in general, a Proto-Quipper program produces a circuit as a *side effect* of its evaluation. If we want to reason about the width of said circuit, it is not enough to rely on a regular linear type system, although dependent. Rather, we have to introduce the second ingredient of our analysis and turn to a *type-and-effect system* [40], revolving around a type judgment of the form

$$ \Theta; \Gamma; Q \vdash_c M : A; I, \qquad (3) $$

which intuitively reads “for all natural values of the index variables in $\Theta$, under typing context $\Gamma$ and label context $Q$, term $M$ has type $A$ and produces a circuit of width at most $I$”. Therefore, $\Theta$ is a collection of index variables which are universally quantified in the rest of the judgment, while $\Gamma$ is a typing context for parameter and linear variables alike. When a typing context contains exclusively parameter variables, we write it as $\Phi$. In this judgment, $I$ plays the role of an *effect annotation*, describing a relevant aspect of the side effect produced by the evaluation of $M$ (i.e. the width of the produced circuit). The attentive reader might wonder why this annotation consists only of one index, whereas when we discussed arrow types in previous sections we needed two. The reason is that the second index, which we use to keep track of the number of wires captured by a function, is redundant in a typing judgment where the same quantity can be inferred directly from the environments $\Gamma$ and $Q$. A similar typing judgment of the form $\Theta; \Gamma; Q \vdash_v V : A$ is introduced for values, which are effect-less.

The rules for deriving typing judgments are those in Figure 12, where $\Gamma_1, \Gamma_2$ denotes the union of two contexts with disjoint domains. A well-formedness judgment of the form $\Theta \vdash I$ means that all the free index variables occurring in $I$ are in $\Theta$. Well-formedness is lifted to types and typing contexts in the
<figure><img src="image_6.png" /><figcaption>Fig. 12. Proto-Quipper-R type system</figcaption></figure>
natural way. Among interesting typing rules, we can see how the *circ* rule bridges between CRL and Proto-Quipper-R. A boxed circuit ($\ell, C, k$) is well typed with type $\text{Circ}^I(T, U)$ when $C$ is no wider than the quantity denoted by $I, C: Q \to L$ and $\ell, k$ contain all and only the labels in $Q$ and $L$, respectively, acting as a language-level interface to $C$.

The two main constructs that interact with circuits are **apply** and **box**. The *apply* rule is the foremost place where effects enter the type derivation: $V$ represents some boxed circuit of width at most $I$, so its application to an appropriate wire bundle $W$ produces exactly a circuit of width at most $I$. The **box** rule, on the other hand, works approximately in the opposite direction. If $V$ is a circuit building function that, once applied to an input of type $T$, would build a circuit of output type $U$ and width at most $I$, then boxing it means turning it into a boxed circuit with the same characteristics. Note that the **box** rule requires that the typing context be devoid of linear variables. This reflects the idea that $V$ is meant to be executed in complete isolation, to build a standalone, replicable circuit, and therefore it should not capture any linear resource (e.g. a label) from the surrounding environment.

**Wire Count** Notice that many rules rely on an operator written `#(·)`, which we call the *wire count* operator. Intuitively, this operator returns the number of wire resources (in our case, bits or qubits) represented by a type or context. To understand how this is important, consider the *return* rule. The *return* operator turns a value $V$ into a trivial computation that evaluates immediately to $V$, and therefore it would be tempting to give it an effect annotation of 0. However, $V$ is not necessarily a closed value. In fact, it might very well contain many bits and qubits, coming both from the typing context $\Gamma$ and the label context $Q$. Although nothing happens to these bits and qubits, they still correspond to wires in the underlying circuit, and these wires have a width which must be accounted for in the judgment for the otherwise trivial computation. The *return* rule therefore produces an effect annotation of the form `#(Γ; Q)`, which is shorthand for `#(Γ) + #(Q)` and corresponds exactly to this quantity. A formal definition of the wire count operator on types is given in the following definition, which is lifted to contexts in the natural way.

**Definition 2 (Wire Count).** We define the wire count of a type $A$, written `#(A)$`, as a function `#(·)`: `TYPE` $\to$ `INDEX` such that

$$ \#(1) = \#(!A) = \#(\text{Circ}^I(T, U)) = 0, \qquad \#(w) = 1, $$

$$ \#(A \otimes B) = \#(A) + \#(B), \qquad \#(A \stackrel{\cdot}{\to}_{I,J} B) = J, \qquad \#(\text{List}^I A) = I \times \#(A). $$

This definition is fairly straightforward, except for the arrow case. By itself, an arrow type does not give us any information about the amount of qubits or bits captured in the corresponding closure. This is precisely where the second index $J$, which keeps track exactly of this quantity, comes into play. This annotation is introduced by the *abs* rule and allows our analysis to circumvent data hiding.
The *let* rule is another rule in which wire counts are essential. The two terms *M* and *N* in *let x = M in N* build the circuits *C*<sub>*M*</sub> and *C*<sub>*N*</sub>, whose widths are bounded by *I* and *J*, respectively. Once again, it might be tempting to conclude that the overall circuit built by the *let* construct has width bounded by *max(I, J)*, but this fails to take into account the fact that while *M* is building *C*<sub>*M*</sub> starting from the wires contained in Γ<sub>1</sub> and *Q*<sub>1</sub>, we must keep aside the wires contained in Γ<sub>2</sub> and *Q*<sub>2</sub>, which will be used by *N* to build *C*<sub>*N*</sub>. These wires must flow alongside *C*<sub>*M*</sub> and their width, i.e. #(*Γ*₂; *Q*₂), adds up to the total width of the left-hand side of the *let* construct, leading to an overall width upper bound of max(*I* + #(*Γ*₂; *Q*₂), *J*). This situation is better illustrated in Figure 13.

<figure><img src="image_7.png" /><figcaption>Fig. 13. The shape of a circuit built by a *let* construct</figcaption></figure>

The last rule that makes substantial use of wire counts is *fold*, arguably the most complex rule of the system. The main ingredient of the fold rule is the bound index variable *i*, which occurs in the accumulator type *B* and is used to keep track of the number of steps performed by the fold. Let $(\cdot)\{I/i\}$ denote the capture-avoiding substitution of the index term *I* for the index variable *i* inside an index, type, context, value or term, not unlike $(\cdot)[V/x]$ denotes the capture-avoiding substitution of the value *V* for the variable *x*. Intuitively, if the accumulator has initially type $B\{0/i\}$ and each application of the step function increases *i* by one, then when we fold over a list of length *I* we get an output of type $B\{I/i\}$. Index *E* is the upper bound to the width of the overall circuit built by the fold: if the input list is empty, then the width of the circuit is just the number of wires contained in the initial accumulator, that is, #(*I*; *Q*). If the input list is non-empty, on the other hand, things get slightly more complicated. At each step *i*, the step function builds a circuit $C_i$ of width bounded by *J*, where *J* might depend on *i*. This circuit takes as input all the wires in the accumulator, as well as the wires contained in the first element of the input list, which are #(*A*). The wires contained in remaining *I*−1−*i* elements have to flow alongside $C_i$, giving a width upper bound of *J* + (*I* − 1 − *i*) × #(*A*) at each step *i*. The overall width upper bound is then the maximum for *i* going from 0 to *I* − 1 of this quantity, i.e. precisely $\max_{i<j} J + (I - j) \times #(A)$. Once again, a graphical representation of this scenario is given in Figure 14.
<figure><img src="image_8.png" /><figcaption>Fig. 14. The shape of a circuit built by a fold applied to an input list of type `List<IB>`</figcaption></figure>

**Subtyping** Notice that Proto-Quipper-R's type system includes two subsumption rules, which are effectively the same rule for terms and values, respectively: `csub` and `vsub`. We mentioned that our type system resembles a refinement type system, and all such systems induce a subtyping relation between types, where `A` is a subtype of `B` whenever the former is “at least as refined” as the latter. In our case, a subtyping judgment such as `Θ ⊢_s A <: B` means that for all natural values of the index variables in `Θ`, `A` is a subtype of `B`.

$$ \text{unit} \xrightarrow{\Theta \vdash_s 1 <: 1} \text{wire} \xrightarrow{\Theta \vdash_s w <: w} \text{bang} \xrightarrow{\Theta \vdash_s A <: B} \Theta \vdash_s ! A <: ! B $$

$$ \text{tensor} \xrightarrow{\substack{\Theta \vdash_s A_1 <: A_2 \\ \Theta \vdash_s A_1 \otimes B_1 <: A_2 \otimes B_2}} \Theta \vdash_s A_1 \to_{I_1, J_1} B_1 <: A_2 \to_{I_2, J_2} B_2 $$

$$ \text{arrow} \xrightarrow{\substack{\Theta \vdash_s A_2 <: A_1 \\ \Theta \vdash_s B_1 <: B_2 \\ \Theta \vdash I_1 \le I_2 \\ \Theta \vdash J_1 = J_2}} \Theta \vdash_s A_1 \to_{I_1, J_1} B_1 <: A_2 \to_{I_2, J_2} B_2 $$

$$ \text{list} \xrightarrow{\substack{\Theta \vdash_s A <: B \\ \Theta \vdash I = J}} \Theta \vdash_s \text{List}^I A <: \text{List}^J B $$

$$ \text{circ} \xrightarrow{\substack{\Theta \vdash_s T_1 <: T_2 \\ \Theta \vdash_s U_1 <: U_2 \\ \Theta \vdash I \le J}} \Theta \vdash_s \text{Circ}^I(T_1, U_1) <: \text{Circ}^J(T_2, U_2) $$

<caption>Fig. 15. Proto-Quipper-R subtyping rules</caption>

We derive this kind of judgments by the rules in Figure 15. Note that $Θ ⊢_s A <: B$ is shorthand for $“Θ ⊢_s A <: B$ and $Θ ⊢_s B <: A”$. Subtyping relies in turn on a judgment of the form $Θ \vdash I \le J$, which is a generalization of the semantic judgment that we used in the CRL type system in Section 4.2. Such a judgment asserts that for all natural values of the index variables in `Θ`, `I` is
lesser or equal than $J$. Consequently, $\Theta \models I = J$ is shorthand for "$\Theta \models I \leq J$ and $\Theta \models J \leq I$". We purposefully leave the decision procedure of this kind of judgments unspecified, with the prospect that, from a more practical perspective, they could be delegated to an SMT solver [7].

## 4.4 Operational Semantics

Operationally speaking, it does not make sense, in the Proto-Quipper languages, to speak of the semantics of a term in isolation: a term is always evaluated in the context of an underlying circuit that supplies all of the term's free labels. We therefore define the operational semantics of Proto-Quipper-R as a big-step evaluation relation $\downarrow$ on configurations, i.e. circuits paired with either terms or values. Intuitively, $(C, M) \downarrow (\mathcal{D}, V)$ means that $M$ evaluates to $V$ and updates $C$ to $\mathcal{D}$ as a side effect.

$$
\begin{aligned}
app & \quad \frac{(C, M[V/x]) \downarrow (\mathcal{D}, W)}{(C, (\lambda x_A.M) V) \downarrow (\mathcal{D}, W)} & dest & \quad \frac{(C, M[V/x][W/y]) \downarrow (\mathcal{D}, X)}{(C, \text{let } (x, y) = (V, W) \text{ in } M) \downarrow (\mathcal{D}, X)} \\
force & \quad \frac{(C, M) \downarrow (\mathcal{D}, V)}{(C, \text{force}(\text{lift } M)) \downarrow (\mathcal{D}, V)} & apply & \quad \frac{(\mathcal{E}, \bar{q}) = \text{append}(C, \bar{l}, (\bar{l}, \mathcal{D}, \bar{k}))}{(C, \text{apply}((\bar{l}, \mathcal{D}, \bar{k}), \bar{l})) \downarrow (\mathcal{E}, \bar{q})} \\
box & \quad \frac{(Q, \bar{l}) = \text{freshlabels}(T)}{(C, \text{box}_T(\text{lift } M)) \downarrow (C, (\bar{l}, \mathcal{D}, \bar{k}))} & let & \quad \frac{(C, M) \downarrow (\mathcal{E}, V)}{(C, \text{let } x = M \text{ in } N) \downarrow (\mathcal{D}, W)} \\
return & \quad \frac{(C, \text{return } V) \downarrow (C, V)}{\text{fold-end}} & \frac{(C, (\text{fold}_i V W) \text{nil}) \downarrow (C, W)}{\text{fold-step}} & \quad \frac{(C, M\{0/i\}) \downarrow (C, Y)}{(\mathcal{E}, (\text{fold}_i (\text{lift } M\{i+1/i\}) Z) W') \downarrow (\mathcal{D}, X)} \\
& & & \quad \frac{(C, (\text{fold}_i (\text{lift } M) V) (\text{cons } W W')) \downarrow (\mathcal{D}, X)}{\text{fold-end}}
\end{aligned}
$$

<caption>**Fig. 16.** Proto-Quipper-R big-step operational semantics</caption>

The rules for evaluating configurations are given in Figure 16, where $C, \mathcal{D}$ and $\mathcal{E}$ are circuits, $M$ and $N$ are terms, while $V, W, X, Y$ and $Z$ are values. Most evaluation rules are straightforward, with the exception perhaps of *apply*, *box* and *fold-step*. Being the fundamental block of circuit-building, the semantics of *apply* lies almost entirely in the way it updates the underlying circuit. The concatenation of the underlying circuit $C$ and the applicand $\mathcal{D}$ is delegated entirely to the append function, which is given in Definition 4. Before we examine the append function, however, consider than when we deal with circuit objects we are not really interested in the concrete labels that occur in them, but rather
in the *structure* that they convey. For this reason, we introduce the following notion of *circuit equivalence*.

**Definition 3 (Circuit Equivalence).** We say that two boxed circuits $(\overline{\ell}, \mathcal{C}, \overline{k})$ and $(\tilde{t}, \mathcal{D}, \overline{q})$ are equivalent, and we write $(\overline{\ell}, \mathcal{C}, \overline{k}) \cong (\tilde{t}, \mathcal{D}, \overline{q})$, when there exists a renaming $\rho$ of labels such that $\rho(\overline{\ell}) = \tilde{t}$, $\rho(\overline{k}) = \overline{q}$ and $\rho(\mathcal{C}) = \mathcal{D}$.

We can now move on to the definition of append, where the notion of circuit equivalence is used to instantiate the generic input interface of a boxed circuit with the actual labels that it is going to be appended to, and to ensure that there are no name clashes between the appended circuit and the underlying circuit.

**Definition 4 (append).** We define the append of $(\overline{\ell}, \mathcal{D}, \overline{k})$ to $\mathcal{C}$ on $\tilde{t}$, written $\text{append}(\mathcal{C}, \tilde{t}, (\overline{\ell}, \mathcal{D}, \overline{k}))$, as the function that performs the following steps:

1. Finds $(\tilde{t}, \mathcal{D}', \overline{q}) \cong (\overline{\ell}, \mathcal{D}, \overline{k})$ such that the labels shared by $\mathcal{C}$ and $\mathcal{D}'$ are all and only those in $\tilde{t}$,

2. *Computes* $\mathcal{E} = \mathcal{C} :: \mathcal{D}'$,

3. *Returns* $(\mathcal{E}, \overline{q})$.

On the other hand, the semantics of a term of the form $\text{box}_T(\text{lift } M)$ relies on the freshlabels function. What freshlabels does is take as input a bundle type $T$ and instantiate fresh $Q, \overline{\ell}$ such that $Q \vdash_w \overline{\ell} : T$. The wire bundle $\overline{\ell}$ is then used as a dummy argument to $V$, the circuit-building function resulting from the evaluation of $M$. This function application is evaluated in the context of the identity circuit $id_Q$ and eventually produces a circuit $\mathcal{D}$, together with its output labels $\overline{k}$. Finally, $\overline{\ell}$ and $\overline{k}$ become respectively the input and output interfaces of the boxed circuit $(\overline{\ell}, \mathcal{D}, \overline{k})$, which is the result of the evaluation of $\text{box}_T(\text{lift } M)$.

Note, at this point, that $T$ controls how many labels are initialized by the freshlabels function. Because $T$ can contain indices (e.g. it could be that $T \equiv \text{List}^3 \text{Qubit}$), it follows that in Proto-Quipper-R indices are not only relevant to typing, but they also have operational value. For this reason, the semantics of Proto-Quipper-R is well-defined only on terms closed both in the sense of regular variables and index variables, since a circuit-building function of input type, say, List<^i Qubit does not correspond to any individual circuit, and therefore it makes no sense to box it. This aspect of the semantics is also apparent in the *fold-step* rule, where the index variable *i* occurring free in *M* is instantiated to 0 before evaluating *M* to obtain the step function *Y*. Then, before evaluating the next fold, *i* is replaced with *i* + 1 in *M*, increasing the index for the next iteration.

# 5 Type Safety and Correctness

Because the operational semantics of Proto-Quipper-R is based on configurations, we ought to adopt a notion of well-typedness which is also based on configurations. The following definition of *well-typed configuration* is thus central to our type-safety analysis.
**Definition 5 (Well-typed Configuration).** We say that configuration $(C, M)$ is well-typed with input $Q$, type $A$, width $I$ and output $L$, and we write $Q \vdash (C, M) : A; I; L$, whenever $C : Q \to L, H$ for some $H$ such that $\emptyset; \emptyset; H \vdash_c M : A; I$. We write $Q \vdash (C, V) : A; L$ whenever $C : Q \to L, H$ for some $H$ such that $\emptyset; \emptyset; H \vdash_v V : A$.

The three results that we want to show in this section are that any well-typed term configuration $Q \vdash (C, M) : A; I; L$ evaluates to some configuration $(\mathcal{D}, V)$, that $Q \vdash (\mathcal{D}, V) : A; L$ and that $\mathcal{D}$ is obtained from $C$ by extending it with a sub-circuit of width at most $I$. These claims correspond to the *subject reduction* and *total correctness* properties that we will prove at the end of this section. However, both these results rely on a central lemma and on the mutual notions of *realization* and *reducibility*, which we first give formally.

**Definition 6 (Realization).** We define $V \Vdash_Q A$, which reads $V$ realizes $A$ under $Q$, as the smallest relation such that

- $\ast \Vdash_\emptyset 1$,

- $\ell \Vdash_{\ell:w} w$,

- $V \Vdash_Q A \dashv_{\alpha} I, J$ $B$ iff $\vdash J = |Q|$ and $\forall W : W \Vdash_L A \implies VW \Vdash_{Q,L} I, B$,

- lift $M \Vdash_\emptyset! A$ iff $M \Vdash_\emptyset^0 A$,

- $\langle V, W \rangle \Vdash_{Q,L} A \otimes B$ iff $V \Vdash_Q A$ and $W \Vdash_L B$,

- nil $\Vdash_\emptyset$ List$^I$ $A$ iff $\vdash I = 0$,

- $\text{cons } V W \Vdash_{Q,L} \text{List}^I A$ iff $\vdash I = J + 1$ and $V \Vdash_Q A$ and $W \Vdash_L \text{List}^J A$,

- $(\bar{l}, \bar{c}, \bar{k}) \Vdash_\emptyset \text{Circ}^I(T, U)$ iff $\mathcal{C} : Q \to L$ and $Q \vdash_w \bar{l} : T$ and $L \vdash_w \bar{k} : U$ and $\vdash \text{width}(\mathcal{C}) \le I$.

**Definition 7 (Reducibility).** We say that $M$ is reducible under $Q$ with type $A$ and width $I$, and we write $M \Vdash_Q^I A$, if, for all $C$ such that $C : L \to Q, H$, there exist $\mathcal{D}, V$ such that

1. $(C, M) \Downarrow (C :: \mathcal{D}, V)$,

2. $\vdash \text{width}(\mathcal{D}) \le I$,

3. $\mathcal{D} : Q \to K$ for some $K$ such that $V \Vdash_K A$.

Both relations, and in particular reducibility, are given in the form of unary logical relations [55]. The intuition is pretty straightforward: a term is reducible with width $I$ if it evaluates correctly when paired with any circuit $C$ which provides its free labels and if it extends $C$ with a sub-circuit $\mathcal{D}$ whose width is bounded by $I$. Realization, on the other hand, is less immediate. For most cases, realizing type $A$ loosely corresponds to being closed and well-typed with type $A$, but a value realizes an arrow type $A \dashv_{\alpha} I, J$ $B$ when its application to a value realizing $A$ is reducible with type $B$ and width $I$.

By themselves, realization and reducibility are defined only on terms and values closed in the sense both of regular and index variables. To extend these notions to open terms and values, we adopt the standard approach of reasoning explicitly about the substitutions that would render them closed. A *closing value*
substitution $\gamma$ is a function that turns an open term $M$ into a closed term $\gamma(M)$ by substituting a value for each free variable occurring in $M$. We say that $\gamma$ implements a typing context $\Gamma$ using label context $Q$, and we write $\gamma \models_Q \Gamma$, when it replaces every variable $x_i$ in the domain of $\Gamma$ with a value $V_i$ such that $V_i \models_{Q_i} \Gamma(x_i)$ and $Q = \bigcup_{x_i \in \text{dom}(\Gamma)} Q_i$. A closing index substitution $\theta$ is similar, only it substitutes closed indices for index variables and can be applied to indices, types, contexts, values and terms alike. We say that $\theta$ implements an index context $\Theta$, and we write $\theta \models \Theta$, when it replaces every index variable in $\Theta$ with a closed index term. This allows us to give the following fundamental lemma, which will be used while proving all other claims.

**Lemma 1 (Core Correctness).** Let $\Pi$ be a type derivation. For all $\theta \models \Theta$ and $\gamma \models_Q \theta(\Gamma)$, we have that

$$ \Pi \triangleright \Theta; \Gamma; L \vdash_c M : A; I \implies \gamma(\theta(M)) \models_{Q,L}^{\theta(I)} \theta(A), \\ \Pi \triangleright \Theta; \Gamma; L \vdash_v V : A \implies \gamma(\theta(V)) \models_{Q,L} \theta(A). $$

*Proof.* By induction on the size of $\Pi$, making use of Theorem 1.

Lemma 1 tells us that any well-typed term (resp. value) is reducible (resp. realizes its type) when we instantiate its free variables according to its contexts. Now that we have Lemma 1, we can proceed to proving the aforementioned results of subject reduction and total correctness. We start with the former, which unsurprisingly requires the following substitution lemmata.

**Lemma 2 (Index Substitution).** Let $\Pi$ be a type derivation and let $I$ be an index such that $\Theta \vdash I$. We have that

$$ \Pi \triangleright \Theta, i; \Gamma; Q \vdash_c M : A; J \implies \Theta; \Gamma\{I/i\}; Q \vdash_c M\{I/i\} : A\{I/i\}; J\{I/i\}, \\ \Pi \triangleright \Theta, i; \Gamma; Q \vdash_v V : A \implies \Theta; \Gamma\{I/i\}; Q \vdash_v V\{I/i\} : A\{I/i\}. $$

*Proof.* By induction on the size of $\Pi$.

**Lemma 3 (Value Substitution).** Let $\Pi$ be a type derivation and let $V$ be a value such that $\Theta; \Phi, \Gamma_1; Q_1 \vdash_V V : A$. We have that

$$ \Pi \triangleright \Theta; \Phi, \Gamma_2, x : A; Q_2 \vdash_c M : B; I \implies \Theta; \Phi, \Gamma_1, \Gamma_2; Q_1, Q_2 \vdash_c M[V/x] : B; I, \\ \Pi \triangleright \Theta; \Phi, \Gamma_2, x : A; Q_2 \vdash_v W : B \implies \Theta; \Phi, \Gamma_1, \Gamma_2; Q_1, Q_2 \vdash_v W[V/x] : B. $$

*Proof.* By induction on the size of $\Pi$.

**Theorem 2 (Subject Reduction).** If $Q \vdash (C, M) : A; I; L$ and $(C, M) \Downarrow (D, V)$, then $Q \vdash (D, V) : A; L$.

*Proof.* By induction on the derivation of $(C, M) \Downarrow (D, V)$ and case analysis on the last rule used in its derivation. Lemma 3 is essential to the *app,dest* and *let* cases, while Lemma 2 is used in the *fold-step* case. Lemma 1 is essential to the *box* case, as it is the only case in which the side effect of the evaluation (the circuit built by the function being boxed), whose preservation is the a matter of correctness, becomes a value (the resulting boxed circuit).
Of course, type soundness is not enough: we also want the resource analysis
carried out by our type system to be correct, as stated in the following theorem.

**Theorem 3 (Total Correctness).** If $Q \vdash (C, M) : A; I; L$, then there exist $D, V$ such that $(C, M) \Downarrow (C :: D, V)$ and $\vdash \text{width}(D) \le I$.

*Proof.* By definition, $Q \vdash (C, M) : A; I; L$ entails that $C : Q \to L, H$ and $\emptyset; \emptyset; H \vdash_C M : A; I$. Since an empty context is trivially implemented by an empty closing substitution, by Lemma 1 we get $M \Vdash_H^I A$, which by definition entails that there exist $D, V$ such that $(C, M) \Downarrow (C :: D, V)$ and $\vdash \text{width}(D) \le I$.

6 A Practical Example

This section provides an example of how Proto-Quipper-R can be used to verify
the resource usage of realistic quantum algorithms. In particular, we use our
language to implement the QFT algorithm [11,39] and verify that the circuits it
produces have width no greater than the size of their input, i.e. that the QFT
algorithm does not overall use additional ancillary qubits.

```
qft    ≜ fold<sub>j</sub> qftStep nil

qftStep ≜ lift(<u>return</u> λ⟨qs, q⟩<sub>List<sub>j</sub></sub> Qubit⊗Qubit·
             let ⟨n, qs⟩ = qlen qs in
             let revQs = rev qs in
             let ⟨q, qs⟩ = (<u>fold</u><sub>e</sub> (<u>rotate</u> n)) ⟨q, nil⟩) revQs in
             let q = apply(H, q) in
             return (cons q qs))

rotate ≜ λn<sub>Nat</sub>·return λ⟨⟨q, cs⟩, c⟩<sub>(Qubit⊗List<e></sub> Qubit)⊗Qubit·
             let ⟨m, cs⟩ = qlen cs in
             let rgate = makeRGate (n + 1 − m) in
             let ⟨q, c⟩ = apply(rgate, ⟨q, c⟩) in
             return ⟨q, cons c cs⟩
```

<caption>**Fig. 17.** A Proto-Quipper-R implementation of the Quantum Fourier Transform circuit family. The usual syntactic sugar is employed.</caption>

The Proto-Quipper-R implementation of the QFT algorithm is given in Figure
17. As we walk through the various parts of the program, be aware that we
will focus on the resource aspects of the algorithm, ignoring much of its actual
meaning. Starting bottom-up, we assume that we have an encoding of naturals in the language and that we can perform arithmetic on them. We also assume some primitive gates and gate families: H is the boxed circuit corresponding to the Hadamard gate and has type Circ¹(Qubit, Qubit), whereas the makeRGate function has type Nat $\to$$_{0,0}$ Circ²(Qubit $\otimes$ Qubit, Qubit $\otimes$ Qubit) and produces instances of the parametric controlled $R_n$ gate. On the other hand, qlen and rev stand for regular language terms which implement respectively the linear list length and reverse functions. They have type qlen : List¹ Qubit $\to$$_{i,0}$ (Nat $\otimes$ List¹ Qubit) and rev : List¹ Qubit $\to$$_{i,0}$ List¹ Qubit in our type system.

We now turn our attention to the actual QFT algorithm. Function qftStep builds a single step of the QFT circuit. The width of the circuit produced at step $j$ is dominated by the folding of the rotate $n$ function, which applies controlled rotations between appropriate pairs of qubits and has type

$$ (\text{Qubit} \otimes \text{List}^e \text{Qubit}) \otimes \text{Qubit} \to_{e+2,0} \text{Qubit} \otimes \text{List}^{e+1} \text{Qubit}, \quad (4) $$

meaning that rotate $n$ rearranges the structure of its inputs, but overall does not introduce any new wire. We fold this function starting from an accumulator $\langle q, \text{nil} \rangle$, meaning that we can give fold$_j$ (lift(rotate $n$)) $\langle q, \text{nil} \rangle$ type as follows:

$$ \text{fold} \frac{i, j, e; n : \text{Nat}; \emptyset \vdash_v \text{lift}(\text{rotate } n) : !((\text{Q} \otimes \text{List}^e \text{Q}) \otimes \text{Q} \to_{e+2,0} \text{Q} \otimes \text{List}^{e+1} \text{Q})}{i, j; q : \text{Q}; \emptyset \vdash_v \langle q, \text{nil} \rangle : \text{Q} \otimes \text{List}^0 \text{Q} \qquad i, j \vdash j \qquad i, j \vdash \text{Q}} i, j; n : \text{Nat}, q : \text{Q}; \emptyset \vdash_v \text{fold}_e \text{lift}(\text{rotate } n) \langle q, \text{nil} \rangle : \text{List}^j \text{Q} \to_{j+1,1} \text{Q} \otimes \text{List}^j \text{Q} \quad (5) $$

where Q is shorthand for Qubit and where we implicitly use the fact that $i, j \vdash = \max(1, \max_{e<j} e + 2 + (j - 1 - e) \times 1) = j + 1$ to simplify the arrow's width annotation using vsub and the arrow subtyping rule. Next, we fold over revQs, which has the same elements as qs and thus has length $j$, and we obtain that the fold produces a circuit whose width is bounded by $j + 1$. Therefore, qftStep has type

$$ !((\text{List}^j \text{Qubit} \otimes \text{Qubit}) \to_{j+1,0} \text{List}^{j+1} \text{Qubit}), \quad (6) $$

which entails that when we pass it as an argument to the topmost fold together with nil we can conclude that the type of the qft function is

$$ \text{fold} \frac{i, j; \emptyset; \emptyset \vdash_v \text{qftStep} : !((\text{List}^j \text{Qubit} \otimes \text{Qubit}) \to_{j+1,0} \text{List}^{j+1} \text{Qubit})}{i; \emptyset; \emptyset \vdash_v \text{nil} : \text{List}^0 \text{Qubit} \qquad i \vdash i \qquad i \vdash \text{Qubit}} i; \emptyset; \emptyset \vdash_v \text{fold}_j \text{qftStep} \text{nil} : \text{List}^i \text{Qubit} \to_{i,0} \text{List}^i \text{Qubit} \quad (7) $$

where we once again implicitly simplify the arrow type using the fact that $i \vdash = \max(0, \max_{j<i} j + 1 + (i - 1 - j) \times 1) = i$. This concludes our analysis and the resulting type tells us that qft produces a circuit of width at most $i$ on inputs of size $i$, without overall using any additional wires. If we instantiate $i$ to 3, for example, we can apply qft to a list of 3 qubits to obtain the circuit shown in Figure 18, whose width is exactly 3.

To conclude this section, note that for ease of exposition qft actually produces the reversed QFT circuit. This is not a problem, since the two circuits are
<figure><img src="image_9.png" /><figcaption>Fig. 18. The circuit of input size 3 produced by *qft* (*cons q₁ cons q₂ cons q₃ nil*)</figcaption></figure>

equivalent resource-wise and the actual QFT circuit can be recovered by boxing the result of *qft* and reversing it via a primitive operator. Besides, note that Quipper's internal implementation of the QFT is also reversed [16].

# 7 Related Work

The metatheory of quantum circuit description languages, and in particular of Quipper-style languages, has been the subject of quite some work in recent years, starting with Ross's thesis on Proto-Quipper-S [48] and going forward with Selinger and Rios's Proto-Quipper-M [46]. In the last five years, some proposals have also appeared for more expressive type systems or for language extensions that can handle non-standard language features, such as the so-called *dynamic lifting* [8,21,35], available in the Quipper language, or dependent types [22]. Although some embryonic contributions in the direction of analyzing the size of circuits produced using Quipper have been given [56], no contribution tackles the problem of deriving resource bounds *parametric* on the size of the input. In this, the ability to have types which depend on the input, certainly a feature of Proto-Quipper-D [22], is not useful for the analysis of intensional attributes of the underlying circuit, simply because such attributes are not visible in types.

If we broaden the horizon to quantum programming languages other than Quipper, we come across, for example, the recent works of Avanzini et al. [5] and Liu et al. [36] on adapting the classic weakest precondition technique to the cost analysis of quantum programs, which however focus on programs in an imperative language. The work of Dal Lago et al. [13] on a quantum language which characterizes complexity classes for quantum polynomial time should certainly be remembered: even though the language allows the use of higher-order functions, the manipulation of quantum data occurs directly and not through circuits. Similar considerations hold for the recent work of Hainry et al. [29] and Yamakami's algebra of functions [59] in the style of Bellantoni and Cook [6], both characterizing quantum polynomial time.

If we broaden our scope further and become interested in the analysis of the cost of classical or probabilistic programs, we face a vast literature, with contributions employing a variety of techniques on heterogeneous languages and calculi: from functional programs [2,32,33] and term rewriting systems [3,4,41]
to probabilistic [34] and object-oriented programs [19,28]. In this context, the resource under analysis is often assumed to be computation *time*, which is relatively easy to analyze given its strictly monotonic nature. Circuit width, although monotonically non-decreasing, evolves in a way that depends on a non-monotonic quantity, i.e. the number of wires discarded by a circuit. As a result, width has the flavor of space and its analysis is less straightforward.

It is also worth mentioning that linear dependent types can be seen as a specialized version of refinement types [18], which have been used extensively in the literature to automatically verify interesting properties of programs [37,62]. In particular, the work of Vazou et al. on Liquid Haskell [57,58] has been of particular inspiration, on account of Quipper being embedded precisely in Haskell. The liquid type system [47] of Liquid Haskell relies on SMT solvers to discharge proof obligations and has been used fruitfully to reason about both the correctness and the resource consumption (mainly time complexity) of concrete, practical programs [30].

# 8 Generalization to Other Resource Types

This work focuses on estimating the *width* of the circuits produced by Quipper programs. This choice is dictated by the fact that the width of a circuit corresponds to the maximum number of distinct wires, and therefore individual qubits, required to execute it. Nowadays, this is considered as one of the most precious resources in quantum computing, and as such must be kept under control. However, this does not mean that our system could not be adapted to the estimation of other parameters. This section outlines how this may be possible.

First, estimating strictly monotonic resources, such as the total number of gates in a circuit, is possible and in fact simpler than estimating width. A single index term $I$ that measures the number of gates in the circuit built by a computation would be enough to carry out this analysis. This index would be appropriately increased any time an `apply` instruction is executed, while sequencing two terms via `let` would simply add together the respective indices.

If we were instead interested in the *depth* of a circuit, then we would need a slightly different approach. Although in principle it would be possible to still rely on a single index $I$, this would give rise to a very coarse approximation, effectively collapsing the analysis of depth to a gate count analysis. A more precise approximation could instead be obtained by keeping track of depth *locally*. More specifically, it would be sufficient to decorate each occurrence of a wire type $w$ with an index term $I$ so that if a label $\ell$ were typed with $w^I$, it would mean that the sub-circuit rooted in $\ell$ has a depth at most equal to $I$.

Finally, it should be mentioned that the resources considered, i.e. the depth, width, and gate count of a circuit, can be further refined so as to take into account only *some* kinds of wires and gates. For instance, one could want to keep track of the maximum number of *qubits* needed, ignoring the number of classical bits, or at least distinguishing the two parameters, which of course have distinct levels of criticality in current quantum hardware.
# 9 Conclusion and Future Work

In this paper we introduced a linear dependent type system based on index refinements and effect typing for the paradigmatic calculus *Proto-Quipper*, with the purpose of using it to derive upper bounds on the width of the circuits produced by programs. We proved not only the classic type safety properties, but also that the upper bounds derived via the system are correct. We also showed how our system can verify a realistic quantum algorithm and elaborated on some ideas on how our technique could be adapted to other crucial resources types, like gate count and circuit depth. Ours is the first type system designed specifically for the purpose of resource analysis to target circuit description languages such as *Quipper*. Technically, the main novelties are the smooth combination of effect typing and index refinements, but also the proof of correctness, in which reducibility and effects are shown to play well together.

Among topics for further work, we can identify three main research directions. First and foremost, it would be valuable to investigate the ideas presented in this paper from a more practical perspective, that is, to provide a prototype implementation of the language with its type-checking procedure. The necessity to count the wires present in the context (e.g. when typing abstractions) makes it difficult to embed *Proto-Quipper-R* into existing languages, even those that, in principle, seem like ideal hosts, like *Liquid Haskell* [57] or *Granule* [42]. Because of this, we think that it would be better to produce a standalone implementation of *Proto-Quipper-R* that interfaces directly with SMT solvers to discharge the semantic judgments that are used pervasively in the typing rules.

Staying instead on the theoretical side of things, on one hand we have the prospect of denotational semantics: most incarnations of *Proto-Quipper* are endowed with categorical semantics that model both circuits and the terms of the language that build them [21,22,35,46]. We already mentioned how the intensional nature of the quantity under analysis renders the formulation of an abstract categorical semantics for *Proto-Quipper-R* and its circuits a nontrivial task, but we believe that one such semantics would help *Proto-Quipper-R* fit better in the *Proto-Quipper* landscape.

On the other hand, in Section 8 we briefly discussed how our system could be modified to handle the analysis of different resource types. It would be interesting to test this path and to investigate the possibility of *actually generalizing* our resource analysis, that is, of making it parametric on the kind of resource being analyzed. This would allow for the same program in the same language to be amenable to different forms of verification, in a very flexible fashion.

**Acknowledgments** The research leading to these results has received funding from the European Union - NextGenerationEU through the Italian Ministry of University and Research under PNRR - M4C2 - I1.4 Project CN00000013 "National Centre for HPC, Big Data and Quantum Computing".
References

1. Altenkirch, T., Grattage, J.: A functional quantum programming language. In: Proc. of LICS '05 (2005)

2. Avanzini, M., Dal Lago, U., Moser, G.: Analysing the complexity of functional programs: Higher-order meets first-order. In: Proc. of ICFP 2015 (2015)

3. Avanzini, M., Moser, G.: Complexity analysis by rewriting. In: Proc. of FLOPS 2008 (2008)

4. Avanzini, M., Moser, G.: Tyrlean Complexity Tool: Features and Usage. In: Proc. of RTA 2013. vol. 21 (2013)

5. Avanzini, M., Moser, G., Pechoux, R., Perdrix, S., Zamdzhiev, V.: Quantum expectation transformers for cost analysis. In: Proc. of LICS '22 (2022)

6. Bellantoni, S., Cook, S.: A new recursion-theoretic characterization of the polytime functions (extended abstract). In: STOC '92 (1992)

7. Biere, A., Heule, M., van Maaren, H., Walsh, T.: Handbook of Satisfiability - Second Edition, Frontiers in Artificial Intelligence and Applications, vol. 336. IOS Press (2021)

8. Colledan, A., Dal Lago, U.: On Dynamic Lifting and Effect Typing in Circuit Description Languages. In: TYPES 2022. vol. 269 (2023)

9. Collins, H., Nay, C.: Ibm unveils 400 qubit-plus quantum processor and next-generation ibm quantum system two (2022), https://is.gd/WPV7lO, retrieved on Oct. 15, 2023

10. Conover, E.: Light-based quantum computer jiuzhang achieves quantum supremacy (2020), https://is.gd/kFv6IOy, retrieved on Oct. 15, 2023

11. Coppersmith, D.: An approximate fourier transform useful in quantum factoring, ibm research report rc19642 (2002)

12. Dal Lago, U., Gaboardi, M.: Linear dependent types and relative completeness. In: Proc. of LICS '11 (2011)

13. Dal Lago, U., Masini, A., Zorzi, M.: Quantum implicit computational complexity. TCS 411(2) (2010)

14. Dal lago, U., Petit, B.: Linear dependent types in a call-by-value scenario. In: Proc. of PPDP '12 (2012)

15. Dal lago, U., Petit, B.: The geometry of types. In: Proc. of POPL '13 (2013)

16. Eisenberg, R., Green, A., Lumsdaine, P., Kim, K., Mau, S.C., Mohan, B., Ng, W., Ravelomanantsoa-Ratsimihah, J., Ross, N., Scherer, A., Selinger, P., Valiron, B., Virodov, A., Zdancewic, S.: Quipper.libraries.qft, https://is.gd/AEJmp9, retrieved on Oct. 15, 2023

17. Fingerhuth, M., Babej, T., Wittek, P.: Open source software in quantum computing. PLOS ONE 13(12) (2018)

18. Freeman, T., Pfenning, F.: Refinement types for ml. In: Proc. of PLDI '91 (1991)

19. Frohn, F., Giesl, J.: Complexity analysis for java with aprove. In: Proc. of IFM 2017 (2017)

20. Fu, P., Kishida, K., Ross, N.J., Selinger, P.: A tutorial introduction to quantum circuit programming in dependently typed proto-quipper. In: Proc. of RC (2020)

21. Fu, P., Kishida, K., Ross, N.J., Selinger, P.: Proto-quipper with dynamic lifting. In: Proc. of POPL '23 (2023)

22. Fu, P., Kishida, K., Selinger, P.: Linear dependent type theory for quantum programming languages: Extended abstract. In: Proc. of LICS '20 (2020)

23. Gaboardi, M., Haeberlen, A., Hsu, J., Narayan, A., Pierce, B.C.: Linear dependent types for differential privacy. In: Proc. of POPL '13 (2013)
24. Gay, S.J.: Quantum programming languages: Survey and bibliography. Math. Struct. Comput. Sci. 16(4) (2006)

25. Green, A.S., Lumsdaine, P.L., Ross, N.J., Selinger, P., Valiron, B.: An introduction to quantum programming in quipper. In: Proc. of RC (2013)

26. Green, A.S., Lumsdaine, P.L., Ross, N.J., Selinger, P., Valiron, B.: Quipper. In: Proc. of PLDI (2013)

27. Grover, L.K.: A fast quantum mechanical algorithm for database search (1996)

28. Hainry, E., Péchoux, R.: Type-based heap and stack space analysis in Java (2013), technical report

29. Hainry, E., Péchoux, R., Silva, M.: A programming language characterizing quantum polynomial time. In: Proc. of FoSSaCS 2023 (2023)

30. Handley, M., Vazou, N., Hutton, G.: Liquidate your assets: reasoning about resource usage in liquid haskell. PACMPL 4 (2019)

31. Harrow, A.W., Hassidim, A., Lloyd, S.: Quantum algorithm for linear systems of equations. Phys. Rev. Lett. 103 (2009)

32. Hoffmann, J., Aehlig, K., Hofmann, M.: Resource aware ml. In: Computer Aided Verification (2012)

33. Hoffmann, J., Hofmann, M.: Amortized resource analysis with polynomial potential. In: Programming Languages and Systems (2010)

34. Kaminski, B.L., Katoen, J.P., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected run-times of probabilistic programs. In: Programming Languages and Systems. Berlin, Heidelberg (2016)

35. Lee, D., Perrelle, V., Valiron, B., Xu, Z.: Concrete Categorical Model of a Quantum Circuit Description Language with Measurement. In: Proc. of FSTTCS (2021)

36. Liu, J., Zhou, L., Barthe, G., Ying, M.: Quantum weakest preconditions for reasoning about expected runtimes of quantum programs. In: Proc. of LICS '22 (2022)

37. Mandelbaum, Y., Walker, D., Harper, R.: An effective theory of type refinements. In: Proc. of ICFP '03 (2003)

38. Martinis, J.: Quantum supremacy using a programmable superconducting processor (2019), https://is.gd/v3VXFi, retrieved on Oct. 15, 2023

39. Nielson, M.A., Chuang, I.L.: Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press (2010)

40. Nielson, F., Nielson, H.R.: Type and effect systems. In: Correct System Design: Recent Insights and Advances. Springer Berlin Heidelberg (1999)

41. Noschinski, L., Emmes, F., Giesl, J.: Analyzing innermost runtime complexity of term rewriting by dependency pairs. Journal of Automated Reasoning 51(1) (2013)

42. Orchard, D., Liepelt, V.B., Eades III, H.: Quantitative program reasoning with graded modal types. In: Proc. of ICFP '19. vol. 3 (2019)

43. Palsberg, J.: Toward a universal quantum programming language. XRDS: Crossroads 26(1) (2019)

44. Paykin, J., Rand, R., Zdancewic, S.: Qwire: A core language for quantum circuits. In: Proc. of POPL '17 (2017)

45. Preskill, J.: Quantum computing and the entanglement frontier (2012)

46. Rios, F., Selinger, P.: A categorical model for a quantum circuit description language. In: Proc. of QPL '17. vol. 266 (2017)

47. Rondon, P.M., Kawaguci, M., Jhala, R.: Liquid types. In: Proc. of PLDI '08 (2008)

48. Ross, N.: Algebraic and Logical Methods in Quantum Computation. Ph.D. thesis, Dalhousie University (2015)

49. Sanders, J.W., Zuliani, P.: Quantum programming. In: Proc. of MPC 2000 (2000)

50. Schlosshauer, M.: Decoherence and the Quantum-To-Classical Transition. Springer Berlin Heidelberg (2007)
51. Selinger, P.: A brief survey of quantum programming languages. In: Proc. of FLOPS 2004 (2004)

52. Selinger, P.: Towards a quantum programming language. Math. Struct. Comput. Sci. 14(4) (2004)

53. Selinger, P., Valiron, B.: A lambda calculus for quantum computation with classical control. In: Proc. of TLCA (2005)

54. Shor, P.: Algorithms for quantum computation: discrete logarithms and factoring. In: Proc. of FOCS '94 (1994)

55. Skorstengaard, L.: An introduction to logical relations (2019)

56. Valiron, B.: Automated, parametric gate count of quantum programs (2016), https://is.gd/Xlm3lh, retrieved on Oct. 15 2023

57. Vazou, N., Seidel, E.L., Jhala, R.: Liquidhaskell: Experience with refinement types in the real world. In: Proc. of Haskell '14 (2014)

58. Vazou, N., Seidel, E.L., Jhala, R., Vytiniotis, D., Peyton-Jones, S.: Refinement types for Haskell. In: Proc. of ICFP '14 (2014)

59. Yamakami, T.: A schematic definition of quantum polynomial time computability. The Journal of Symbolic Logic 85(4) (2020)

60. Yanofsky, N.S., Mannucci, M.A.: Quantum Computing for Computer Scientists. Cambridge University Press, USA, 1st edn. (2008)

61. Ying, M.: Foundations of Quantum Programming. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 1st edn. (2016)

62. Çiçek, E., Garg, D., Acar, U.: Refinement Types for Incremental Computational Complexity. In: Programming Languages and Systems, vol. 9032. Springer Berlin Heidelberg (2015)

63. Ömer, B.: Classical concepts in quantum programming. Int. J. Theor. Phys. 44(7) (2005)

**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.