## 5.5 Formally verified quantum compilation in an imperative setting: CertiQ

CertiQ [173] is another noticeable effort for verified compilation. Interestingly, it applies to QISKIT language, which is certainly the most widely used quantum compiler. CertiQ proceeds similarly as VOQC, by applying successive optimization passes, each consisting in applying local circuit equivalence transformations over quantum circuits. CertiQ has been evaluated against the very compilation environment provided by IBM QISKIT framework. And verified optimization went through 26 out of the 30 compilation passes the framework offered at writing time. Hence, the current limitations of formally verified compilation is mainly inherited from the state of the art in (non verified) quantum compilation.

The application to QISKIT also inevitably brings an additional drawback: while CertiQ can bring insurance that compilation respects the functional equivalence between an input and an output quantum circuits, the initial circuit building brick still lacks formal verification. Indeed, the environment is not provided formal means to assess that the input circuit meets a given functional specification. An open work direction then is to develop formal circuit building verification methods similar as SQIR or QBRICKS but applying to (mostly imperative) widely used development environments such as QISKIT, so as to complete the verified development chain.

# 6 Formal Quantum Programming Languages

For reasoning on a concrete *runs* of quantum algorithms solving a specific problem *instances*, the notion of quantum circuit is natural. Yet, a quantum circuit is only a by-product of a specific run of a quantum algorithm, holding only for a specific instantiation of the algorithm parameters.

Hence, a quantum algorithm is not reducible to a quantum circuit. To run quantum algorithms and reason about them, one needs *quantum programming languages (QPL)*: this is the topic of the current section.

## 6.1 Quantum Programming Languages Design

In Section 5, circuits were merely seen as sequences of elementary gates. However, in most quantum algorithms circuits follow a more complex structure: they are built compositionally from smaller sub-circuits and circuits combiners. Circuits are usually *static* objects, buffered until completion before being flushed to the quantum co-processor. Still, in some algorithms, they are *dynamically* generated: the tail of the circuit depends on the result of former measurements.

In this section, we discuss the high-level structure of quantum algorithms, the requirements for a quantum programming language, and review some of the existing proposals.

### 6.1.1 Structure of Quantum Algorithms

The usual model for quantum computation was depicted in Figure 1: a classical computer controls a quantum co-processor, whose role is to hold a quantum memory. A programmatic interface for interacting with the co-processor is provided to the programmer sitting in front of the classical computer. The interface gives methods to send instructions to the quantum memory to allocate and initialize new quantum registers, apply unitary gates on qubits, and eventually perform measurements. Even though the set of instructions is commonly represented as a circuit, it is merely the result of a *trace of classical execution* of a classical program on the classical computer.

Figure 8 presents two standard workflows with a quantum co-processor. In Figure 8a, the classical execution inputs some (classical) parameters, performs some pre-processing, generates a circuit,
<figure><img src="image_13.png" /><figcaption>Figure 8: Workflows for quantum algorithm</figcaption></figure>

sends the circuit to the coprocessor, collects the result of the measurement, and finally performs some post-processing to decide whether an output can be produced or if one needs to start over. Shor's factoring algorithm [175] or Grover's algorithm [84] fall into this scheme: the circuit is used as a fancy probabilistic oracle. Most of the recent variational algorithms [135] also fall into this scheme, with the subtlety that the circuit might be updated at each step. The other, less standard workflow is presented in Figure 8b. In this scheme, the circuit is built "on the fly", and measurements might be performed on a sub-part of the memory along the course of execution of the circuit. The latter part of the circuit might then depends on the result of classical processing in the middle of the computation.

Understanding a quantum circuit as a by-product of the execution of a classical program shines a fresh view on quantum algorithms: it cannot be identified with a quantum circuit. Instead, in general, at the very least a quantum algorithm describes a *family* of quantum circuits. Indeed, consider the setting of Figure 8a. The algorithm is fed with some parameters and then builds a circuit: the circuit will depend on the shape of the parameters. If for instance, we were using Shor's factoring algorithm, we would not build the same circuit for factoring 15 or 114,908,028,227. The bottom line is that a quantum programming language should be able to describe *parametrized* families of circuits.

The circuits described by quantum algorithms are potentially very large—a concrete instance of the HHL algorithm [87] for solving linear systems of equations has been shown [165] to count as much as ~ $10^{40}$ elementary gates, if not optimized. Unlike the circuit-construction schemes hinted at in Section 5, this circuit is not uniquely given as a list of elementary gates: it is built from sub-circuits —possibly described as a list of elementary gates but not only—and from high-level circuit combiners. These combiners build a circuit by (classically) processing a possibly large sub-circuit. Some standard such combiners are shown in Figure 9 (where we represent inverse with reflected letters). There is a distinction to be made between the combinator, applied on a sub-circuit, and its semantics, which is an action on each elementary gate. Combinators are abstractions that can be composed to build larger combiners, such as the one presented in Figure 10, built from inversion, controlling and sequential composition.
<figure><img src="image_15.png" /><figcaption>Figure 8: Workflows for quantum algorithm</figcaption></figure>

sends the circuit to the coprocessor, collects the result of the measurement, and finally performs some post-processing to decide whether an output can be produced or if one needs to start over. Shor's factoring algorithm [175] or Grover's algorithm [84] fall into this scheme: the circuit is used as a fancy probabilistic oracle. Most of the recent variational algorithms [135] also fall into this scheme, with the subtlety that the circuit might be updated at each step. The other, less standard workflow is presented in Figure 8b. In this scheme, the circuit is built "on the fly", and measurements might be performed on a sub-part of the memory along the course of execution of the circuit. The latter part of the circuit might then depend on the result of classical processing in the middle of the computation.

Understanding a quantum circuit as a by-product of the execution of a classical program shines a fresh view on quantum algorithms: it cannot be identified with a quantum circuit. Instead, in general, at the very least a quantum algorithm describes a *family* of quantum circuits. Indeed, consider the setting of Figure 8a. The algorithm is fed with some parameters and then builds a circuit: the circuit will depend on the shape of the parameters. If for instance, we were using Shor's factoring algorithm, we would not build the same circuit for factoring 15 or 114,908,028,227. The bottom line is that a quantum programming language should be able to describe *parametrized* families of circuits.

The circuits described by quantum algorithms are potentially very large—a concrete instance of the HHL algorithm [87] for solving linear systems of equations has been shown [165] to count as much as ~ $10^{40}$ elementary gates, if not optimized. Unlike the circuit-construction schemes hinted at in Section 5, this circuit is not uniquely given as a list of elementary gates: it is built from sub-circuits —possibly described as a list of elementary gates but not only—and from high-level circuit combiners. These combiners build a circuit by (classically) processing a possibly large sub-circuit. Some standard such combiners are shown in Figure 9 (where we represent inverse with reflected letters). There is a distinction to be made between the combinator, applied on a sub-circuit, and its semantics, which is an action on each elementary gate. Combinators are abstractions that can be composed to build larger combiners, such as the one presented in Figure 10, built from inversion, controlling and sequential composition.
<figure><img src="image_14.png" /><figcaption>Figure 9: Standard Circuit Combinators</figcaption></figure>

<figure><img src="image_15.png" /><figcaption>Figure 10: Example of a derived circuit combinator</figcaption></figure>

## 6.1.2 Requirements for Quantum Programming Languages

Any scalable quantum programming language should therefore allow the following operations within a common framework.

* Manipulation of quantum registers and quantum circuits as first-class objects. The programmer should both be able to refer to "wires" in a natural manner and handle circuits as independent objects.

* Description of *parametric families* of quantum circuits, both in a procedural manner as a sequence of operations-gates or subcircuits-and in an applicative manner, using circuit combinators;

* Classical processing. In our experience [83], quantum algorithms mostly consists of classical processing-processing the parameters, building the circuits, processing the result of the measurement.

This broad description of course calls for refinements. For instance some of the classical processing might be performed on the quantum co-processor-typically the simple classical controls involved in quantum error correction. The level of classical processing performed on the classical computer and performed on the quantum co-processor is dependent on the physical implementation. Even though some recent proposals such as Quingo [183] discuss the design of quantum programming languages aware of the two levels of classical processing-in and out of the co-processor, this is still a work in progress.

## 6.1.3 Review of the Existing Approaches

Most of the current existing quantum programming languages follow the requirements discussed in Section 6.1.2. In this section, we review some typical approaches followed both in academic and
<figure><img src="image_16.png" /><figcaption>Figure 9: Standard Circuit Combinators</figcaption></figure>

<figure><img src="image_17.png" /><figcaption>Figure 10: Example of a derived circuit combinator</figcaption></figure>

## 6.1.2 Requirements for Quantum Programming Languages

Any scalable quantum programming language should therefore allow the following operations within a common framework.

* Manipulation of quantum registers and quantum circuits as first-class objects. The programmer should both be able to refer to "wires" in a natural manner and handle circuits as independent objects.

* Description of *parametric families* of quantum circuits, both in a procedural manner as a sequence of operations—gates or subcircuits—and in an applicative manner, using circuit combinators;

* Classical processing. In our experience [83], quantum algorithms mostly consists of classical processing—processing the parameters, building the circuits, processing the result of the measurement.

This broad description of course calls for refinements. For instance some of the classical processing might be performed on the quantum co-processor—typically the simple classical controls involved in quantum error correction. The level of classical processing performed on the classical computer and performed on the quantum co-processor is dependent on the physical implementation. Even though some recent proposals such as Quingo [183] discuss the design of quantum programming languages aware of the two levels of classical processing—in and out of the co-processor, this is still a work in progress.

## 6.1.3 Review of the Existing Approaches

Most of the current existing quantum programming languages follow the requirements discussed in Section 6.1.2. In this section, we review some typical approaches followed both in academic and
industrial settings. This review is by no means meant to be exhaustive: its only purpose is to discuss
the possible strategies for the design of QPLs.

When designing a realistic programming language from scratch, the main problem is access to existing libraries and tools. In the context of quantum computation, one would need for instance to access the file system, make use of specific libraries such as Lapack or BLAS, etc. One can also rely on the well-maintained and optimized compiler or interpreter of the host language. To quickly come up with a scalable language, the easiest strategy consists in embedding the target language in a host language. Indeed, a quantum programming language can be seen as a domain-specific language (DSL), and it can be built over a regular language.

Even though the advantages of working inside a host language are clear, there are two main drawbacks. The first one is the potential rigidity of the host language: there might be constructs natural to the DSL that are hardly realizable inside the host language. The second drawback has to do with the compilation toolchain: the shallow embedding of the DSL makes it impossible to access its abstract syntax tree, rendering specific manipulation thereof impossible.

**Embedded QPLs.** The first scalable embedded proposal is Quipper [83, 82]. Embedded in Haskell, it capitalizes on *monads* to model the interaction with the quantum co-processor. Quipper's monadic semantics is meant to be easily abstracted and reasoned over: it is the subject of Section 6.2.2. Since Quipper, there has been a steady stream of embedded quantum programming languages, often dedicated to a specific quantum co-processor or attached to a specific vendor, and mostly in Python: QISKIT [153] and PROJECTQ [180] for IBMQ, CirQ [41] for Google, Strawberry Fields [106] for Xanadu, AQASM for Atos, etc. From a language-design point of view, most of these approaches heavily rely on Python objects to represent circuits and operations: the focus is on usability and versatility rather than safety and well-foundedness.

**Standalone QPLs.** On the other side of the spectrum, some quantum programming languages have been designed as standalone languages, with their own parser and abstract syntax tree. Maybe the first proposed scalable language was Ömer's QCL [142]. Ömer experimented several features such as circuit-as-function, automatic inversion and oracle generation. However, due to its non-modular approach, the language did not have successors.

Liqui|\rangle [193] and its sequel Q# [181] developed by Microsoft are good examples of an attempt at building a standalone language while keeping a tight link with an existing programming environment, as Liqui|\rangle and Q# are tightly linked with the F# framework (itself embedded in the whole .NET framework), making it possible to easily "reuse" library functions from within a Q# piece of code. On the other hand, Q# has its own syntax and type system, to capture run-time errors specific to quantum computation.

ScaffCC [99] is another example of a standalone QPL. Even though the language is rather low-level its compiler has been heavily optimized and experimented over, and it serves as a support for a long stream of research on quantum compiler optimizations.

The last noteworthy language to cite in the series is SILQ [27], as it serves as a good interface with the next paragraph: aimed at capturing most of the best practices in terms of soundness and safety, it is nonetheless targeted toward usability.

**Formal QPLs.** The last line of works on QPLs we would like to mention here is formal languages aimed at exploring and understanding the design principles and the semantics of quantum algorithms. We shall be brief as this is the topic of the remainder of this survey. The initial line of work
industrial settings. This review is by no means meant to be exhaustive: its only purpose is to discuss
the possible strategies for the design of QPLs.

When designing a realistic programming language from scratch, the main problem is access to existing libraries and tools. In the context of quantum computation, one would need for instance to access the file system, make use of specific libraries such as Lapack or BLAS, etc. One can also rely on the well-maintained and optimized compiler or interpreter of the host language. To quickly come up with a scalable language, the easiest strategy consists in embedding the target language in a host language. Indeed, a quantum programming language can be seen as a domain-specific language (DSL), and it can be built over a regular language.

Even though the advantages of working inside a host language are clear, there are two main drawbacks. The first one is the potential rigidity of the host language: there might be constructs natural to the DSL that are hardly realizable inside the host language. The second drawback has to do with the compilation toolchain: the shallow embedding of the DSL makes it impossible to access its abstract syntax tree, rendering specific manipulation thereof impossible.

**Embedded QPLs.** The first scalable embedded proposal is Quipper [83, 82]. Embedded in Haskell, it capitalizes on *monads* to model the interaction with the quantum co-processor. Quipper's monadic semantics is meant to be easily abstracted and reasoned over: it is the subject of Section 6.2.2. Since Quipper, there has been a steady stream of embedded quantum programming languages, often dedicated to a specific quantum co-processor or attached to a specific vendor, and mostly in Python: QISKIT [153] and PROJECTQ [180] for IBMQ, CirQ [41] for Google, Strawberry Fields [106] for Xanadu, AQASM for Atos, etc. From a language-design point of view, most of these approaches heavily rely on Python objects to represent circuits and operations: the focus is on usability and versatility rather than safety and well-foundedness.

**Standalone QPLs.** On the other side of the spectrum, some quantum programming languages have been designed as standalone languages, with their own parser and abstract syntax tree. Maybe the first proposed scalable language was Ömer's QCL [142]. Ömer experimented several features such as circuit-as-function, automatic inversion and oracle generation. However, due to its non-modular approach, the language did not have successors.

Liqui|\rangle [193] and its sequel Q# [181] developed by Microsoft are good examples of an attempt at building a standalone language while keeping a tight link with an existing programming environment, as Liqui|\rangle and Q# are tightly linked with the F# framework (itself embedded in the whole .NET framework), making it possible to easily "reuse" library functions from within a Q# piece of code. On the other hand, Q# has its own syntax and type system, to capture run-time errors specific to quantum computation.

ScaffCC [99] is another example of a standalone QPL. Even though the language is rather low-level its compiler has been heavily optimized and experimented over, and it serves as a support for a long stream of research on quantum compiler optimizations.

The last noteworthy language to cite in the series is SILQ [27], as it serves as a good interface with the next paragraph: aimed at capturing most of the best practices in terms of soundness and safety, it is nonetheless targeted toward usability.

**Formal QPLs.** The last line of works on QPLs we would like to mention here is formal languages aimed at exploring and understanding the design principles and the semantics of quantum algorithms. We shall be brief as this is the topic of the remainder of this survey. The initial line of work
was initiated by Selinger [168] with the study of a small flow-chart language with primitive constructs to interact with the quantum co-processor: qubit initialization, elementary gate application and measurement. This language was later extended to a simple Lambda-Calculus with similar primitive quantum features [170, 172]. Even though the language is not aimed at full-scale quantum algorithms, it is nonetheless enough to serve as a testbed for experimenting type systems and many operational [170, 57, 120] and denotational [143, 171, 58, 88] semantics.

The study of formal QPLs took a turn toward circuit-description languages à la Quipper with the development of scalable quantum languages. One of the first proposals of formalization is QWIRE [148], embedded in the proof assistant Coq. QWIRE uses Coq expressive system to encode the sophisticated typing rules of QWIRE. In a sense, Coq type system is expressive enough to use Coq as a host language and still be able to manipulate the abstract syntax tree of a program. The main design choice for QWIRE is to separate pure quantum computation with its constraints such as no-cloning, from classical computation.

Albeit disconnected from Coq, the formalization of Quipper has followed a similar root. This development is based on the formal language ProtoQuipper [162], which extracts the critical features out of Quipper: the creation and manipulation of circuits using a minimal Lambda-Calculus. The language is equipped with a linear type system and a simple operational semantics based on circuit construction. The simple core proposed by ProtoQuipper has stirred a line of research on the topic, including the formalization of inductive datatypes, recursion and dependent types in this context [160, 159, 130, 77].

The last class of formal programming language we want to mention focuses on the specification and verification of high-level properties of programs, and are solely based on circuit manipulation: unlike QWIRE or Quipper, qubits are not first-class objects and circuits are simple “bricks” to be horizontally or vertically stacked. In this class of languages, one can mention qPCF [144], mainly a theoretical exploration of dependent type systems in this setting, and QBRICKS, presented in Section 7.2.

## 6.2 Formalizing the Operational Semantics

In order to reason on quantum programming languages, one needs to have a formal understanding of their operational semantics.

### 6.2.1 Quantum Lambda-Calculi

The Lambda-Calculus [16] is a formal language encapsulating the main property of higher-order functional languages: functions are first-class citizens that can be passed as arguments to other functions. Lambda-Calculus features many extensions to model and reason about side-effects such as probabilistic or non-deterministic behaviors, shared memory, read/write, etc.

One of the first formal proposals of a quantum, functional language has precisely been a quantum extension of Lambda-Calculus [170]. On top of the regular Lambda-Calculus constructs, the quantum Lambda-Calculus features constants to name the operations of qubit initialization, unitary maps and measurements. A minimal system consists of the following terms:

$$ M, N ::= x \mid \lambda x.M \mid MN \mid \\ 	t \mid ff \mid if M then N_1 else N_2 \mid \\ 
qinit \mid U \mid meas. $$

Terms are represented with *M* and *N*, while variables *x* range over an enumerable set of identifiers. The term $\lambda x.M$ is an abstraction: it stands for a function of argument *x* and of body *M*.
was initiated by Selinger [168] with the study of a small flow-chart language with primitive constructs to interact with the quantum co-processor: qubit initialization, elementary gate application and measurement. This language was later extended to a simple Lambda-Calculus with similar primitive quantum features [170, 172]. Even though the language is not aimed at full-scale quantum algorithms, it is nonetheless enough to serve as a testbed for experimenting type systems and many operational [170, 57, 120] and denotational [143, 171, 58, 88] semantics.

The study of formal QPLs took a turn toward circuit-description languages à la Quipper with the development of scalable quantum languages. One of the first proposals of formalization is QWIRE [148], embedded in the proof assistant Coq. QWIRE uses Coq expressive system to encode the sophisticated typing rules of QWIRE. In a sense, Coq type system is expressive enough to use Coq as a host language and still be able to manipulate the abstract syntax tree of a program. The main design choice for QWIRE is to separate pure quantum computation with its constraints such as no-cloning, from classical computation.

Albeit disconnected from Coq, the formalization of Quipper has followed a similar root. This development is based on the formal language ProtoQuipper [162], which extracts the critical features out of Quipper: the creation and manipulation of circuits using a minimal Lambda-Calculus. The language is equipped with a linear type system and a simple operational semantics based on circuit construction. The simple core proposed by ProtoQuipper has stirred a line of research on the topic, including the formalization of inductive datatypes, recursion and dependent types in this context [160, 159, 130, 77].

The last class of formal programming language we want to mention focuses on the specification and verification of high-level properties of programs, and are solely based on circuit manipulation: unlike QWIRE or Quipper, qubits are not first-class objects and circuits are simple “bricks” to be horizontally or vertically stacked. In this class of languages, one can mention qPCF [144], mainly a theoretical exploration of dependent type systems in this setting, and QBRICKS, presented in Section 7.2.

## 6.2 Formalizing the Operational Semantics

In order to reason on quantum programming languages, one needs to have a formal understanding of their operational semantics.

### 6.2.1 Quantum Lambda-Calculi

The Lambda-Calculus [16] is a formal language encapsulating the main property of higher-order functional languages: functions are first-class citizens that can be passed as arguments to other functions. Lambda-Calculus features many extensions to model and reason about side-effects such as probabilistic or non-deterministic behaviors, shared memory, read/write, etc.

One of the first formal proposals of a quantum, functional language has precisely been a quantum extension of Lambda-Calculus [170]. On top of the regular Lambda-Calculus constructs, the quantum Lambda-Calculus features constants to name the operations of qubit initialization, unitary maps and measurements. A minimal system consists of the following terms:

$$M, N ::= x \mid \lambda x.M \mid MN \mid \\ 	t \mid ff \mid if M then N_1 else N_2 \mid \\ 
qinit \mid U \mid meas.$$

Terms are represented with *M* and *N*, while variables *x* range over an enumerable set of identifiers. The term $\lambda x.M$ is an abstraction: it stands for a function of argument *x* and of body *M*.
The application of a function *M* to an argument *N* is represented with *MN*. To this core Lambda-Calculus, we can add constructs to deal with booleans: *tt* and *ff* are the boolean constant values, while if *M* then *N* else *N*₂ is the usual test. Finally, *qinit* stands for qubit initialization, *meas* for measurement and *U* ranges over a set of unitary operations. These three constants are functions: for instance, *qinit* *tt* corresponds to |1⟩ and *qinit* *ff* to |0⟩, while *meas* applied to a qubit stands for the measurement of this qubit. A fair coin can then be represented by the term

$$ \mathrm{meas}(\mathrm{H}(\mathrm{qinit}\ \mathrm{tt})), \qquad (3) $$

where *H* stands for the Hadamard gate.

The question is now: how do we formalize the evaluation of a piece of code? In the regular Lambda-Calculus, evaluation is performed with *substitution* as follows:

$$ (\lambda x.M)N \rightarrow M[x := N] $$

where *M[x := N]* stands for *M* where all free occurrences of *x* –i.e., those corresponding to the argument of the function–have been replaced by *N*. Even though we can still require such a rule in the context of the quantum Lambda-Calculus, this does not say how to deal with the term *qinit* *tt*.

In order to give an operational semantics to the Lambda-Calculus, a naive idea could be to add yet another construction: a set of constants *c*<sub>|*φ*<sub>1</sub>|</sub>, once for every possible qubit state |*φ*<sub>1</sub>⟩. If–as shown by van Tonder [188]– this can somehow be made to work, a more natural presentation consists in mimicking the behavior of a quantum co-processor, in the style of Knill’s QRAM model [113]: we define an *abstract machine* (|*φ*<sub>1</sub>⟩<sub>n</sub>, *L*, *M*) consisting of a finite memory state |*φ*<sub>1</sub>⟩<sub>n</sub> of *n* qubits, a term *M* with *n* free variables *x*₁, ..., *x*<sub>n</sub>, and a *linking function* *L*, bijection between {*x*₁, ..., *x*<sub>n</sub>} and the qubit indices {1, ..., *n*}. Variables of *M* captured by *L* are essentially pointers to qubits standing in the quantum memory. The fair coin of Eq. (3) then evaluates as follows.

$$ \begin{align*} & (|0⟩_0, \{\}, \mathrm{meas}(\mathrm{H}(\mathrm{qinit}\ \mathrm{tt}))) \\ & \rightarrow (|1⟩_1, \{x \mapsto 1\}, \mathrm{meas}(\mathrm{H}x)) \\ & \rightarrow (\frac{1}{\sqrt{2}}(|0⟩_1 - |1⟩_1), \{x \mapsto 1\}, \mathrm{meas}x) \\ & \rightarrow \begin{cases} (|0⟩_1, \{\}, \mathrm{ff}) & \text{with prob. 0.5} \\ (|1⟩_1, \{\}, \mathrm{tt}) & \text{with prob. 0.5.} \end{cases} \end{align*} $$

In this evaluation, most of quantum computation has been exemplified: initialization of qubits, unitary operations and measurements. Handling the latter in particular requires a *probabilistic evaluation*, and this requires some care–we invite the interested reader to consult for example Selinger & Valiron [170] for details.

### 6.2.2 Monadic Semantics

The operational semantics of the quantum Lambda-Calculus is very limited. Indeed, as discussed in Section 6.1, quantum algorithms do not in general send operations one by one to the quantum co-processor: instead, a quantum program must build circuits (or pieces thereof) before sending them to the co-processor as batch jobs. The quantum Lambda-Calculus does not allow to build circuits: operations can only be sent one at a time. In particular, there is no possibility to create, manipulate and process circuits: circuit generation in the quantum Lambda-Calculus is a *side-effect* that is external to the language. One cannot interfere with it, and embedding the quantum Lambda-Calculus as it stands inside a host language, as suggested in Section 6.1.3, would not help.

The solution devised by Quipper consists in relying on a special language feature from Haskell called *monad*. A monad is a type operator encapsulating a side effect. Consider for instance a
The application of a function *M* to an argument *N* is represented with *MN*. To this core Lambda-Calculus, we can add constructs to deal with booleans: *tt* and *ff* are the boolean constant values, while if *M* then *N* else *N*₂ is the usual test. Finally, *qinit* stands for qubit initialization, *meas* for measurement and *U* ranges over a set of unitary operations. These three constants are functions: for instance, *qinit* *tt* corresponds to |1⟩ and *qinit* *ff* to |0⟩, while *meas* applied to a qubit stands for the measurement of this qubit. A fair coin can then be represented by the term

$$ \mathrm{meas}(\mathrm{H}(\mathrm{qinit}\ \mathrm{tt})), \qquad (3) $$

where H stands for the Hadamard gate.

The question is now: how do we formalize the evaluation of a piece of code? In the regular Lambda-Calculus, evaluation is performed with *substitution* as follows:

$$ (\lambda x.M)N \rightarrow M[x := N] $$

where *M[x := N]* stands for *M* where all free occurrences of *x* –i.e., those corresponding to the argument of the function–have been replaced by *N*. Even though we can still require such a rule in the context of the quantum Lambda-Calculus, this does not say how to deal with the term *qinit* *tt*.

In order to give an operational semantics to the Lambda-Calculus, a naive idea could be to add yet another construction: a set of constants *c*<sub>|*φ*<sub>1</sub>|</sub>, once for every possible qubit state |*φ*<sub>1</sub>⟩. If–as shown by van Tonder [188]– this can somehow be made to work, a more natural presentation consists in mimicking the behavior of a quantum co-processor, in the style of Knill’s QRAM model [113]: we define an *abstract machine* (|*φ*<sub>1</sub>⟩<sub>n</sub>, *L*, *M*) consisting of a finite memory state |*φ*<sub>1</sub>⟩<sub>n</sub> of *n* qubits, a term *M* with *n* free variables *x*₁, ..., *x*<sub>n</sub>, and a *linking function* *L*, bijection between {*x*₁, ..., *x*<sub>n</sub>} and the qubit indices {1, ..., *n*}. Variables of *M* captured by *L* are essentially pointers to qubits standing in the quantum memory. The fair coin of Eq. (3) then evaluates as follows.

$$ \begin{align*} & (|0⟩_0, \{\}, \mathrm{meas}(\mathrm{H}(\mathrm{qinit}\ \mathrm{tt}))) \\ & \rightarrow (|1⟩_1, \{x \mapsto 1\}, \mathrm{meas}(\mathrm{H}x)) \\ & \rightarrow (\frac{1}{\sqrt{2}}(|0⟩_1 - |1⟩_1), \{x \mapsto 1\}, \mathrm{meas}x) \\ & \rightarrow \begin{cases} (|0⟩_1, \{\}, \mathrm{ff}) & \text{with prob. 0.5} \\ (|1⟩_1, \{\}, \mathrm{tt}) & \text{with prob. 0.5.} \end{cases} \end{align*} $$

In this evaluation, most of quantum computation has been exemplified: initialization of qubits, unitary operations and measurements. Handling the latter in particular requires a *probabilistic evaluation*, and this requires some care–we invite the interested reader to consult for example Selinger & Valiron [170] for details.

### 6.2.2 Monadic Semantics

The operational semantics of the quantum Lambda-Calculus is very limited. Indeed, as discussed in Section 6.1, quantum algorithms do not in general send operations one by one to the quantum co-processor: instead, a quantum program must build circuits (or pieces thereof) before sending them to the co-processor as batch jobs. The quantum Lambda-Calculus does not allow to build circuits: operations can only be sent one at a time. In particular, there is no possibility to create, manipulate and process circuits: circuit generation in the quantum Lambda-Calculus is a *side-effect* that is external to the language. One cannot interfere with it, and embedding the quantum Lambda-Calculus as it stands inside a host language, as suggested in Section 6.1.3, would not help.

The solution devised by Quipper consists in relying on a special language feature from Haskell called *monad*. A monad is a type operator encapsulating a side effect. Consider for instance a
probabilistic side effect. There are therefore two classes of terms: terms without side-effect, with types e.g. `Bool`, or `Int`, and terms with side-effect, with types e.g. `P Bool` or `P Int` standing for "term evaluating to a boolean/integer, possibly with a probabilistic effect". The operator `P (-)` captures the probabilistic side effect.

A monad comes with two standard maps. In the case of P we would have:

```
return :: A -> P(A)
bind :: P(A) -> (A -> P(B)) -> P(B)
```

The `return` operation says that an effect-free term can be considered as having an effect-in the case of the probabilistic effect, it just means "with probability 1". The `bind` operation<fnref n="7" /> says how to compose effectful operations: given a function inputting `A` and returning an object of type `B` with a probabilistic side-effect, how to apply this function to a term of type `A` also having a probabilistic effect? We surely get something of type `P(B)`, but the way to construct it is described by `bind`. A few equations have to be satisfied by `return` and `bind` for them to describe a monad. For instance, `bind return` is the identity on `P(A)`. There can of course be more operations: for instance, we can add to the signature of `P` an operator `coin` of type `() -> P(Bool)`<fnref n="8" />.

A nice property of monads is that effectful operations can be written with syntactic sugar in an imperative style:

```
do
    x <- coin ()
    if x then return 0 else return 1
```

is a term of type `P(Int)` equals to

`bind (coin()) (\lambda x. if x then return 0 else return 1)`

once the syntactic sugar has been removed.

Following this approach, quantum computation can be understood as side-effect: it combines both (1) Read/Write effect, since gates are sent to the coprocessor, and results of measurements are received; (2) Probabilistic effects, since measurement is a probabilistic operation. The first attempt at formalizing this monad is Green's quantum IO monad [3]: it has then been further developed in Quipper [83].

Internally, circuits in Quipper are represented using a simple inductive datatype akin to a list of gates<fnref n="9" />. The interaction with the quantum-coprocessor is modeled using a specific I/O monad `Circ`. This monad encapsulates the construction of circuits featuring wires holding qubits but also wires holding bits —results of measurements. A bit is however uniquely useable "inside" the monad: to use it in Haskell —in an if-then-else construct for instance— we need to "lift" it into a regular Boolean. The signature of the monad in particular includes

```
qinit :: Bool -> Circ(Qubit)
measure :: Qubit -> Circ(Bit)
hadamard :: Qubit -> Circ(Qubit)
```

A fair coin can be implemented as a circuit returning a bit, of type `() -> Circ Bit`.

<footnote n="7">⁷In Haskell, this map is denoted with `>>=`. For the sake of legibility, here we denote it with `bind`.</footnote>

<footnote n="8">⁸In Haskell, the unit type is denoted with `()`.</footnote>

<footnote n="9">⁹Technically a tree structure, as measurements entails branching.</footnote>
probabilistic side effect. There are therefore two classes of terms: terms without side-effect, with types e.g. `Bool`, or `Int`, and terms with side-effect, with types e.g. `P Bool` or `P Int` standing for "term evaluating to a boolean/integer, possibly with a probabilistic effect". The operator `P (-)` captures the probabilistic side effect.

A monad comes with two standard maps. In the case of P we would have:

```
return :: A -> P(A)
bind :: P(A) -> (A -> P(B)) -> P(B)
```

The `return` operation says that an effect-free term can be considered as having an effect—in the case of the probabilistic effect, it just means “with probability 1”. The `bind` operation<fnref n="7" /> says how to compose effectful operations: given a function inputting `A` and returning an object of type `B` with a probabilistic side-effect, how to apply this function to a term of type `A` also having a probabilistic effect? We surely get something of type `P(B)`, but the way to construct it is described by `bind`. A few equations have to be satisfied by `return` and `bind` for them to describe a monad. For instance, `bind return` is the identity on `P(A)`. There can of course be more operations: for instance, we can add to the signature of `P` an operator `coin` of type `() -> P(Bool)`<fnref n="8" />.

A nice property of monads is that effectful operations can be written with syntactic sugar in an imperative style:

```
do
    x <- coin ()
    if x then return 0 else return 1
```

is a term of type `P(Int)` equals to

```
bind (coin()) (λx.if x then return 0 else return 1)
```

once the syntactic sugar has been removed.

Following this approach, quantum computation can be understood as side-effect: it combines both (1) Read/Write effect, since gates are sent to the coprocessor, and results of measurements are received; (2) Probabilistic effects, since measurement is a probabilistic operation. The first attempt at formalizing this monad is Green's quantum IO monad [3]: it has then been further developed in Quipper [83].

Internally, circuits in Quipper are represented using a simple inductive datatype akin to a list of gates<fnref n="9" />. The interaction with the quantum-coprocessor is modeled using a specific I/O monad `Circ`. This monad encapsulates the construction of circuits featuring wires holding qubits but also wires holding bits —results of measurements. A bit is however uniquely useable “inside” the monad: to use it in Haskell —in an if-then-else construct for instance— we need to “lift” it into a regular Boolean. The signature of the monad in particular includes

```
qinit :: Bool -> Circ(Qubit)
measure :: Qubit -> Circ(Bit)
hadamard :: Qubit -> Circ(Qubit)
```

A fair coin can be implemented as a circuit returning a bit, of type `() -> Circ Bit`.

<footnote n="7">⁷In Haskell, this map is denoted with `>>=`. For the sake of legibility, here we denote it with `bind`.</footnote>

<footnote n="8">⁸In Haskell, the unit type is denoted with `()`.</footnote>

<footnote n="9">⁹Technically a tree structure, as measurements entails branching.</footnote>
bitcoin () = do
q <- qinit True
q' <- hadamard q
r <- measure q'
return r

The function bitcoin will merely generate a computation —producing a circuit— waiting to be
executed. To implement the toss-coin of Section 6.2.2, we then need to “run” the circuit for lifting
the bit into a Boolean. Provided that we have a function

run :: Circ Bit -> P Bool

one can then implement coin () as run (bitcoin()).

Thanks to the monadic encapsulation, circuits can be manipulated within Haskell. For instance,
inversion and control can be coded in Haskell as circuit combinators with the following types.

inverse :: (a -> Circ b) -> (b -> Circ a)
control :: (a -> Circ b) -> ((a,Qubit) -> Circ (b,Qubit))

The compositionality of the monadic semantics also makes it possible to automatically construct
oracles out of classical specification [83, 186].

Compared with the quantum λ-Calculus discussed in Section 6.2.1, where the program can only
send gates one by one to the co-processor, Quipper gives to the programmer the ability to manipu-
late circuits. Although both the quantum λ-Calculus and Quipper represent quantum computations
mathematically, Quipper provides a richer model, better-suited for program specification and verifi-
cation than the plain λ-Calculus.

**6.3 Type Systems**

In Section 6.2, we discussed how to model the operational behavior of a quantum program. We have
however not mentioned yet the run-time errors inherent to quantum computation. In the classical
world, type systems are a standard strategy to catch run-time errors at compile-time. Several run-
time errors specific to quantum computation can also be caught with a type system, with a few
specificities that we discuss in this section.

**6.3.1 Quantum Data and Type Linearity**

The main problem with quantum information is that it is *non-duplicable* (a.k.a. *non clonable*, see
Section 4.2.3). In terms of quantum programming language, this means that a program cannot
duplicate a quantum bit: if *U* is a unitary map acting on two qubits, the function *λ*x.U(*x* ⊗ *x*) trying
to feed *U* with two copies of its argument makes no sense. Similarly, it is not possible to control a
gate acting on a qubit with the same qubit. The Quipper code of Figure 11 is, therefore, buggy.

Type systems, in a broad sense, provide a predicate that says that a well-typed program does not
have a certain class of bugs: in the case of quantum programming languages, a large class of bugs
comes from duplicating non-duplicable objects. This calls for a *linear* type system, enforcing at least
the non-duplication of qubits. This has been taken into account in recent scalable implementations
such as Silq [27].

On the theoretical side, type systems for quantum Lambda-Calculi and ProtoQuipper [162]–the
formalization of Quipper–are typically based on linear logic. Originally designed by Girard [79] (as
a continuation of [121]), linear logic assumes that formulas are linear–i.e. non-duplicable and non-
erasable–by default, and the logic comes equipped with a logic constructor “!” to annotate duplicable
bitcoin () = do
    q <- qinit True
    q' <- hadamard q
    r <- measure q'
return r

The function `bitcoin` will merely generate a computation —producing a circuit— waiting to be executed. To implement the toss-coin of Section 6.2.2, we then need to “run” the circuit for lifting the bit into a Boolean. Provided that we have a function

run :: Circ Bit -> P Bool

one can then implement `coin()` as `run(bitcoin())`.

Thanks to the monadic encapsulation, circuits can be manipulated within Haskell. For instance, inversion and control can be coded in Haskell as circuit combinators with the following types.

inverse :: (a -> Circ b) -> (b -> Circ a)
control :: (a -> Circ b) -> ((a,Qubit) -> Circ (b,Qubit))

The compositionality of the monadic semantics also makes it possible to automatically construct oracles out of classical specification [83, 186].

Compared with the quantum $\lambda$-Calculus discussed in Section 6.2.1, where the program can only send gates one by one to the co-processor, Quipper gives to the programmer the ability to manipulate circuits. Although both the quantum $\lambda$-Calculus and Quipper represent quantum computations mathematically, Quipper provides a richer model, better-suited for program specification and verification than the plain $\lambda$-Calculus.

## 6.3 Type Systems

In Section 6.2, we discussed how to model the operational behavior of a quantum program. We have however not mentioned yet the run-time errors inherent to quantum computation. In the classical world, type systems are a standard strategy to catch run-time errors at compile-time. Several run-time errors specific to quantum computation can also be caught with a type system, with a few specificities that we discuss in this section.

### 6.3.1 Quantum Data and Type Linearity

The main problem with quantum information is that it is *non-duplicable* (a.k.a. *non clonable*, see Section 4.2.3). In terms of quantum programming language, this means that a program cannot duplicate a quantum bit: if *U* is a unitary map acting on two qubits, the function $\lambda x.U(x \otimes x)$ trying to feed *U* with two copies of its argument makes no sense. Similarly, it is not possible to control a gate acting on a qubit with the same qubit. The Quipper code of Figure 11 is, therefore, buggy.

Type systems, in a broad sense, provide a predicate that says that a well-typed program does not have a certain class of bugs: in the case of quantum programming languages, a large class of bugs comes from duplicating non-duplicable objects. This calls for a *linear type system*, enforcing at least the non-duplication of qubits. This has been taken into account in recent scalable implementations such as Silq [27].

On the theoretical side, type systems for quantum Lambda-Calculi and ProtoQuipper [162]–the formalization of Quipper–are typically based on linear logic. Originally designed by Girard [79] (as a continuation of [121]), linear logic assumes that formulas are linear–i.e. non-duplicable and non-erasable–by default, and the logic comes equipped with a logic constructor “!” to annotate duplicable
```pascal
exp :: Circ Qubit
exp = do
  q1 <- qinit True
  q2 <- qinit True
  r <- qnot q1 'controlled' q1
return r
```

<caption>Figure 11: An example of a buggy Quipper program</caption>

and erasable formulas. Linear logic also proposes a special pairing constructor ⊗ replacing the usual product and compatible with both the linearity constructs and the (linear) implication —.

A core type system for a quantum Lambda-Calculus with pairing therefore consists of the following grammar:

$$A, B ::= qubit | bool | A \to B | A \otimes B | !A.$$

Type $A \to B$ represents the type of (linear) functions, using their argument only once. Type $A \otimes B$ represents the pair of a term of type $A$ and a term of type $B$. Type $!A$ stands for a duplicable term of type $A$. We give a few examples as follows.

* The identity function $\lambda x.x$ is of type $A \to A$, but also of type $!(A \to A)$ as it is duplicable (since it does not contain any non-duplicable object);

* If the pairing construct is represented with $\langle -, - \rangle$, the function $\lambda x.\langle x, x \rangle$ is of type $!A \to (!A \otimes !A)$: it asks for a duplicable argument;

* The operator $qinit$ is of type $!(bool \to qubit)$: it is duplicable but it does not generate a duplicable qubit;

* The operator $meas$ can however be typed with $!(qubit \to !bool)$ as a boolean should be duplicable;

* Provided that $U$ is a unitary acting on two qubits, one can type it in a functional manner with $qubit \otimes qubit \to qubit \otimes qubit$: it inputs two (non-duplicable) qubits and outputs the (still non-duplicable) modified qubits;

* In particular, provided that we assume implicit dereliction, casting duplicable elements of type $!A$ to $A$, the term $\lambda x.U\langle x, x \rangle$ can only be typed with $!qubit \to qubit \otimes qubit$: its argument has to be duplicable. The fact that this program can never be actually used on a concrete qubit is a property of the type system (intuitively, $qinit$ only generates non-duplicable qubits).

### 6.3.2 Example: Quantum Teleportation

Mixing quantum computation and higher-order objects can yield non-trivial objects. The scheme of teleportation is given in Figure 12. It consists of three steps: (A) creation of a Bell state, (B) measure in the Bell basis to retrieve two booleans and (C) application of a gate $U_{b_1b_2}$ dependent on the result of the measure. The state of the top wire is then “teleported” to the bottom wire. It is possible to understand the pieces of the quantum teleportation protocol as three (duplicable) functions:

(A) $!(()) \to qubit \otimes qubit$

(B) $!(qubit \to (qubit \to bool \otimes bool))$

(C) $!(qubit \to (bool \otimes bool \to qubit))$
```pascal
exp :: Circ Qubit
exp = do
  q1 <- qinit True
  q2 <- qinit True
  r <- qnot q1 'controlled' q1
return r
```

<caption>Figure 11: An example of a buggy Quipper program</caption>

and erasable formulas. Linear logic also proposes a special pairing constructor ⊗ replacing the usual product and compatible with both the linearity constructs and the (linear) implication —.

A core type system for a quantum Lambda-Calculus with pairing therefore consists of the following grammar:

$$A, B ::= \text{qubit} | \text{bool} | A \to B | A \otimes B | !A.$$

Type $A \to B$ represents the type of (linear) functions, using their argument only once. Type $A \otimes B$ represents the pair of a term of type A and a term of type B. Type $!A$ stands for a duplicable term of type A. We give a few examples as follows.

* The identity function $\lambda x.x$ is of type $A \to A$, but also of type $!(A \to A)$ as it is duplicable (since it does not contain any non-duplicable object);

* If the pairing construct is represented with $\langle -, - \rangle$, the function $\lambda x.\langle x, x \rangle$ is of type $!A \to (!A \otimes !A)$: it asks for a duplicable argument;

* The operator $qinit$ is of type $!(\mathit{qubit} \to \mathit{qubit})$: it is duplicable but it does not generate a duplicable qubit;

* The operator $\mathit{meas}$ can however be typed with $!(\mathit{qubit} \to !\mathit{bool})$ as a boolean should be duplicable;

* Provided that $U$ is a unitary acting on two qubits, one can type it in a functional manner with $\mathit{qubit} \otimes \mathit{qubit} \to \mathit{qubit} \otimes \mathit{qubit}$: it inputs two (non-duplicable) qubits and outputs the (still non-duplicable) modified qubits;

* In particular, provided that we assume implicit dereliction, casting duplicable elements of type $!A$ to $A$, the term $\lambda x.U\langle x, x \rangle$ can only be typed with $!\mathit{qubit} \to \mathit{qubit} \otimes \mathit{qubit}$: its argument has to be duplicable. The fact that this program can never be actually used on a concrete qubit is a property of the type system (intuitively, $qinit$ only generates non-duplicable qubits).

### 6.3.2 Example: Quantum Teleportation

Mixing quantum computation and higher-order objects can yield non-trivial objects. The scheme of teleportation is given in Figure 12. It consists of three steps: (A) creation of a Bell state, (B) measure in the Bell basis to retrieve two booleans and (C) application of a gate $U_{b_1b_2}$ dependent on the result of the measure. The state of the top wire is then “teleported” to the bottom wire. It is possible to understand the pieces of the quantum teleportation protocol as three (duplicable) functions:

(A) $!(()) \to \mathit{qubit} \otimes \mathit{qubit}$

(B) $!(\mathit{qubit} \to (\mathit{qubit} \to \mathit{bool} \otimes \mathit{bool}))$

(C) $!(\mathit{qubit} \to (\mathit{bool} \otimes \mathit{bool} \to \mathit{qubit}))$
<figure><img src="image_16.png" /><figcaption>Figure 12: Teleportation algorithm</figcaption></figure>

The parts (B) and (C) are duplicable functions producing two non-duplicable functions of type qubit $\to$ bool $\otimes$ bool and bool $\otimes$ bool $\to$ qubit. The teleportation algorithm then feeds the two qubits emitted by (A) to (B) and (C); this gives a general type

$$ !((\to (qubit \to bool \otimes bool) \otimes (bool \otimes bool \to qubit))) $$

for the protocol. It can be used several times (as it is duplicable). Each time it is run, it generates a pair of non-duplicable functions $\langle f,g \rangle$, and the specification of the protocol states that these two functions are inverse one of the other.

These two functions f and g of the pair are non-duplicable. Indeed, each of them holds a (non-duplicable) qubit coming from (A). Moreover, in a sense, these functions are entangled, since the Bell state from (A) is entangled.

### 6.3.3 Extending the Type System to Support Circuits

Let us assume that the type system of the quantum Lambda-Calculus is extended with lists: [A] stands for lists of elements of type A (see e.g. [170] to see how to do this). A function [qubit] $\to$ [qubit] inputs a list of qubits. It can apply unitary gates to these qubit arguments: It can in fact describe different circuits, depending on the size of the list. Such a function, therefore, describes a family of circuits. The quantum Lambda-Calculus is not expressive enough to extract one circuit out of this family of circuits and operate on it (e.g. by inversing or controlling it).

The ProtoQuipper language [162] and its successors [160, 159, 77, 130] are formalized fragments of the programming language Quipper. They enforce structural properties of quantum programs using the linear type system of the quantum Lambda-Calculus, yet extending it to support circuit manipulation. ProtoQuipper comes with a new type construct Circ(A,B): the type of circuits from A to B, and two functions:

* box sends A $\to$ B to Circ(A,B). It takes a function A $\to$ B, partially evaluates it, and stores the emitted circuit in an object of type Circ(A,B).

* unbox sends Circ(A,B) to A $\to$ B. It takes a circuit from A to B and reads it as a function of input A and output B.

The behavior of box and unbox is specified by the operational semantic of the language [162].

One of the subtleties is the fact that box turns a function-possibly representing a family of many circuits-to one circuit. In the case of a function of type [qubit] $\to$ [qubit], this corresponds
<figure><img src="image_18.png" /><figcaption>Figure 12: Teleportation algorithm</figcaption></figure>

The parts (B) and (C) are duplicable functions producing two non-duplicable functions of type qubit $\to$ bool $\otimes$ bool and bool $\otimes$ bool $\to$ qubit. The teleportation algorithm then feeds the two qubits emitted by (A) to (B) and (C); this gives a general type

$$ !((\to (qubit \to bool \otimes bool) \otimes (bool \otimes bool \to qubit))) $$

for the protocol. It can be used several times (as it is duplicable). Each time it is run, it generates a pair of non-duplicable functions $\langle f, g \rangle$, and the specification of the protocol states that these two functions are inverse one of the other.

These two functions f and g of the pair are non-duplicable. Indeed, each of them holds a (non-duplicable) qubit coming from (A). Moreover, in a sense, these functions are entangled, since the Bell state from (A) is entangled.

### 6.3.3 Extending the Type System to Support Circuits

Let us assume that the type system of the quantum Lambda-Calculus is extended with lists: [A] stands for lists of elements of type A (see e.g. [170] to see how to do this). A function [qubit] $\to$ [qubit] inputs a list of qubits. It can apply unitary gates to these qubit arguments: It can in fact describe different circuits, depending on the size of the list. Such a function, therefore, describes a family of circuits. The quantum Lambda-Calculus is not expressive enough to extract one circuit out of this family of circuits and operate on it (e.g. by inversing or controlling it).

The ProtoQuipper language [162] and its successors [160, 159, 77, 130] are formalized fragments of the programming language Quipper. They enforce structural properties of quantum programs using the linear type system of the quantum Lambda-Calculus, yet extending it to support circuit manipulation. ProtoQuipper comes with a new type construct Circ(A, B): the type of circuits from A to B, and two functions:

* box sends A $\to$ B to Circ(A, B). It takes a function A $\to$ B, partially evaluates it, and stores the emitted circuit in an object of type Circ(A, B).

* unbox sends Circ(A, B) to A $\to$ B. It takes a circuit from A to B and reads it as a function of input A and output B.

The behavior of box and unbox is specified by the operational semantic of the language [162].

One of the subtleties is the fact that box turns a function-possibly representing a family of many circuits-to one circuit. In the case of a function of type [qubit] $\to$ [qubit], this corresponds
to choosing one size of list and building the circuit for this input size. Whenever the type system supports inductive types such as lists, the operator box then also takes a *shape* as a second argument, for deciding on the shape of the circuit to build. In recent works [77], ProtoQuipper's type system has been extended to very expressive *dependent types*, in order to characterize with a very fine-grain the shape structure of a family of circuits.

For instance, suppose that the program *P* sends `[qubit]` to `[qubit]`. It corresponds to a family of circuits, but if we pick a choice of input size *n*, the type gives no information on the output shape of the circuit—that is, the number of output wires. Maybe *P* duplicates each input wire? With dependent types, we can for instance index list-types with size and type *P* with

$$ \forall n. [qubit]_n \to [qubit]_{2n}. $$

This type tells us that *P* corresponds to a family of circuits of even output wires. This makes it possible to catch errors when using circuit combiners: for instance, the inverse operator can be typed with

$$ \forall n m. Circ([qubit]_m, [qubit]_n) \to Circ([qubit]_n, [qubit]_m) $$

The inverse of *P* then becomes a function of type

$$ \forall n. [qubit]_{2n} \to [qubit]_n. $$

In particular, this function can only be applied to lists of even sizes. This run-time error cannot be checked without shape information.

Although such a type system becomes very expressive, in general, it fails to feature a type inference algorithm, as this would require to be able to solve arbitrary arithmetic equations.

### 6.3.4 Dependent types and Proofs of Programs

To build a dependently typed language, an alternative approach is to embed it inside an existing host language with this feature: QWIRE [148, 147] follows this route and relies on the language and proof-assistant Coq [25]. While Quipper uses Haskell's monads to encode circuits, QWIRE capitalizes on Coq's inductive types within the formalism of the Calculus of Inductive Constructions (CiC) [146], the logical framework of Coq.

In Haskell, inductive types are limited in expressivity: without dependent types, it is not possible to impose constraints on the content of a datastructure. As circuits in Quipper are internally made of elements of an inductive type, it makes it impossible to forbid ill-defined constructions such as re-using an erased wire, or using twice a wire on a controlled-not, as shown in Fig. 11.

QWIRE can instead rely on dependent, inductive types to enforce such constraints on circuit constructions: instead of simply considering circuits as lists of gates, a circuit in QWIRE consists in a list of gates together with proofs that the gates are added in a sensible way —in other words, the constructors of the inductive type of circuits in QWIRE corresponds to a set of *typing rules* for writing valid circuits.

Interestingly enough, QWIRE does not have to rely on "!" type constructor to distinguish between duplicable and non-duplicable data. The idea is that instead of working in a linear-logic based type-system, QWIRE considers an equivalent linear-non-linear model [23]. In this paradigm, there are two intertwined languages:

* A linear language aimed at qubit manipulation and gate application: a program in this language is a circuit. The linearity of the type system enforces the necessary constraints so that e.g. Fig. 11 is indeed invalid;
to choosing one size of list and building the circuit for this input size. Whenever the type system supports inductive types such as lists, the operator box then also takes a *shape* as a second argument, for deciding on the shape of the circuit to build. In recent works [77], ProtoQuipper's type system has been extended to very expressive *dependent types*, in order to characterize with a very fine-grain the shape structure of a family of circuits.

For instance, suppose that the program *P* sends `[qubit]` to `[qubit]`. It corresponds to a family of circuits, but if we pick a choice of input size *n*, the type gives no information on the output shape of the circuit—that is, the number of output wires. Maybe *P* duplicates each input wire? With dependent types, we can for instance index list-types with size and type *P* with

$$ \forall n.[qubit]_n \to [qubit]_{2n}. $$

This type tells us that *P* corresponds to a family of circuits of even output wires. This makes it possible to catch errors when using circuit combiners: for instance, the inverse operator can be typed with

$$ \forall n m.Circ([qubit]_m, [qubit]_n) \to Circ([qubit]_n, [qubit]_m) $$

The inverse of *P* then becomes a function of type

$$ \forall n.[qubit]_{2n} \to [qubit]_n. $$

In particular, this function can only be applied to lists of even sizes. This run-time error cannot be checked without shape information.

Although such a type system becomes very expressive, in general, it fails to feature a type inference algorithm, as this would require to be able to solve arbitrary arithmetic equations.

### 6.3.4 Dependent types and Proofs of Programs

To build a dependently typed language, an alternative approach is to embed it inside an existing host language with this feature: QWIRE [148, 147] follows this route and relies on the language and proof-assistant Coq [25]. While Quipper uses Haskell's monads to encode circuits, QWIRE capitalizes on Coq's inductive types within the formalism of the Calculus of Inductive Constructions (CiC) [146], the logical framework of Coq.

In Haskell, inductive types are limited in expressivity: without dependent types, it is not possible to impose constraints on the content of a datastructure. As circuits in Quipper are internally made of elements of an inductive type, it makes it impossible to forbid ill-defined constructions such as re-using an erased wire, or using twice a wire on a controlled-not, as shown in Fig. 11.

QWIRE can instead rely on dependent, inductive types to enforce such constraints on circuit constructions: instead of simply considering circuits as lists of gates, a circuit in QWIRE consists in a list of gates together with proofs that the gates are added in a sensible way —in other words, the constructors of the inductive type of circuits in QWIRE corresponds to a set of *typing rules* for writing valid circuits.

Interestingly enough, QWIRE does not have to rely on `!` type constructor to distinguish between duplicable and non-duplicable data. The idea is that instead of working in a linear-logic based type-system, QWIRE considers an equivalent linear-non-linear model [23]. In this paradigm, there are two intertwined languages:

* A linear language aimed at qubit manipulation and gate application: a program in this language is a circuit. The linearity of the type system enforces the necessary constraints so that e.g. Fig. 11 is indeed invalid;
* A high-level, regular language–typically a lambda-calculus, with a regular type system. This language represents the “usual” programming paradigm where classical, conventional computation happens;

* Then there are two operations, akin to box and unbox, to move from the linear language to the classical language.

In the context of QWIRE, the classical, regular language is Coq and the linear language is encoded using the inductive type of circuits. As Coq features dependent types, QWIRE can then be regarded as a dependently-typed quantum programming language. However, due to the sophisticated type system, QWIRE does not feature a type inference algorithm.

### 6.3.5 Discussion

Type systems for quantum programming languages provide very efficient ways to encode and–whenever featuring a type inference algorithm–automatically verify some important properties of programs, and in particular to rule out at compile-time large classes of run-time errors specific to quantum computation. In particular, type systems have been used to characterize and enforce

* structure of parametric families of circuits;

* linearity of non-duplicable elements;

* control and inversion of only purely quantum circuits.

However, to be able to go further and characterize functional correctness with respect to specification, or validate the number of gates of a circuit, or catch subtle bugs involving concatenation of inverted circuits, one needs to move away from the simple linear type systems of quantum lambda-calculi and shift towards sophisticated dependent types, such as the extension ProtoQuipper-D [77] of ProtoQuipper, or the approach of QWIRE. The gain in expressiveness is then at the expense of automation [177, 148].

The quest for a finer trade-off, permitting automation while capturing some of what is currently only available with dependent type system is an active research area in the community.

# 7 High and Mid-Level Verification: Algorithms and Programs

Most quantum programming languages (QISKIT [153] Quipper [83], Liqui|〉 [193], Q# [181], PROJECTQ [180], SILQ [27], etc) embed features for quantum circuit manipulations within a standard classical programming language. Such circuit-building quantum languages is the current consensus for high-level executable quantum programming languages. A current major challenge is to link this language design paradigm with formally verified programming. In the present section, we introduce the main existing propositions in that direction.

## 7.1 Quantum Hoare Logic

Quantum Hoare logic (QHL) [37, 66, 105, 194, 185, 184, 19] is a general framework for reasoning about the classical control instructions over unitary operations in quantum algorithms. Referring again to Figure 1, the focus is on the interaction between the classical computer and the quantum co-processor, instead of the circuit analysis as in Section 5, or the gate to gate circuit building
* A high-level, regular language–typically a lambda-calculus, with a regular type system. This language represents the “usual” programming paradigm where classical, conventional computation happens;

* Then there are two operations, akin to `box` and `unbox`, to move from the linear language to the classical language.

In the context of QWIRE, the classical, regular language is `Coq` and the linear language is encoded using the inductive type of circuits. As `Coq` features dependent types, QWIRE can then be regarded as a dependently-typed quantum programming language. However, due to the sophisticated type system, QWIRE does not feature a type inference algorithm.

### 6.3.5 Discussion

Type systems for quantum programming languages provide very efficient ways to encode and–whenever featuring a type inference algorithm–*automatically* verify some important properties of programs, and in particular to rule out at compile-time large classes of run-time errors specific to quantum computation. In particular, type systems have been used to characterize and enforce

* structure of parametric families of circuits;

* linearity of non-duplicable elements;

* control and inversion of only purely quantum circuits.

However, to be able to go further and characterize functional correctness with respect to specification, or validate the number of gates of a circuit, or catch subtle bugs involving concatenation of inverted circuits, one needs to move away from the simple linear type systems of quantum lambda-calculi and shift towards sophisticated dependent types, such as the extension ProtoQuipper-D [77] of ProtoQuipper, or the approach of QWIRE. The gain in expressiveness is then at the expense of automation [177, 148].

The quest for a finer trade-off, permitting automation while capturing some of what is currently only available with dependent type system is an active research area in the community.

# 7 High and Mid-Level Verification: Algorithms and Programs

Most *quantum programming languages* (QISKIT [153] Quipper [83], Liqui|〉 [193], Q# [181], PROJECTQ [180], SILQ [27], etc) embed features for quantum circuit manipulations within a standard classical programming language. Such *circuit-building quantum languages* is the current consensus for high-level executable quantum programming languages. A current major challenge is to link this language design paradigm with formally verified programming. In the present section, we introduce the main existing propositions in that direction.

## 7.1 Quantum Hoare Logic

Quantum Hoare logic (QHL) [37, 66, 105, 194, 185, 184, 19] is a general framework for reasoning about the classical control instructions over unitary operations in quantum algorithms. Referring again to Figure 1, the focus is on the interaction between the classical computer and the quantum co-processor, instead of the circuit analysis as in Section 5, or the gate to gate circuit building
functions as in Sections 7.2 and 7.3. Therefore, we consider it as a high-level description of quantum algorithms.

It is based on the assertion method of Floyd and Hoare [74, 94]–attach each program point with an assertion and whenever the data flow reaches a program point the attached assertion should be satisfied—which was originated with Alan Turing [8]. Hoare’s approach enables (interactive) theorem proving for high-level algorithmic description verification that proceeds at the same abstraction level as the language itself. This makes verification more human-friendly than lower-level (machine-friendly) verification.

### 7.1.1 Quantum Programming Language: Quantum WHILE-Programs

The guideline for the hybrid model introduced in Section 2.1.1 is summed up by the slogan “quantum data and classical control” [168]: quantum data can be superposed and entangled, they are manipulated by basic quantum operations–unitary evolution and measurement, but the high-level control is still classical (e.g. branch, loops, etc).

In light of this slogan, QHL introduces a minimal programming language for describing quantum algorithms [195]. We follow [194] for the introduction of QHL technical environment. Let $q$ (resp. $\bar{q}$) be a quantum variable (resp. a list of quantum variables); let $U$ be a unitary operator acting on the qubits $\bar{q}$ and let $M \triangleq \{M_m\}_m$ with $\sum_m M_m^\dagger M_m = I$ be a measurement on the qubits $\bar{q}$, each $M_m$ corresponding to a measurement result $m$ (see Section 2.1.5). As a special case, let $M' \triangleq \{M_0, M_1\}$ with $M_0^\dagger M_0 + M_1^\dagger M_1 = I$. Then quantum WHILE-programs are generated by the following syntax.

<table><tr><td>$S \triangleq \textbf{skip}$</td><td>No operation</td></tr><tr><td>$q := |0\rangle$</td><td>Initialization</td></tr><tr><td>$\bar{q} := U$</td><td>Unitary operation</td></tr><tr><td>$S_1; S_2$</td><td>Sequential composition</td></tr><tr><td>$\textbf{if } \Box m \cdot M[\bar{q}] = m \to S_m \textbf{ fi}$</td><td>Probabilistic branching</td></tr><tr><td>$\textbf{while } M'[\bar{q}] = 1 \textbf{ do } S_0 \textbf{ od}$</td><td>Probabilistic while loop</td></tr></table>

The intended semantics of language constructs above is similar to that of their classical counterparts. To illustrate the quantum features contained in these constructs, we make the following comments:

(i) in the initialization, the choice of a fixed state $|0\rangle$ is without loss of generality, since any known quantum state can be prepared by applying a unitary operator to $|0\rangle$;

(ii) according to Born rule, measurement results follow a probabilistic law. Since they lie on measurement result observations, branching (resp. while loops) is therefore probabilistic. It creates different branches $\{S_m\}_m$ (resp. $\{\textbf{skip}, S_0\}$), chosen according to outcomes of the measurement $M$ (resp. $M'$) on the qubits $\bar{q}$.

We refer the reader to [194] for a detailed exposition of the syntax above.

**Example 7.1** (Preparation of the Bell state $|\beta_{00}\rangle$). Let $p$ and $q$ be quantum variables, each denoting one qubit. Then the following program initiates them to $|0\rangle$ and implements the circuit from Figure 2, preparing state $|\beta_{00}\rangle$ from Example 2.1.:

$$ \beta_{00} \triangleq p := |0\rangle; q := |0\rangle; p := H; (p,q) := \text{CNOT} $$

Note that the quantum programming language defined above is in the spirit of the hybrid circuit model presented in Section 2. Indeed, the basic sequence of quantum operations (initialization, unitary operation, and measurement) are meant to be interpreted as a generalized quantum circuit to be executed on a quantum co-processor; and post-measurement branchings (in, e.g., probabilistic branching and while loop) are meant to be controlled by a classical computer.
functions as in Sections 7.2 and 7.3. Therefore, we consider it as a high-level description of quantum algorithms.

It is based on the assertion method of Floyd and Hoare [74, 94]–attach each program point with an assertion and whenever the data flow reaches a program point the attached assertion should be satisfied—which was originated with Alan Turing [8]. Hoare’s approach enables (interactive) theorem proving for high-level algorithmic description verification that proceeds at the same abstraction level as the language itself. This makes verification more human-friendly than lower-level (machine-friendly) verification.

### 7.1.1 Quantum Programming Language: Quantum WHILE-Programs

The guideline for the hybrid model introduced in Section 2.1.1 is summed up by the slogan “quantum data and classical control” [168]: quantum data can be superposed and entangled, they are manipulated by basic quantum operations–unitary evolution and measurement, but the high-level control is still classical (e.g. branch, loops, etc).

In light of this slogan, QHL introduces a minimal programming language for describing quantum algorithms [195]. We follow [194] for the introduction of QHL technical environment. Let $q$ (resp. $\bar{q}$) be a quantum variable (resp. a list of quantum variables); let $U$ be a unitary operator acting on the qubits $\bar{q}$ and let $M \triangleq \{M_m\}_m$ with $\sum_m M_m^\dagger M_m = I$ be a measurement on the qubits $\bar{q}$, each $M_m$ corresponding to a measurement result $m$ (see Section 2.1.5). As a special case, let $M' \triangleq \{M_0, M_1\}$ with $M_0^\dagger M_0 + M_1^\dagger M_1 = I$. Then quantum WHILE-programs are generated by the following syntax.

<table><tr><td>$S \triangleq \textbf{skip}$</td><td>No operation</td></tr><tr><td>$q := |0\rangle$</td><td>Initialization</td></tr><tr><td>$\bar{q} := U$</td><td>Unitary operation</td></tr><tr><td>$S_1; S_2$</td><td>Sequential composition</td></tr><tr><td>$\textbf{if } \Box m \cdot M[\bar{q}] = m \to S_m \textbf{ fi}$</td><td>Probabilistic branching</td></tr><tr><td>$\textbf{while } M'[\bar{q}] = 1 \textbf{ do } S_0 \textbf{ od}$</td><td>Probabilistic while loop</td></tr></table>

The intended semantics of language constructs above is similar to that of their classical counterparts. To illustrate the quantum features contained in these constructs, we make the following comments:

(i) in the initialization, the choice of a fixed state $|0\rangle$ is without loss of generality, since any known quantum state can be prepared by applying a unitary operator to $|0\rangle$;

(ii) according to Born rule, measurement results follow a probabilistic law. Since they lie on measurement result observations, branching (resp. while loops) is therefore probabilistic. It creates different branches $\{S_m\}_m$ (resp. $\{\textbf{skip}, S_0\}$), chosen according to outcomes of the measurement $M$ (resp. $M'$) on the qubits $\bar{q}$.

We refer the reader to [194] for a detailed exposition of the syntax above.

**Example 7.1** (Preparation of the Bell state $|\beta_{00}\rangle$). Let $p$ and $q$ be quantum variables, each denoting one qubit. Then the following program initiates them to $|0\rangle$ and implements the circuit from Figure 2, preparing state $|\beta_{00}\rangle$ from Example 2.1.:

$$ \beta_{00} \triangleq p := |0\rangle; q := |0\rangle; p := H; (p,q) := \text{CNOT} $$

Note that the quantum programming language defined above is in the spirit of the hybrid circuit model presented in Section 2. Indeed, the basic sequence of quantum operations (initialization, unitary operation, and measurement) are meant to be interpreted as a generalized quantum circuit to be executed on a quantum co-processor; and post-measurement branchings (in, e.g., probabilistic branching and while loop) are meant to be controlled by a classical computer.
### 7.1.2 Quantum States, Operations and Predicates

Measuring a quantum state transforms it, following the Born rule (see Section 2.1.2). The resulting probability distribution over quantum states is formalized as a mixed state (as opposed to pure states, see Section 2.1.5). For example, a measurement on any pure quantum state $|+\rangle \triangleq \frac{1}{\sqrt{2}}(|0\rangle + |1\rangle)$ or $|-\rangle \triangleq \frac{1}{\sqrt{2}}(|0\rangle - |1\rangle)$ will result in the mixed state $\mathbb{E} = \{(\frac{1}{2}, |0\rangle), (\frac{1}{2}, |1\rangle)\}$, with states $|0\rangle$ and $|1\rangle$ occurring with an equal probability of $\frac{1}{2}$ (notice that this observation makes both states $|+\rangle$ and $|-\rangle$ impossible to distinguish by simple measurement).

In this way, the representation of the final state of applying a series of measurements to a quantum state could expand exponentially. To address this issue, a square-matrix representation of quantum states, i.e. partial density operator, is adopted instead. For example, pure quantum state $|+\rangle$ is represented as $|+\rangle \langle +|$, and mixed quantum state $\mathbb{E}$ as $\frac{1}{2}|0\rangle \langle 0| + \frac{1}{2}|1\rangle \langle 1|$. See Section 2.1.5 for a brief introduction to partial density operators, and [168, 195, 139] for further details.

If we see the matrix representation of a quantum state (partial density operator) as a linear operator, then a quantum operation—initialization, unitary evolution and measurement—can be thought of as a super operator, i.e. a function from linear operators to linear operators. What's interesting is that every quantum WHILE-program defined above can be interpreted as a quantum operation, and partial density operators are closed under quantum operations. This justifies the success of representing quantum states as partial density operators and defining the denotational semantics of quantum programs as quantum operations [168, 195].

Following [56], a quantum predicate on vector space $H$ is defined as a Hermitian operator $M$ between the zero operator $0_H$ (representing the contradiction) and the identity operator $I_H$ (representing the tautology). Instead of the usual binary satisfaction judgment, QHL evaluates the satisfaction of a predicate by a state as a real value between 0 (false) and 1 (true). It is defined as the trace $\text{tr}(M\rho)$ of the product $M\rho$. Intuitively, it represents the expectation for the truth value of $M$ in the mixed state $\rho$ (which is, again, a probability distribution over pure states).

Then, the intuition of implication between predicates is also probabilistic. It is filled by the Löowner order $M \sqsubseteq N$, relating operators $M$ and $N$, if and only if, for any state $\rho$, the expectation truth value of $N$ in $\rho$ is more or equal to that of $M$ in $\rho$. This condition is formalized as $\text{tr}(M\rho) \le \text{tr}(N\rho)$ for all states $\rho$ (See, e.g., [194, Lemma 2.1]).

Adopting such quantum predicates as assertions, among many others (e.g., interpreted as physical observables), provides simple expression means for many properties of quantum effects. For example, quantum predicate $|+\rangle \langle +|$ expresses that a state $\rho$ is in the equal superposition $|+\rangle$ with probability $\text{tr}(|+\rangle \langle +|\rho)$; quantum predicate $|\beta_{00}\rangle \langle \beta_{00}|$ expresses that a state $\rho$ is in the maximal entanglement $|\beta_{00}\rangle$ with probability $\text{tr}(|\beta_{00}\rangle \langle \beta_{00}|\rho)$, etc.

### 7.1.3 Quantum Program Verification

For now, a quantum (partial) correctness formula can be the Hoare's triple $\{P\} S \{Q\}$, where $S$ is a quantum WHILE-program, and $P, Q$ are quantum predicates. To define the partial-correctness semantics of quantum Hoare's triples, in the sequel, let $\llbracket S \rrbracket$ denote the semantic function of $S$ (Note that $\llbracket S \rrbracket$ is a quantum operation defined by induction on $S$, cf. [195]), and $\llbracket S \rrbracket(\rho)$ the output of $S$ on the input $\rho$.

**Definition 7.1** (Semantics of partial correctness, cf. [194]). Let $P, Q$ be quantum predicates and $S$ a quantum WHILE-program. We say that $S$ is (partially) correct w.r.t. precondition $P$ and postcondition $Q$, written $\models \{P\} S \{Q\}$, if

$$ \forall \rho, \quad \text{tr}(P\rho) \le \text{tr}(Q\llbracket S \rrbracket(\rho)) + [\text{tr}(\rho) - \text{tr}(\llbracket S \rrbracket(\rho))]. \quad (4) $$
### 7.1.2 Quantum States, Operations and Predicates

Measuring a quantum state transforms it, following the Born rule (see Section 2.1.2). The resulting probability distribution over quantum states is formalized as a mixed state (as opposed to pure states, see Section 2.1.5). For example, a measurement on any pure quantum state $|+\rangle \triangleq \frac{1}{\sqrt{2}}(|0\rangle + |1\rangle)$ or $|-\rangle \triangleq \frac{1}{\sqrt{2}}(|0\rangle - |1\rangle)$ will result in the mixed state $\mathbb{E} = \{(\frac{1}{2}, |0\rangle), (\frac{1}{2}, |1\rangle)\}$, with states $|0\rangle$ and $|1\rangle$ occurring with an equal probability of $\frac{1}{2}$ (notice that this observation makes both states $|+\rangle$ and $|-\rangle$ impossible to distinguish by simple measurement).

In this way, the representation of the final state of applying a series of measurements to a quantum state could expand exponentially. To address this issue, a square-matrix representation of quantum states, i.e. partial density operator, is adopted instead. For example, pure quantum state $|+\rangle$ is represented as $|+\rangle \langle +|$, and mixed quantum state $\mathbb{E}$ as $\frac{1}{2}|0\rangle \langle 0| + \frac{1}{2}|1\rangle \langle 1|$. See Section 2.1.5 for a brief introduction to partial density operators, and [168, 195, 139] for further details.

If we see the matrix representation of a quantum state (partial density operator) as a linear operator, then a quantum operation—initialization, unitary evolution and measurement—can be thought of as a super operator, i.e. a function from linear operators to linear operators. What's interesting is that every quantum WHILE-program defined above can be interpreted as a quantum operation, and partial density operators are closed under quantum operations. This justifies the success of representing quantum states as partial density operators and defining the denotational semantics of quantum programs as quantum operations [168, 195].

Following [56], a quantum predicate on vector space $H$ is defined as a Hermitian operator $M$ between the zero operator $0_H$ (representing the contradiction) and the identity operator $I_H$ (representing the tautology). Instead of the usual binary satisfaction judgment, QHL evaluates the satisfaction of a predicate by a state as a real value between 0 (false) and 1 (true). It is defined as the trace $\text{tr}(M\rho)$ of the product $M\rho$. Intuitively, it represents the expectation for the truth value of $M$ in the mixed state $\rho$ (which is, again, a probability distribution over pure states).

Then, the intuition of implication between predicates is also probabilistic. It is filled by the Löowner order $M \sqsubseteq N$, relating operators $M$ and $N$, if and only if, for any state $\rho$, the expectation truth value of $N$ in $\rho$ is more or equal to that of $M$ in $\rho$. This condition is formalized as $\text{tr}(M\rho) \le \text{tr}(N\rho)$ for all states $\rho$ (See, e.g., [194, Lemma 2.1]).

Adopting such quantum predicates as assertions, among many others (e.g., interpreted as physical observables), provides simple expression means for many properties of quantum effects. For example, quantum predicate $|+\rangle \langle +|$ expresses that a state $\rho$ is in the equal superposition $|+\rangle$ with probability $\text{tr}(|+\rangle \langle +|\rho)$; quantum predicate $|\beta_{00}\rangle \langle \beta_{00}|$ expresses that a state $\rho$ is in the maximal entanglement $|\beta_{00}\rangle$ with probability $\text{tr}(|\beta_{00}\rangle \langle \beta_{00}|\rho)$, etc.

### 7.1.3 Quantum Program Verification

For now, a quantum (partial) correctness formula can be the Hoare's triple $\{P\} S \{Q\}$, where $S$ is a quantum WHILE-program, and $P, Q$ are quantum predicates. To define the partial-correctness semantics of quantum Hoare's triples, in the sequel, let $\llbracket S \rrbracket$ denote the semantic function of $S$ (Note that $\llbracket S \rrbracket$ is a quantum operation defined by induction on $S$, cf. [195]), and $\llbracket S \rrbracket(\rho)$ the output of $S$ on the input $\rho$.

**Definition 7.1** (Semantics of partial correctness, cf. [194]). Let $P, Q$ be quantum predicates and $S$ a quantum WHILE-program. We say that $S$ is (partially) correct w.r.t. precondition $P$ and postcondition $Q$, written $\models \{P\} S \{Q\}$, if

$$ \forall \rho, \quad \text{tr}(P\rho) \le \text{tr}(Q\llbracket S \rrbracket(\rho)) + [\text{tr}(\rho) - \text{tr}(\llbracket S \rrbracket(\rho))]. \quad (4) $$
Note that Inequality (4) can be seen as a probabilistic version of the following statement: if state $\rho$ satisfies predicate $P$, then, executing program $S$ on input $\rho$, either $S$ fails to terminate or the resulting state $[S](\rho)$ satisfies predicate $Q$.

<table><caption>Table 2: Proof system for partial correctness.</caption><tr><td>(Skip Axiom)</td><td>{P} <b>skip</b> {P}</td></tr><tr><td>(Init Axiom)</td><td>{&Sigma;<sub>i</sub>|i&rangle;<sub>q</sub> &lang;0|P|0&rangle;<sub>q</sub> &lang;i&rangle;}&rangle; q := |0&rangle; {P}</td></tr><tr><td>(Unit Axiom)</td><td>{U<sup>&dagger;</sup>PU} q&#773; *:= U {P}</td></tr><tr><td>(Comp Rule)</td><td>{P} S<sub>1</sub> {Q} {Q} S<sub>2</sub> {R} {P} S<sub>1</sub>;S<sub>2</sub> {R}</td></tr><tr><td>(If Rule)</td><td>{P<sub>m</sub>} S<sub>m</sub> {Q} for all m {&Sigma;<sub>m</sub>M<sub>m</sub><sup>&dagger;</sup>P<sub>m</sub>M<sub>m</sub>} if &square;m &middot; M[q&#773;] = m &rarr; S<sub>m</sub> <b>fi</b> {Q}</td></tr><tr><td>(Par Loop Rule)</td><td>{P} S<sub>0</sub> {M<sub>0</sub><sup>&dagger;</sup>QM<sub>0</sub>+M<sub>1</sub><sup>&dagger;</sup>PM<sub>1</sub>} {M<sub>0</sub><sup>&dagger;</sup>QM<sub>0</sub>+M<sub>1</sub><sup>&dagger;</sup>PM<sub>1</sub>} <b>while</b> M'[q&#773;]=1 <b>do</b> S<sub>0</sub> <b>od</b> {Q}</td></tr><tr><td>(Order Rule)</td><td>P &sqsubseteq; P' {P'} S {Q'} Q' &sqsubseteq; Q {P} S {Q}</td></tr></table>

The axiom system for proving partial correctness of quantum WHILE-programs is composed of axioms and inference rules manipulating quantum Hoare's triples [194]. It is shown in Table 2 (where {|i&rangle;}_q is the computational basis for quantum variable $q$). Remark that each of these rules and axioms follows the assertion method. Here we only show how to derive the most complex rule (Par Loop Rule). The derivation of other proof rules can be done similarly.

**Intuition of (Par Loop Rule).** To derive (Par Loop Rule), by assertion method, we attach each program point, say $l_1, l_2, l_3$, of a WHILE-statement with an assertion, say $R, P, Q$, respectively:

$$ \{l_1 : R\} \text{ while } M'[\bar{q}] = 1 \text{ do } \{l_2 : P\} S \text{ od } \{l_3 : Q\} $$

Fix the input $\rho$ at the program point $l_1$ satisfying the assertion $R$. By semantics of a WHILE loop, after the measurement $M'$, one part $M_1\rho M_1^\dagger$ of the input will go to the loop body through the program point $l_2$ where the assertion $P$ will be satisfied; the other part $M_0\rho M_0^\dagger$ will leave the while loop through the program point $l_3$ in which the assertion $Q$ will be satisfied. Hence:

$$ tr(R\rho) \leq tr(Q(M_0\rho M_0^\dagger)) + tr(P(M_1\rho M_1^\dagger)) $$

Due to the arbitrariness of $\rho$, by properties of the trace function and Löowner order, we have that $R \sqsubseteq M_0^\dagger QM_0 + M_1^\dagger PM_1$. Then, by weakening $R$ to $M_0^\dagger QM_0 + M_1^\dagger PM_1$ and lifting the above reasoning process into an inference rule, (Par Loop Rule) follows.

The following example illustrates how to derive a partially correct quantum Hoare triple using the axioms and inference rules presented above.

**Example 7.2** (Specification and correctness proof for the $|\beta_{00}\rangle$ state construction program). *Recall from Example 7.1 the definition of quantum program $\beta_{00}$:*

$$ \beta_{00} \triangleq p := |0\rangle; q := |0\rangle; p *:= H; (p,q) *:= CNOT $$
Note that Inequality (4) can be seen as a probabilistic version of the following statement: if state $\rho$ satisfies predicate $P$, then, executing program $S$ on input $\rho$, either $S$ fails to terminate or the resulting state $\llbracket S \rrbracket(\rho)$ satisfies predicate $Q$.

<table><caption>Table 2: Proof system for partial correctness.</caption><tr><td>(Skip Axiom)</td><td>{P} <b>skip</b> {P}</td></tr><tr><td>(Init Axiom)</td><td>{∑<sub>i</sub>|i⟩<sub>q</sub> ⟨0|P|0⟩<sub>q</sub> ⟨i|} q := |0⟩ {P}</td></tr><tr><td>(Unit Axiom)</td><td>{U<sup>†</sup>PU} ¯q *:= U {P}</td></tr><tr><td>(Comp Rule)</td><td>{P} S<sub>1</sub> {Q} {Q} S<sub>2</sub> {R} <br> {P} S<sub>1</sub>;S<sub>2</sub> {R}</td></tr><tr><td>(If Rule)</td><td>{P<sub>m</sub>} S<sub>m</sub> {Q} for all m <br> {∑<sub>m</sub> M<sup>†</sup><sub>m</sub>P<sub>m</sub>M<sub>m</sub>} if □m·M[¯q] = m→S<sub>m</sub> <b>fi</b> {Q}</td></tr><tr><td>(Par Loop Rule)</td><td>{P} S<sub>0</sub> {M<sup>†</sup><sub>0</sub>QM<sub>0</sub>+M<sup>†</sup><sub>1</sub>PM<sub>1</sub>} <br> {M<sup>†</sup><sub>0</sub>QM<sub>0</sub>+M<sup>†</sup><sub>1</sub>PM<sub>1</sub>} <b>while</b> M'[¯q]=1 <b>do</b> S<sub>0</sub> <b>od</b> {Q}</td></tr><tr><td>(Order Rule)</td><td><u>P</u> ⊑ <u>P'</u> {P'} S {Q'} Q' ⊑ <u>Q</u> <br> {P} S {Q}</td></tr></table>

The axiom system for proving partial correctness of quantum WHILE-programs is composed of axioms and inference rules manipulating quantum Hoare's triples [194]. It is shown in Table 2 (where {|i⟩}q is the computational basis for quantum variable q). Remark that each of these rules and axioms follows the assertion method. Here we only show how to derive the most complex rule (Par Loop Rule). The derivation of other proof rules can be done similarly.

**Intuition of (Par Loop Rule).** To derive (Par Loop Rule), by assertion method, we attach each program point, say $l_1, l_2, l_3$, of a WHILE-statement with an assertion, say $R, P, Q$, respectively:

$$ \{l_1 : R\} \text{ while } M'[\bar{q}] = 1 \text{ do } \{l_2 : P\} S \text{ od } \{l_3 : Q\} $$

Fix the input $\rho$ at the program point $l_1$ satisfying the assertion $R$. By semantics of a WHILE loop, after the measurement $M'$, one part $M_1\rho M_1^\dagger$ of the input will go to the loop body through the program point $l_2$ where the assertion $P$ will be satisfied; the other part $M_0\rho M_0^\dagger$ will leave the while loop through the program point $l_3$ in which the assertion $Q$ will be satisfied. Hence:

$$ \mathrm{tr}(R\rho) \le \mathrm{tr}(Q(M_0\rho M_0^\dagger)) + \mathrm{tr}(P(M_1\rho M_1^\dagger)) $$

Due to the arbitrariness of $\rho$, by properties of the trace function and Löowner order, we have that $R \sqsubseteq M_0^\dagger QM_0 + M_1^\dagger PM_1$. Then, by weakening $R$ to $M_0^\dagger QM_0 + M_1^\dagger PM_1$ and lifting the above reasoning process into an inference rule, (Par Loop Rule) follows.

The following example illustrates how to derive a partially correct quantum Hoare triple using the axioms and inference rules presented above.

**Example 7.2** (Specification and correctness proof for the $|\beta_{00}\rangle$ state construction program). *Recall from Example 7.1 the definition of quantum program $\beta_{00}$:*

$$ \beta_{00} \triangleq p := |0\rangle; q := |0\rangle; p *:= H; (p,q) *:= CNOT $$
To show (partial) correctness of this program, it suffices to prove

$$ \{I_p \otimes I_q\} \beta_{00} \{|\beta_{00}\rangle_{p,q} \langle\beta_{00}|\} \qquad (5) $$

This can be done as follows. By sake of space we need to decompose the derivation tree. We first derive specifications for the initialization instructions:

$$ \frac{\substack{\text{Init Axiom} \\ \{I_p \otimes I_q\} p := |0\rangle \{ |0\rangle_p \langle 0| \otimes I_q \} \\ \qquad \{ |0\rangle_p \langle 0| \otimes I_q \} q := |0\rangle \{ |0\rangle_p \langle 0| \otimes |0\rangle_q \langle 0| \} \\ \qquad \{ I_p \otimes I_q \} p := |0\rangle; q := |0\rangle \{ |0\rangle_p \langle 0| \otimes |0\rangle_q \langle 0| \} \quad (i)}}{\text{Comp Rule}} $$

Then come the unitary application instructions. We set the following abbreviations for Hoare triples:

$$ (ii) \quad := \{ |0\rangle_p \langle 0| \otimes |0\rangle_q \langle 0| \} p := H \{ |+\rangle_p \langle +| \otimes |0\rangle_q \langle 0| \} $$

$$ (iii) := \{ |+\rangle_p \langle +| \otimes |0\rangle_q \langle 0| \} (p,q) := \text{CNOT} \{ |\beta_{00}\rangle_{p,q} \langle \beta_{00}| \} $$

They are instances of axioms and we can combine them:

$$ \frac{\overline{(ii)} \quad \text{Init Axiom} \quad \overline{(iii)} \quad \text{Init Axiom}}{\{ |0\rangle_p \langle 0| \otimes |0\rangle_q \langle 0| \} p := H; (p,q) := \text{CNOT} \{ |\beta_{00}\rangle_{p,q} \langle \beta_{00}| \} \quad (iv)} \quad \text{Comp Rule} $$

Finally, the two preceding proof tree branch together via the sequential composition rule, which achieves the derivation:

$$ \frac{\qquad (i) \qquad (iv)}{\{I_p \otimes I_q\} \beta_{00} \{|\beta_{00}\rangle_{p,q} \langle\beta_{00}|\}} \quad \text{Comp Rule} $$

### 7.1.4 Implementations and Extensions

Several works have taken advantage of extended Quantum Hoare Logic, e.g. algorithmic analysis of termination problem [127] or characterization and generation of loop invariants (i.e. $M_0^\dagger QM_0 + M_1^\dagger PM_1$ in (Par Loop Rule)) [198].

The practical illustration of QHL can be found in Liu et al. paper [132], containing an implementation in ISABELLE/HOL together with a formalization of Grover [84] and Quantum Phase Estimation (QPE [111]) algorithms. Nevertheless in these examples, the central verification part is assumed through Python libraries uses.

More recent work [131] includes full proof for a parametrized version of Grover's search algorithm. It constitutes an illustration of QHL use on a non-trivial example.

### 7.1.5 Other Quantum Hoare Logics

In addition to the framework introduced above, applying Hoare Logic methods to quantum processes brought several additional developments, focusing on different aspects of quantum computations. We introduce a few of these QHL related framework in the following paragraphs.
**Quantum Hoare Logic with ghost variables.** One of the principal shortcuts of [194] comes from the limitations of the specification language. In [184], the author in particular targets the possibility to characterize probabilistic distributions of values. His proposition introduces *ghost* variables in the specifications language: a *ghost* variable does not occur in the program but only in its specifications. In [184], a ghost variable is interpreted under an implicit existential quantification. Ghost variables enable, in particular, to explicitly refer to discarded, measured or overwritten qubits. In addition to probability distribution definitions, it brings several features to the expressive power of the specifications language, such as separability-unentanglement-of variables or the fact, for a given variable, to hold for a classical data value.

**Quantum Hoare Logic with classical variables.** With similar concern, [67] extends QHL specifications with classical variables. In the specification and verification of algorithms of practical use, holding classical information is indeed crucial. It enables, for example, describing and specifying an algorithm holding classical parameters or a hybrid program intertwining classical and quantum instructions (see Section 2.1.1).

Hence, the semantics relies on so-called *cq-states* (classical/quantum states) made of both:

* a classical variable assignment for the interpretation of classical variables;

* a density operator interpreting quantum variables.

This extension of the semantics induces an extension of the proof system, which is proved sound and complete—with respect to partial correctness. Interestingly, the paper presents detailed specified case studies, including Grover's and Shor's algorithms.

**Robustness analysis** is another important line of work, initiated in [97] as a continuation of QHL. The different solutions presented so far rely on the implicit assumption that quantum gates are applied deterministically as indicated by their matrix semantics. Still, as stated in Section 2.3.2, this noise-free modeling is not perfectly accurate in the NISQ era.

A more realistic description of the behavior of a gate would consider several different possible behaviors, weighed with their respective probabilities of occurrence: the *intended* one, expected by the semantics, and one or several additional erroneous behaviors<fnref n="10" />.

Interestingly, in this setting, the application of a quantum gate is formally represented as a probability distribution over unitaries. Hence, a non-deterministic gate application naturally formalizes in the formalism of super operators acting over density operators.

Then, a metrics is defined for measuring the difference between the behavior of a quantum system under a given error scheme (for each gate application, the mention of a possible erroneous behavior together with its probability of occurrence) and its intended behavior. It is called the *trace distance* and serves as an evaluation for the robustness of the implementation.

Among other case studies, the method is illustrated by evaluating a minimal quantum error correcting scheme.

**Quantum separation logic** [201] aims at simplifying quantum programs specifications. The leading observation is that, while quantum programs often manipulate big quantum circuits, with matrix semantics growing exponentially over their width, many quantum algorithms proceed via

<footnote n="10">¹⁰Strictly speaking, the language in 2.3.2 is limited to considering up to one possible error per gate application. But this is without lost of generality since more sophisticated scenarios can be encoded through, eg., the replacement of gate application intervals by potentially erroneous identity transformations.</footnote>
**Quantum Hoare Logic with ghost variables.** One of the principal shortcuts of [194] comes from the limitations of the specification language. In [184], the author in particular targets the possibility to characterize probabilistic distributions of values. His proposition introduces *ghost* variables in the specifications language: a *ghost* variable does not occur in the program but only in its specifications. In [184], a ghost variable is interpreted under an implicit existential quantification. Ghost variables enable, in particular, to explicitly refer to discarded, measured or overwritten qubits. In addition to probability distribution definitions, it brings several features to the expressive power of the specifications language, such as separability-unentanglement-of variables or the fact, for a given variable, to hold for a classical data value.

**Quantum Hoare Logic with classical variables.** With similar concern, [67] extends QHL specifications with classical variables. In the specification and verification of algorithms of practical use, holding classical information is indeed crucial. It enables, for example, describing and specifying an algorithm holding classical parameters or a hybrid program intertwining classical and quantum instructions (see Section 2.1.1).

Hence, the semantics relies on so-called *cq-states* (classical/quantum states) made of both:

* a classical variable assignment for the interpretation of classical variables;

* a density operator interpreting quantum variables.

This extension of the semantics induces an extension of the proof system, which is proved sound and complete—with respect to partial correctness. Interestingly, the paper presents detailed specified case studies, including Grover's and Shor's algorithms.

**Robustness analysis** is another important line of work, initiated in [97] as a continuation of QHL. The different solutions presented so far rely on the implicit assumption that quantum gates are applied deterministically as indicated by their matrix semantics. Still, as stated in Section 2.3.2, this noise-free modeling is not perfectly accurate in the NISQ era.

A more realistic description of the behavior of a gate would consider several different possible behaviors, weighed with their respective probabilities of occurrence: the *intended* one, expected by the semantics, and one or several additional erroneous behaviors<fnref n="10" />.

Interestingly, in this setting, the application of a quantum gate is formally represented as a probability distribution over unitaries. Hence, a non-deterministic gate application naturally formalizes in the formalism of super operators acting over density operators.

Then, a metrics is defined for measuring the difference between the behavior of a quantum system under a given error scheme (for each gate application, the mention of a possible erroneous behavior together with its probability of occurrence) and its intended behavior. It is called the *trace distance* and serves as an evaluation for the robustness of the implementation.

Among other case studies, the method is illustrated by evaluating a minimal quantum error correcting scheme.

**Quantum separation logic** [201] aims at simplifying quantum programs specifications. The leading observation is that, while quantum programs often manipulate big quantum circuits, with matrix semantics growing exponentially over their width, many quantum algorithms proceed via

<footnote n="10">¹⁰Strictly speaking, the language in 2.3.2 is limited to considering up to one possible error per gate application. But this is without lost of generality since more sophisticated scenarios can be encoded through, eg., the replacement of gate application intervals by potentially erroneous identity transformations.</footnote>
sequences of local manipulations over quantum sub-registers. The authors exhibit the examples of Quantum Machine Learning [26] and Variational Quantum Algorithms (VQA [135]), which are among the most promising classes of algorithms in the NISQ era (see Section 2.3.2).

To efficiently reason about state evolution in such implementations, a Quantum Separation Logic is proposed, together with a dedicated proof system. This logic allows the expression of local manipulation on separated quantum registers while maintaining the state of the rest of the register. The approach is probed with case studies from both quantum programming analysis (VQA) and communication protocols security checks (one-time pad and secret sharing).

**Quantum relational Hoare logic** [185, 19] allows to reason about how the outputs of two quantum programs relate to each other given a relation between their inputs, which can be used to analyze security of post-quantum cryptography and quantum protocols.

**Quantum Hoare type theory** [177] is inspired by classical Hoare type theory and extends the Quantum IO Monad [3] by indexing it with pre- and postconditions that serve as program specifications, which has the potential to be a unified system for programming, specifying, and reasoning about quantum programs.

**Quantum dynamic logic.** We end up this section by mentioning a line of work that is not a strict extension or application of Hoare Logic [94], but shares similar concerns and related solutions. Just as QHL and its extensions, dynamic logic formalizes the evolution of a state along the execution of a process acting over it.

Dynamic logic inherits from the modal logic apparatus where, in addition to propositional logic connectives, modalities `□` and `◇` are intruded. Intuitively, given a formula $\phi$, `□\phi` means that $\phi$ is necessarily true and `◇\phi` means that $\phi$ is possibly true. The standard semantics, based on Kripke models [115], helps catching this intuition. A Kripke model $\mathcal{K}$ is made of a set of states $S$ holding, each, a valuation $P: S \to \{\text{true, false}\}$ for a set of propositional variables $P$. And the modality is interpreted through an accessibility relation $R \subseteq S \times S$. For example, given a propositional variable $p$, `□p` (resp. `◇p`) is true in state $s$, written $\mathcal{K},s \models \Box p$ iff $p$ (resp. $\mathcal{K},s \models \Diamond p$) is true if $p$ is true in every (resp. at least one) state $s'$ such that $(s,s') \in R$.

In dynamic logic, several modalities coexist, formalizing a set of actions. Hence, given an action $a$, formula $[a]\phi$ is true iff $\phi$ is always true after performing action $a$. Actions can combine together, for example $[a;a']\phi$ means that $\phi$ is always true after the successive performance of actions $a$ and $a'$.

In their *Logic of Quantum Programs* (LQP [14, 15]), Baltag and Smets designed a quantum version of dynamic logic. Here, states correspond to one-dimensional subspaces of a Hilbert space for a quantum register. Actions are of two kinds: a *test* encodes a measurement through the set of projection transitions corresponding to the different possible outcomes (for example, given formulas $\varphi$ and $\psi$, $\varphi?\psi$ is satisfied in the state of evaluation if and only if any state satisfying $\varphi$ after measurement-any successful test for $\varphi$-also satisfies $\psi$), and proper *actions* deterministically encode unitary state transformations). In [14], the framework is illustrated by a correction proof for the teleportation and quantum secret sharing protocols. Baltag and Smets link their work to similar quantum logics as in [34].

Note that to treat measurement, LQP formalizes informations about the set of states that are possibly reachable, but the language does not hold any notion of probability. This shortcut is overcome in [13], where the authors introduce a probabilistic test modality characterizing, for any formula $\varphi$ and rational $x \in [0, 1]$, that a test for $\varphi$ has probability at least $x$ to succeed from the evaluation state.
sequences of local manipulations over quantum sub-registers. The authors exhibit the examples of Quantum Machine Learning [26] and Variational Quantum Algorithms (VQA [135]), which are among the most promising classes of algorithms in the NISQ era (see Section 2.3.2).

To efficiently reason about state evolution in such implementations, a Quantum Separation Logic is proposed, together with a dedicated proof system. This logic allows the expression of local manipulation on separated quantum registers while maintaining the state of the rest of the register. The approach is probed with case studies from both quantum programming analysis (VQA) and communication protocols security checks (one-time pad and secret sharing).

**Quantum relational Hoare logic** [185, 19] allows to reason about how the outputs of two quantum programs relate to each other given a relation between their inputs, which can be used to analyze security of post-quantum cryptography and quantum protocols.

**Quantum Hoare type theory** [177] is inspired by classical Hoare type theory and extends the Quantum IO Monad [3] by indexing it with pre- and postconditions that serve as program specifications, which has the potential to be a unified system for programming, specifying, and reasoning about quantum programs.

**Quantum dynamic logic.** We end up this section by mentioning a line of work that is not a strict extension or application of Hoare Logic [94], but shares similar concerns and related solutions. Just as QHL and its extensions, dynamic logic formalizes the evolution of a state along the execution of a process acting over it.

Dynamic logic inherits from the modal logic apparatus where, in addition to propositional logic connectives, modalities `□` and `◇` are intruded. Intuitively, given a formula $\phi$, `□\phi` means that $\phi$ is necessarily true and `◇\phi` means that $\phi$ is possibly true. The standard semantics, based on Kripke models [115], helps catching this intuition. A Kripke model $\mathcal{K}$ is made of a set of states $S$ holding, each, a valuation $P: S \to \{\text{true, false}\}$ for a set of propositional variables $P$. And the modality is interpreted through an accessibility relation $R \subseteq S \times S$. For example, given a propositional variable $p$, `□p` (resp. `◇p`) is true in state $s$, written $\mathcal{K},s \models \Box p$ iff $p$ (resp. $\mathcal{K},s \models \Diamond p$) is true if $p$ is true in every (resp. at least one) state $s'$ such that $(s,s') \in R$.

In dynamic logic, several modalities coexist, formalizing a set of actions. Hence, given an action $a$, formula $[a]\phi$ is true iff $\phi$ is always true after performing action $a$. Actions can combine together, for example $[a;a']\phi$ means that $\phi$ is always true after the successive performance of actions $a$ and $a'$.

In their *Logic of Quantum Programs* (LQP [14, 15]), Baltag and Smets designed a quantum version of dynamic logic. Here, states correspond to one-dimensional subspaces of a Hilbert space for a quantum register. Actions are of two kinds: a *test* encodes a measurement through the set of projection transitions corresponding to the different possible outcomes (for example, given formulas $\varphi$ and $\psi$, $\varphi?\psi$ is satisfied in the state of evaluation if and only if any state satisfying $\varphi$ after measurement-any successful test for $\varphi$-also satisfies $\psi$), and proper *actions* deterministically encode unitary state transformations). In [14], the framework is illustrated by a correction proof for the teleportation and quantum secret sharing protocols. Baltag and Smets link their work to similar quantum logics as in [34].

Note that to treat measurement, LQP formalizes informations about the set of states that are possibly reachable, but the language does not hold any notion of probability. This shortcut is overcome in [13], where the authors introduce a probabilistic test modality characterizing, for any formula $\varphi$ and rational $x \in [0, 1]$, that a test for $\varphi$ has probability at least $x$ to succeed from the evaluation state.
In [13], the authors also provide a decidability proof for their setting and illustrate its expressive power by formally specifying the Grover's search algorithm and a leader election protocol. Further work in the community has used this probabilistic logic setting for the verification of the BB84 Quantum Key Distribution algorithm [24].

## 7.2 QBRICKS

QBRICKS [38] is a recently proposed circuit description language together with a deductive verification framework. It enables automated proof support for program specifications, reducing the required human effort for the development of verified programs.

QBRICKS object language (QBRICKS-DSL) consists in a minimal functional language with features for the design of circuit families. Similarly to the formal contract style of algorithm descriptions (see Section 2.2.2), QBRICKS functions are written with explicit pre-and postconditions, specifying their complexity and the parametrized input-output quantum data registers function they implement. These specifications are written in a dedicated formal language, called QBRICKS-SPEC.

To support proofs, QBRICKS is given a Hoare style derivation rules system including rules for each parametrized circuit constructor. These rules are enriched with equational theories enabling, in particular, reasoning about measurement and probabilities.

QBRICKS is a domain-specific language, embedded in the Why3 [70] deductive verification framework: programs are written in ML language and annotated with specifications in QBRICKS-DSL (pre- and postconditions, loop invariants, calls for lemmas, etc). Compiling a QBRICKS program interprets these specifications as proof obligations. Then, a dedicated interface enables to directly access these proof obligations and either send them to a set of automatic SMT-solvers (CVC4, Alt-Ergo, Z3, etc.), or enter some interactive proof transformation commands (additional calls for lemmas or hypotheses, term substitutions, etc.) or even to proof assistants (Coq, ISABELLE/HOL).

### 7.2.1 Writing Quantum Circuits Functions in QBRICKS: QBRICKS-DSL

QBRICKS-DSL makes use of a regular inductive datatype for circuits, where the data constructors are elementary gates, sequential and parallel composition, and ancilla creation. In particular, unlike in e.g. Quipper or QWIRE, a quantum circuit in QBRICKS is not a function acting on qubits: it is a simple, static object. Nonetheless, for the sake of implementing quantum circuits from the literature, this does not restrict expressiveness as they are usually precisely represented as sequences of blocks.

The core of QBRICKS-DSL is presented in Figure 13. It is a small first-order functional, call-by-value language. To the elementary gates presented in Section 2.1.5, QBRICKS adds the qubit swapping gate SWAP and the identity ID. The constructors for high-level circuit operations are sequential composition SEQ, parallel composition PAR and ancilla creation/termination ANC.

Expression `e` ::= `x` | `c` | `f(e₁,...,eₙ)` | `let ⟨x₁,...,xₙ⟩ = e in e'` | `if e₁ then e₂ else e₃` | `iter f e₁ e₂`

Data Constructor `c` ::= `n` | `tt` | `ff` | ⟨e₁,...,eₙ⟩ | `CNOT` | `SWAP` | `ID` | `H` | `Ph(e)` | `Rz(e)` | `ANC(e)` | `SEQ(e₁,e₂)` | `PAR(e₁,e₂)`

Function `f` ::= `f_d` | `f_c`

Declaration `d` ::= `let f_d(x₁,...,xₙ) = e`

<caption>Figure 13: The syntax for QBRICKS-DSL</caption>
In [13], the authors also provide a decidability proof for their setting and illustrate its expressive power by formally specifying the Grover's search algorithm and a leader election protocol. Further work in the community has used this probabilistic logic setting for the verification of the BB84 Quantum Key Distribution algorithm [24].

## 7.2 QBRICKS

QBRICKS [38] is a recently proposed circuit description language together with a deductive verification framework. It enables automated proof support for program specifications, reducing the required human effort for the development of verified programs.

QBRICKS object language (QBRICKS-DSL) consists in a minimal functional language with features for the design of circuit families. Similarly to the formal contract style of algorithm descriptions (see Section 2.2.2), QBRICKS functions are written with explicit pre-and postconditions, specifying their complexity and the parametrized input-output quantum data registers function they implement. These specifications are written in a dedicated formal language, called QBRICKS-SPEC.

To support proofs, QBRICKS is given a Hoare style derivation rules system including rules for each parametrized circuit constructor. These rules are enriched with equational theories enabling, in particular, reasoning about measurement and probabilities.

QBRICKS is a domain-specific language, embedded in the Why3 [70] deductive verification framework: programs are written in ML language and annotated with specifications in QBRICKS-DSL (pre- and postconditions, loop invariants, calls for lemmas, etc). Compiling a QBRICKS program interprets these specifications as proof obligations. Then, a dedicated interface enables to directly access these proof obligations and either send them to a set of automatic SMT-solvers (CVC4, Alt-Ergo, Z3, etc.), or enter some interactive proof transformation commands (additional calls for lemmas or hypotheses, term substitutions, etc.) or even to proof assistants (Coq, ISABELLE/HOL).

### 7.2.1 Writing Quantum Circuits Functions in QBRICKS: QBRICKS-DSL

QBRICKS-DSL makes use of a regular inductive datatype for circuits, where the data constructors are elementary gates, sequential and parallel composition, and ancilla creation. In particular, unlike in e.g. Quipper or QWIRE, a quantum circuit in QBRICKS is not a function acting on qubits: it is a simple, static object. Nonetheless, for the sake of implementing quantum circuits from the literature, this does not restrict expressiveness as they are usually precisely represented as sequences of blocks.

The core of QBRICKS-DSL is presented in Figure 13. It is a small first-order functional, call-by-value language. To the elementary gates presented in Section 2.1.5, QBRICKS adds the qubit swapping gate SWAP and the identity ID. The constructors for high-level circuit operations are sequential composition SEQ, parallel composition PAR and ancilla creation/termination ANC.

<figure><img src="image_19.png" /><figcaption>Figure 13: The syntax for QBRICKS-DSL</figcaption></figure>
The term constructs are limited to function calls, let-style composition, test with the ternary construct `if-then-else` and simple iteration: `iter f na` stands for $f(f(...f(a)...))$, a succession of `n` calls to `f`.

Even though the language does not feature measurement, it is nonetheless possible to reason on probabilistic outputs of circuits, if we were to measure its output. This is expressed in a regular theory of real and complex numbers in the specification language (see Section 7.2.4 below for details).

## 7.2.2 Parametrized Path-Sums

To interpret circuit description functions, QBRICKS uses parametrized path-sums (pps), that is an extension of path-sums [5] (Section 5.2).

In QBRICKS setting, a path-sum $P$ is an object from an opaque type with four parameters, presented in Table 3 with their types and identifier shortcuts: two integer constants `pps_width(P)` (the width of the target circuit) and `pps_range(P)` (the range, meaning that the output sum of kets has a term for each bit vector $\vec{y}$ of length `pps_range(P)`—written $\vec{y} \in BV_{p \cdot r(P)}$) and two functions `pps_angle(P)` and `pps_ket(P)`: for any input bit vector $\vec{x}$ of length `pps_width(p)` (standing for a basis ket input to the target circuit) and for any index bit vector $\vec{y}$ of length `pps_range(p)`, functions `pps_angle(P)` and `pps_ket(P)` respectively define a real scalar and a bit vector of length `pps_width(p)` (standing for a basis ket output to the target circuit)$^{11}$.

<table><caption>Table 3: Pps accessors and types</caption><thead><tr><th>Identifier</th><th>Type</th><th>Id-abbreviation</th></tr></thead><tbody><tr><td>pps_width</td><td>int</td><td>p_w</td></tr><tr><td>pps_range</td><td>int</td><td>p_r</td></tr><tr><td>pps_angle</td><td>bit_vector → bit_vector → real</td><td>p_a</td></tr><tr><td>pps_ket</td><td>bit_vector → bit_vector → bit_vector</td><td>p_k</td></tr></tbody></table>

Then for any bit vector $\vec{x}$ of size $p \cdot w(P)$, the expression

$$Ps(h, |\vec{x}\rangle) = \frac{1}{\sqrt{2p \cdot r(P)}} \sum_{\vec{y} \in BV_{p \cdot r(P)}} e^{2 \cdot \pi i \cdot p \cdot a(P)(\vec{x}, \vec{y})} |p \cdot k(P)(\vec{x}, \vec{y})\rangle_{p \cdot w(P)} \quad (6)$$

combines these different element together to define a linear application for quantum state vectors. Function $Ps$ is extended by linearity to any ket $|u\rangle$ of length $p \cdot w(p)^{12}$.

A path-sum $P$ is said to correctly interpret a given circuit $C$ (written $(C \triangleright P)$) if and only if $C$ has width $n = \text{pps\_width}(P)$ and for any bit vector $\vec{x}$ of length $n$, $\text{Mat}(C) \cdot |\vec{x}\rangle = Ps(P, |\vec{x}\rangle)$. The relation ($\neg \triangleright$) enjoys nice composition properties along QBRICKS-DSL circuit constructors (see [38]).

QBRICKS-SPEC generalizes path-sums by introducing Parametrized path-sums (pps). A pps is a function that inputs a set of parameters and outputs a path-sum. Then, it can be seen as a family of path-sums (one for each possible value of its parameters) describing the effects of the different members in a family of quantum circuits. Hence, it is well-fitted for the specification of parametrized algorithms such as Shor order finding (Shor-OF see Figure 4).

<footnote n="11">¹¹In the rest of this section, type `bit_vector` corresponds to bit vectors $\vec{x}$. They are encoded in an abstract type that provides a positive integer `length(\vec{x})` (the length of the vector) and a value function `get_bv(\vec{x})`: `int → int`. For any integer $i$, we commonly abbreviate `get_bv(\vec{x})i` as $\vec{x}_i$; if $i \in [0, length(\vec{x})]$ (that is, if $i$ is actually in the range of the bit vector) then it is such that $0 \le \vec{x}_i < 2$.</footnote>

<footnote n="12">¹²That is, to any linear combination of basis kets $|\vec{x}\rangle$ of length $p \cdot w(p)$.</footnote>
The term constructs are limited to function calls, let-style composition, test with the ternary construct `if-then-else` and simple iteration: `iter f na` stands for $f(f(...f(a)...))$, a succession of `n` calls to `f`.

Even though the language does not feature measurement, it is nonetheless possible to reason on probabilistic outputs of circuits, if we were to measure its output. This is expressed in a regular theory of real and complex numbers in the specification language (see Section 7.2.4 below for details).

### 7.2.2 Parametrized Path-Sums

To interpret circuit description functions, QBRICKS uses parametrized path-sums (pps), that is an extension of path-sums [5] (Section 5.2).

In QBRICKS setting, a path-sum $P$ is an object from an opaque type with four parameters, presented in Table 3 with their types and identifier shortcuts: two integer constants `pps_width(P)` (the width of the target circuit) and `pps_range(P)` (the range, meaning that the output sum of kets has a term for each bit vector $\vec{y}$ of length `pps_range(P)`—written $\vec{y} \in BV_{p \cdot r(P)}$) and two functions `pps_angle(P)` and `pps_ket(P)`: for any input bit vector $\vec{x}$ of length `pps_width(p)` (standing for a basis ket input to the target circuit) and for any index bit vector $\vec{y}$ of length `pps_range(p)`, functions `pps_angle(P)` and `pps_ket(P)` respectively define a real scalar and a bit vector of length `pps_width(p)` (standing for a basis ket output to the target circuit)$^{11}$.

<table><caption>Table 3: Pps accessors and types</caption><thead><tr><th>Identifier</th><th>Type</th><th>Id-abbreviation</th></tr></thead><tbody><tr><td>pps_width</td><td>int</td><td>p_w</td></tr><tr><td>pps_range</td><td>int</td><td>p_r</td></tr><tr><td>pps_angle</td><td>bit_vector → bit_vector → real</td><td>p_a</td></tr><tr><td>pps_ket</td><td>bit_vector → bit_vector → bit_vector</td><td>p_k</td></tr></tbody></table>

Then for any bit vector $\vec{x}$ of size $p \cdot w(P)$, the expression

$$Ps(h, |\vec{x}\rangle) = \frac{1}{\sqrt{2p \cdot r(P)}} \sum_{\vec{y} \in BV_{p \cdot r(P)}} e^{2 \cdot \pi i \cdot p \cdot a(P)(\vec{x}, \vec{y})} |p \cdot k(P)(\vec{x}, \vec{y})\rangle_{p \cdot w(P)} \quad (6)$$

combines these different element together to define a linear application for quantum state vectors. Function $Ps$ is extended by linearity to any ket $|u\rangle$ of length $p \cdot w(P)^{12}$.

A path-sum $P$ is said to correctly interpret a given circuit $C$ (written $(C \triangleright P)$) if and only if $C$ has width $n = \text{pps\_width}(P)$ and for any bit vector $\vec{x}$ of length $n$, $\text{Mat}(C) \cdot |\vec{x}\rangle = Ps(P, |\vec{x}\rangle)$. The relation ($\_\triangleright\_$) enjoys nice composition properties along QBRICKS-DSL circuit constructors (see [38]).

QBRICKS-SPEC generalizes path-sums by introducing Parametrized path-sums (pps). A pps is a function that inputs a set of parameters and outputs a path-sum. Then, it can be seen as a family of path-sums (one for each possible value of its parameters) describing the effects of the different members in a family of quantum circuits. Hence, it is well-fitted for the specification of parametrized algorithms such as Shor order finding (Shor-OF see Figure 4).

<footnote n="11">¹¹In the rest of this section, type `bit_vector` corresponds to bit vectors $\vec{x}$. They are encoded in an abstract type that provides a positive integer `length(\vec{x})` (the length of the vector) and a value function `get_bv(\vec{x})`: `int → int`. For any integer $i$, we commonly abbreviate `get_bv(\vec{x})i` as $\vec{x}_i$; if $i \in \llbracket 0, length(\vec{x}) \rrbracket$ (that is, if $i$ is actually in the range of the bit vector) then it is such that $0 \le \vec{x}_i < 2$.</footnote>

<footnote n="12">¹²That is, to any linear combination of basis kets $|\vec{x}\rangle$ of length $p \cdot w(P)$.</footnote>
The main strength of pps semantics, with regards to formal verification, is that each of the path-sum parametrized accessors (see Table 3) combines compositionally along with circuit constructors.

Hence, it enables reasoning about parametrized quantum circuits and their semantics without manipulating sum terms or other higher-order objects. Thanks to this tool, the automatic generation of proof obligations for QBRICKS specifications results in only first-order formulas, enabling a high level of automation when sent to SMT-solvers.

### 7.2.3 From Quantum Circuits to Path-Sums

The specification language for QBRICKS is a first-order predicate language, equipped with various equational theories. For any quantum circuit family C, QBRICKS-DSL enables to identify a pps `circ_to_pps(C)`. Each of its parametrized accessors is defined inductively upon the structure of C and it is proved that `(C ▷ circ_to_pps(C))`, for any instance of circuit. These accessors are listed and given abbreviations in Table 4.

<table><caption>Table 4: Function `circ_to_pps` and accessors</caption><thead><tr><td>Accessor</td><td>Abbreviation</td></tr></thead><tbody><tr><td>pps_width(circ_to_pps(C))</td><td>C_width(C)</td></tr><tr><td>pps_range(circ_to_pps(C))</td><td>C_range(C)</td></tr><tr><td>pps_angle(circ_to_pps(C))</td><td>C_angle(C, -, -)</td></tr><tr><td>pps_ket(circ_to_pps(C))</td><td>C_ket(C, -, -)</td></tr></tbody></table>

### 7.2.4 Probabilistic Reasoning

QBRICKS-DSL does not contain any constructor for the measurement of quantum registers. Nevertheless, QBRICKS-SPEC provides reasoning tools about it. In particular, function

$$ \text{proba\_measure: } \text{circ} \times \text{ket} \times \text{int} \rightarrow \text{real} $$

inputs a circuit C, a quantum data register $|v\rangle_n$ and an index $j \in [0, 2^n]$. It outputs the probability, for one measuring the quantum register resulting from applying circuit C to $|v\rangle$, to get the bit vector representing integer j as a result. Function `proba\_measure` is defined, for any input ket $|u\rangle$ of length `pps\_width(C)`, by application of the Born rule (see Section 2.1.2), as

$$ \text{proba\_measure}(C, |i\rangle_n, j) = |(\text{Ps}(\text{circ\_to\_pps}, |i\rangle_n)(j)|^2. $$

QBRICKS-SPEC also provides similar reasoning ghost functions for discussing the effect of partial measurement over quantum sub-registers.

### 7.2.5 Verified Properties

The QBRICKS framework aims at providing tools for writing and verifying the standard format of quantum algorithm specifications as they appear in algorithms (see, e.g., Figure 4): to perform a given computation task with a given amount of resources. Hence, as illustrated above, QBRICKS-SPEC is designed for the formalization of both:

* parametrized input/output relations for families of circuits. For a family of circuits, they typically consist in characterizing their parametrized output ket vector. Thanks to function
The main strength of pps semantics, with regards to formal verification, is that each of the path-sum parametrized accessors (see Table 3) combines compositionally along with circuit constructors.

Hence, it enables reasoning about parametrized quantum circuits and their semantics without manipulating sum terms or other higher-order objects. Thanks to this tool, the automatic generation of proof obligations for QBRICKS specifications results in only first-order formulas, enabling a high level of automation when sent to SMT-solvers.

### 7.2.3 From Quantum Circuits to Path-Sums

The specification language for QBRICKS is a first-order predicate language, equipped with various equational theories. For any quantum circuit family C, QBRICKS-DSL enables to identify a pps `circ_to_pps(C)`. Each of its parametrized accessors is defined inductively upon the structure of C and it is proved that `(C ▷ circ_to_pps(C))`, for any instance of circuit. These accessors are listed and given abbreviations in Table 4.

<table><caption>Table 4: Function `circ_to_pps` and accessors</caption><thead><tr><td>Accessor</td><td>Abbreviation</td></tr></thead><tbody><tr><td>pps_width(circ_to_pps(C))</td><td>C_width(C)</td></tr><tr><td>pps_range(circ_to_pps(C))</td><td>C_range(C)</td></tr><tr><td>pps_angle(circ_to_pps(C))</td><td>C_angle(C, -, -)</td></tr><tr><td>pps_ket(circ_to_pps(C))</td><td>C_ket(C, -, -)</td></tr></tbody></table>

### 7.2.4 Probabilistic Reasoning

QBRICKS-DSL does not contain any constructor for the measurement of quantum registers. Nevertheless, QBRICKS-SPEC provides reasoning tools about it. In particular, function

$$ \text{proba\_measure: circ} \times \text{ket} \times \text{int} \rightarrow \text{real} $$

inputs a circuit C, a quantum data register $|v\rangle_n$ and an index $j \in [0, 2^n]$. It outputs the probability, for one measuring the quantum register resulting from applying circuit C to $|v\rangle$, to get the bit vector representing integer j as a result. Function `proba\_measure` is defined, for any input ket $|u\rangle$ of length `pps\_width(C)`, by application of the Born rule (see Section 2.1.2), as

$$ \text{proba\_measure}(C, |i\rangle_n, j) = |(\text{Ps}(\text{circ\_to\_pps}, |i\rangle_n)(j)|^2. $$

QBRICKS-SPEC also provides similar reasoning ghost functions for discussing the effect of partial measurement over quantum sub-registers.

### 7.2.5 Verified Properties

The QBRICKS framework aims at providing tools for writing and verifying the standard format of quantum algorithm specifications as they appear in algorithms (see, e.g., Figure 4): to perform a given computation task with a given amount of resources. Hence, as illustrated above, QBRICKS-SPEC is designed for the formalization of both:

* parametrized input/output relations for families of circuits. For a family of circuits, they typically consist in characterizing their parametrized output ket vector. Thanks to function
proba\_measure, QBRICKS enables to identify the probability to get a given result after measurement and derivated probability reasoning (such as bounding the parametrized probability of success of a computation, wrt a pre-defined success condition). Proof support for these specifications is processed through the pps formalism,

* complexity specifications: QBRICKS enables to specify the parametrized width, number of required ancilla qubits and number of elementary gates of a circuit family.

**Example 7.3** (Pps specifications for the Bell generating circuit). For example, a specification for the Bell generating circuit can be written using accessors of pps circ\_to\_pps (Bell-circuit), as below

$$
\Gamma, \vec{x}, \vec{y} : \text{bit\_vector}, j : \text{int} \vdash \\
\quad \left\{
\begin{array}{l}
bv\_length(\vec{x}) = 2 \quad \wedge \quad bv\_length(\vec{y}) = 1 \quad \wedge \quad j \in \llbracket 0, 2 \rrbracket \\
\text{Bell-circuit} \\
\\
\quad \left\{
\begin{array}{l}
C\_width(result) = 2 \quad \wedge \quad C\_ket(result, \vec{x}, \vec{y}) = \overrightarrow{x(0) \cdot (1-x(1))} \quad \wedge \\
C\_range(result) = 1 \quad \wedge \quad C\_angle(result, \vec{x}, \vec{y}) = x(0) * y(0) \quad \wedge \\
\phantom{C\_range(result) = 1 \quad \wedge \quad} width(result) = 2 \quad \wedge \quad size(result) = 2 \quad \wedge \quad ancillas(result) = 0
\end{array}
\right\}
\end{array}
\right.
$$

This Hoare style notation, `{Pre}`p`{Post}` states that whenever Pre is satisfied, then running p ensures that Post is satisfied. Formula Post uses result as a variable standing for program p. The specification uses free-ghost-bit vectors variables x and y and integer variable j. It requires x and y to have respective lengths 2 and 1 and j to be in `[0, 2]`. Given these preconditions, the specifications ensures that the angle C\_angle outputs x̄₀ * ȳ₀ for inputs x and y and the ket function C\_ket outputs x̄₀ · (1 - x̄₁) for inputs x, y and j. Then, one easily verifies that, applying equation 6 on each bit-vector a · b of length 2 results in the corresponding output |β<sub>ab</sub>⟩, formally:

$$
\mathbf{Ps}(\text{circ\_to\_pps}(\text{Bell-circuit}), |ab\rangle) = \mathbf{Mat}(\text{Bell-circuit}) \cdot |ab\rangle
$$

So the postcondition, by use of C\_width, C\_range, C\_angle and C\_ket, enables a complete char-
acterization of the input/output function performed by the Bell circuit. In addition, the specification
brings some complexity related postcondition: the circuit has width 2 and size 2 (i.e., length of the
required quantum register and number of performed elementary operations), and does not use any
additional ancilla qubit.

**7.2.6 Deduction and Proof Support**

Proof support in QBRICKS strongly relies on the compositional structure of quantum circuits, en-
abling compositional reasoning on both pps and complexity features. As an example, in Figure 14
we give some of the rules used for the characterization of circuits size. Gates ID and SWAP are con-
sidered as free, so they count for null. The other elementary gates have size 1, both sequence and
parallel compositions sum the size of their components and ancilla creation/termination does not
affect circuit size.

Similar deduction rules are defined for circuit width, number of ancilla qubits and pps accessors.
We do not introduce them here for sake of concision but we refer the desirous reader to [38].

**7.2.7 Implementation and Case Studies**

QBRICKS enabled to implement, specify and formalize parametrized versions for Quantum Fourier
Transform, Grover search algorithm, QPE, Shor order finding, etc. The main specificity of these
QBRICKS implementations is to hold a high level of proof support automation. This is largely due
to the reduction of proof obligations to first-order logic predicates by use of pps characterizations.
proba\_measure, QBRICKS enables to identify the probability to get a given result after measurement and derivated probability reasoning (such as bounding the parametrized probability of success of a computation, wrt a pre-defined success condition). Proof support for these specifications is processed through the pps formalism,

* complexity specifications: QBRICKS enables to specify the parametrized width, number of required ancilla qubits and number of elementary gates of a circuit family.

**Example 7.3** (Pps specifications for the Bell generating circuit). For example, a specification for the Bell generating circuit can be written using accessors of pps circ\_to\_pps (Bell-circuit), as below

$$ \Gamma, \vec{x}, \vec{y} : \text{bit\_vector}, j : \text{int} \vdash \\ \quad \left\{ \begin{array}{l} \text{bv\_length}(\vec{x}) = 2 \quad \wedge \quad \text{bv\_length}(\vec{y}) = 1 \quad \wedge \quad j \in \llbracket 0, 2 \rrbracket \\ \text{Bell-circuit} \\ \quad \left\{ \begin{array}{l} \text{C\_width}(\text{result}) = 2 \quad \wedge \quad \text{C\_ket}(\text{result}, \vec{x}, \vec{y}) = \overrightarrow{x(0) \cdot (1-x(1))} \quad \wedge \\ \text{C\_range}(\text{result}) = 1 \quad \wedge \quad \text{C\_angle}(\text{result}, \vec{x}, \vec{y}) = x(0) * y(0) \quad \wedge \\ \text{width}(\text{result}) = 2 \quad \wedge \quad \text{size}(\text{result}) = 2 \quad \wedge \quad \text{ancillas}(\text{result}) = 0 \end{array} \right\} \end{array} \right. $$

This Hoare style notation, {$Pre$}p{$Post$} states that whenever Pre is satisfied, then running p ensures that Post is satisfied. Formula Post uses result as a variable standing for program p. The specification uses free-ghost-bit vectors variables $\vec{x}$ and $\vec{y}$ and integer variable j. It requires $\vec{x}$ and $\vec{y}$ to have respective lengths 2 and 1 and j to be in $\llbracket 0, 2 \rrbracket$. Given these preconditions, the specifications ensures that the angle C\_angle outputs $\vec{x}_0 * \vec{y}_0$ for inputs $\vec{x}$ and $\vec{y}$ and the ket function C\_ket outputs $\vec{x}_0 \cdot (1 - \vec{x}_1)$ for inputs $\vec{x}, \vec{y}$ and j. Then, one easily verifies that, applying equation 6 on each bit-vector $a \cdot b$ of length 2 results in the corresponding output $|\beta_{ab}\rangle$, formally:

$$ \mathit{Ps}(\mathit{circ\_to\_pps}(\mathit{Bell-circuit}), |ab\rangle) = \mathbf{Mat}(\mathit{Bell-circuit}) \cdot |ab\rangle $$

So the postcondition, by use of C\_width, C\_range, C\_angle and C\_ket, enables a complete characterization of the input/output function performed by the Bell circuit. In addition, the specification brings some complexity related postcondition: the circuit has width 2 and size 2 (i.e., length of the required quantum register and number of performed elementary operations), and does not use any additional ancilla qubit.

### 7.2.6 Deduction and Proof Support

Proof support in QBRICKS strongly relies on the compositional structure of quantum circuits, enabling compositional reasoning on both pps and complexity features. As an example, in Figure 14 we give some of the rules used for the characterization of circuits size. Gates ID and SWAP are considered as free, so they count for null. The other elementary gates have size 1, both sequence and parallel compositions sum the size of their components and ancilla creation/termination does not affect circuit size.

Similar deduction rules are defined for circuit width, number of ancilla qubits and pps accessors. We do not introduce them here for sake of concision but we refer the desirous reader to [38].

### 7.2.7 Implementation and Case Studies

QBRICKS enabled to implement, specify and formalize parametrized versions for Quantum Fourier Transform, Grover search algorithm, QPE, Shor order finding, etc. The main specificity of these QBRICKS implementations is to hold a high level of proof support automation. This is largely due to the reduction of proof obligations to first-order logic predicates by use of pps characterizations.
$$ 
\begin{array}{l}
\frac{C \in \{\text{ID,SWAP}\}}{\text{width}(C) = 0} \text{ (Id-SWAP-size)} \qquad \frac{C \in \{\text{H,Ph}(n), \text{R}_z(n)\}}{\text{size}(C) = 1} \text{ (H-Ph-R}_z\text{-size)} \\[2ex]
\frac{\Gamma \vdash \text{size}(C_1) = n_1 \quad \Gamma \vdash \text{size}(C_2) = n_2 \quad \Gamma \vdash \text{width}(C_1) = \text{width}(C_2)}{\Gamma \vdash \text{size}(\text{SEQ}(C_1, C_2)) = n_1 + n_2} \text{ (seq-size)} \\[2ex]
\frac{\Gamma \vdash \text{size}(C_1) = n_1 \quad \Gamma \vdash \text{size}(C_2) = n_2}{\Gamma \vdash \text{size}(\text{PAR}(C_1, C_2)) = n_1 + n_2} \text{ (par-size)} \\[2ex]
\frac{\Gamma \vdash \text{size}(C) = n}{\Gamma \vdash \text{size}(\text{ANC}(C)) = n} \text{ (anc-size)}
\end{array}
$$

<caption>Figure 14: Deduction rules for QBRICKS: size (number of gates)</caption>

## 7.3 SQIR

The SQIR language [91, 90] is the representation language used by the VOQC optimizer (see Section 5.4). On its own, it also constitutes a solution for formally proved correct quantum programs. It is developed concurrently with QBRICKS and holds similar concerns: basically, to reduce the expressivity of programming languages such as Quipper and QWIRE so as to (1) still enable the whole implementation of emblematic algorithms (2) enable formal proof of specifications.

The development of SQIR followed that of QWIRE (see Section 6.1.3) when the authors observed the difficulty to hold formal verification, mainly linked to the management of memory wires. Hence SQIR and QWIRE have overlapping author and developer ship, they are both deeply embedded in the Coq proof assistant and they share the same mathematical libraries for, e.g., matrices and complex numbers. Schematically, compared to QWIRE, SQIR has a reduced expressivity (disabling, eg., the identification of qubit held values), making tractable the formal verification of functional program properties.

### 7.3.1 Programming Language

Just as QBRICKS, the programming part of SQIR is reduced to the minimum enabling implementation of main quantum programming features. It is two-layered: the *unitary part* corresponds to the design of unitary circuits and a generalized circuit layer adds branching measurement and ket initialization.

In SQIR, quantum circuits have type $N \rightarrow \text{Set}$, with a positive integer parameter corresponding to their width. Quantum memory wires are identified by integer indexes, bounded by a global register size parameter $d$. Then, the type for unitary operators in SQIR (ucom) features the application of a circuit to a quantum register with $d$ wires. It is defined inductively as follows.

Inductive ucom (U: $N \rightarrow \text{Set}$) (d: $N$) : Set :=
useq : ucom U d \rightarrow ucom U d \rightarrow ucom U d
uapp1 : U 1 \rightarrow N \rightarrow ucom U d
uapp2 : U 2 \rightarrow N \rightarrow N \rightarrow ucom U d
uapp3 : U 3 \rightarrow N \rightarrow N \rightarrow N \rightarrow ucom U d
$$ 
\begin{array}{l@{\qquad}l}
\frac{C \in \{\text{ID,SWAP}\}}{\text{width}(C) = 0} \text{ (Id-SWAP-size)} & \frac{C \in \{\text{H,Ph}(n), \text{R}_z(n)\}}{\text{size}(C) = 1} \text{ (H-Ph-R}_z\text{-size)} \\[2ex]
\frac{\Gamma \vdash \text{size}(C_1) = n_1 \quad \Gamma \vdash \text{size}(C_2) = n_2 \quad \Gamma \vdash \text{width}(C_1) = \text{width}(C_2)}{\Gamma \vdash \text{size}(\text{SEQ}(C_1, C_2)) = n_1 + n_2} \text{ (seq-size)} & \\[2ex]
\frac{\Gamma \vdash \text{size}(C_1) = n_1 \quad \Gamma \vdash \text{size}(C_2) = n_2}{\Gamma \vdash \text{size}(\text{PAR}(C_1, C_2)) = n_1 + n_2} \text{ (par-size)} & \\[2ex]
\frac{\Gamma \vdash \text{size}(C) = n}{\Gamma \vdash \text{size}(\text{ANC}(C)) = n} \text{ (anc-size)} &
\end{array}
$$

<caption>Figure 14: Deduction rules for QBRICKS: size (number of gates)</caption>

## 7.3 SQIR

The SQIR language [91, 90] is the representation language used by the VOQC optimizer (see Section 5.4). On its own, it also constitutes a solution for formally proved correct quantum programs. It is developed concurrently with QBRICKS and holds similar concerns: basically, to reduce the expressivity of programming languages such as Quipper and QWIRE so as to (1) still enable the whole implementation of emblematic algorithms (2) enable formal proof of specifications.

The development of SQIR followed that of QWIRE (see Section 6.1.3) when the authors observed the difficulty to hold formal verification, mainly linked to the management of memory wires. Hence SQIR and QWIRE have overlapping author and developer ship, they are both deeply embedded in the Coq proof assistant and they share the same mathematical libraries for, e.g., matrices and complex numbers. Schematically, compared to QWIRE, SQIR has a reduced expressivity (disabling, eg., the identification of qubit held values), making tractable the formal verification of functional program properties.

### 7.3.1 Programming Language

Just as QBRICKS, the programming part of SQIR is reduced to the minimum enabling implementation of main quantum programming features. It is two-layered: the *unitary part* corresponds to the design of unitary circuits and a generalized circuit layer adds branching measurement and ket initialization.

In SQIR, quantum circuits have type $N \to \text{Set}$, with a positive integer parameter corresponding to their width. Quantum memory wires are identified by integer indexes, bounded by a global register size parameter $d$. Then, the type for unitary operators in SQIR (ucom) features the application of a circuit to a quantum register with $d$ wires. It is defined inductively as follows.

Inductive ucom (U: $N \to \text{Set}$) (d: $N$) : Set :=
useq : ucom U d \to ucom U d \to ucom U d
uapp1 : U 1 \to N \to ucom U d
uapp2 : U 2 \to N \to N \to ucom U d
uapp3 : U 3 \to N \to N \to N \to ucom U d
This definition holds two kinds of operations:

* the sequential composition, `useq`, which inputs two circuits and outputs their sequential composition,

* the application of an elementary gates to (a) given wire(s), depending on the width of this gate. There are three different versions of this operations, for gates of width 1, 2 or 3, named respectively `uapp1`, `uapp2` and `uapp3`. As an example, `uapp1` inputs a gate `U` of width 1 and a parameter `i`. It outputs the result of applying `U` on wire `i` in a register of size `d`<fnref n="13" />.

Then, SQIR provides a generalized circuit building layer, enabling the sequential composition of unitary commands, their initialization and branching measurement. Again, a circuit is an object `com` of type `N → Set` applied on a register of specified size `d`. It is defined, inductively, as follows.

Inductive com (U: N → Set) (d: N) : Set :=
| uc : ucom U d → com U d → ucom U d
| skip : com U d
| meas : N → com U d → com U d → com U d
| seq : com U d → com U d → com U d

A generalized circuit is built as either the lifting `uc` of a circuit into a generalized circuit, the empty `skip` operation, the branching measurement `meas` (with inputs a wire identifier for a qubit to measure and two generalized circuits to execute, depending on the measurement result) and the sequence `seq` of two different generalized circuits.

### 7.3.2 Matrix Semantics and Specifications

The semantics for SQIR programs is based on the standard matrix apparatus. For the unitary fragment, it uses the matrix semantics presented in Section 2.1.5. It is extended for generalized circuits by density operators semantics, similarly as in Section 7.1.

In its present state of development, SQIR enables to specify functional properties, describing the input-output relation, similarly to the one for QBRICKS introduced in Section 7.2.5

### 7.3.3 Implementation and Case Studies

SQIR is implemented as an embedded DSL into the Coq proof assistant. It was illustrated with specified and proved parametrized implementations of Simon's algorithm, QPE and Grover's Search Algorithm.

### 7.3.4 Comparison Between QBRICKS and SQIR

QBRICKS and SQIR are being developed concurrently, with very similar objectives. In particular they both trade-off between offering user-friendly programming features and reducing the language expressivity to the minimal, to enable functional formal verification. The solutions they provide share many common points. We discuss their main design differences.

* SQIR elementary operations consist in applying quantum gates on given wires of a quantum register, whereas QBRICKS proceeds by assembling quantum gates together into a quantum

<footnote n="13">¹³Note that, for this construction to make sense, the parameter `i` should not be greater than `d`. This condition is encoded by the semantics of SQIR.</footnote>
This definition holds two kinds of operations:

* the sequential composition, `useq`, which inputs two circuits and outputs their sequential composition,

* the application of an elementary gates to (a) given wire(s), depending on the width of this gate. There are three different versions of this operations, for gates of width 1, 2 or 3, named respectively `uapp1`, `uapp2` and `uapp3`. As an example, `uapp1` inputs a gate `U` of width 1 and a parameter `i`. It outputs the result of applying `U` on wire `i` in a register of size `d`<fnref n="13" />.

Then, SQIR provides a generalized circuit building layer, enabling the sequential composition of unitary commands, their initialization and branching measurement. Again, a circuit is an object `com` of type `N → Set` applied on a register of specified size `d`. It is defined, inductively, as follows.

Inductive com (U: N → Set) (d: N) : Set :=
| uc : ucom U d → com U d → ucom U d
| skip : com U d
| meas : N → com U d → com U d → com U d
| seq : com U d → com U d → com U d

A generalized circuit is built as either the lifting `uc` of a circuit into a generalized circuit, the empty `skip` operation, the branching measurement `meas` (with inputs a wire identifier for a qubit to measure and two generalized circuits to execute, depending on the measurement result) and the sequence `seq` of two different generalized circuits.

### 7.3.2 Matrix Semantics and Specifications

The semantics for SQIR programs is based on the standard matrix apparatus. For the unitary fragment, it uses the matrix semantics presented in Section 2.1.5. It is extended for generalized circuits by density operators semantics, similarly as in Section 7.1.

In its present state of development, SQIR enables to specify functional properties, describing the input-output relation, similarly to the one for QBRICKS introduced in Section 7.2.5

### 7.3.3 Implementation and Case Studies

SQIR is implemented as an embedded DSL into the Coq proof assistant. It was illustrated with specified and proved parametrized implementations of Simon's algorithm, QPE and Grover's Search Algorithm.

### 7.3.4 Comparison Between QBRICKS and SQIR

QBRICKS and SQIR are being developed concurrently, with very similar objectives. In particular they both trade-off between offering user-friendly programming features and reducing the language expressivity to the minimal, to enable functional formal verification. The solutions they provide share many common points. We discuss their main design differences.

* SQIR elementary operations consist in applying quantum gates on given wires of a quantum register, whereas QBRICKS proceeds by assembling quantum gates together into a quantum

<footnote n="13">¹³Note that, for this construction to make sense, the parameter `i` should not be greater than `d`. This condition is encoded by the semantics of SQIR.</footnote>
circuit, just as bricks of a wall. Both views are inter-simulable: QBRICKS provides a macro place with integer parameters specifying the wire identifier a given sub-circuit should be applied to and the size of the overall circuit (corresponding to the size of the available quantum register). This macro is built by the parallel combination of its sub-circuit arguments with the appropriate number of occurrences of ID gate. It is of similar use as SQIR function uapp. On the other hand, QBRICKS gates assemblage is trivially simulable through SQIR uapp;

* On the other hand, SQIR provides a generalized circuit building layer, including measurement and classical control. Nevertheless, this upper layer is formalized through density operators, which are cumbersome objects for formal reasoning. So far, this part of the language only received illustrations with toy examples, such as superdense coding or quantum teleportation. In more involved implementations (such as QPE or Grover), SQIR authors followed a specification and proof strategy similar to that of QBRICKS: by reasoning on the quantum data outputs of circuits, specifying over the probability distribution of result if a measurement were performed. Hence, designing a generalized circuit building language semantics probed against actual implementations of real usage algorithms is still an open challenge;

* As introduced in Section 4.2.2, complexity properties of circuits constitute a fundamental aspect of quantum certification, decisive with regards to both the physical reliability of a computation and the quantum advantage it may provide. In the present state of development, SQIR does not offer a solution for this type of specifications. Still, this could be merely implemented in SQIR as additional functionality.

## 7.4 Conclusion about Formal Verification of Quantum Programs

In Table 5 we sum up the main concrete case study realizations of formally verified quantum algorithms: instances of Grover algorithm from QBRICKS, SQIR and QHL, Deutsch-Jozsa and QPE instances from QBRICKS and SQIR, and Shor-OF implementation from QBRICKS. For each of these implementations, we give the length of the code (column LoC) and a measure of the human proof effort required for the specification proofs. It was obtained by adding the length of the program specifications (Spec stands for the number of lines of specifications and intermediary lemmas) and the number of proof commands that were required to prove these specifications (column Cmd).

<table><caption>Table 5: Compared implementations of formally verified quantum algorithms</caption><thead><tr><th rowspan="2"></th><th colspan="2">QBRICKS[38]</th><th colspan="2">SQIR [90, 91]</th><th colspan="2">QHL[131]</th></tr><tr><th>LoC</th><th>Spec+Cmd</th><th>LoC</th><th>Spec+Cmd</th><th>LoC</th><th>Spec+Cmd</th></tr></thead><tbody><tr><td>DJ</td><td>11</td><td>85</td><td>10</td><td>261</td><td></td><td></td></tr><tr><td>Grover</td><td>39</td><td>279</td><td>15</td><td>926</td><td>90</td><td>2975</td></tr><tr><td>QPE</td><td>23</td><td>246</td><td>40</td><td>812</td><td></td><td></td></tr><tr><td>Shor-OF</td><td>132</td><td>1212</td><td></td><td></td><td></td><td></td></tr></tbody></table>

To the best of our knowledge Table 5 is comprehensive regarding parametrized formally proved quantum algorithm<fnref n="14" />. Let us stress out how young the field is (in complement to the reduced

<footnote n="14">¹⁴ An additional formalization of Deutsch Jozsa algorithm is presented by Bordg et al. [30]. We do not include it in Table 5 since it is not generated by a programming language but directly led as an algebraic proof. The total length of the proof is over 1 700 lines. Additionally, the online SQIR repository contains a Shor algorithm folder, but to the best of our knowledge, it was never explicitly presented nor described. It seems, by the way, hardly comparable with the QBRICKS implementation since it focuses on different aspects by bringing additional classical post-processing functions but lacking the oracle implementation.</footnote>
circuit, just as bricks of a wall. Both views are inter-simulable: QBRICKS provides a macro place with integer parameters specifying the wire identifier a given sub-circuit should be applied to and the size of the overall circuit (corresponding to the size of the available quantum register). This macro is built by the parallel combination of its sub-circuit arguments with the appropriate number of occurrences of ID gate. It is of similar use as SQIR function uapp. On the other hand, QBRICKS gates assemblage is trivially simulable through SQIR uapp;

* On the other hand, SQIR provides a generalized circuit building layer, including measurement and classical control. Nevertheless, this upper layer is formalized through density operators, which are cumbersome objects for formal reasoning. So far, this part of the language only received illustrations with toy examples, such as superdense coding or quantum teleportation. In more involved implementations (such as QPE or Grover), SQIR authors followed a specification and proof strategy similar to that of QBRICKS: by reasoning on the quantum data outputs of circuits, specifying over the probability distribution of result if a measurement were performed. Hence, designing a generalized circuit building language semantics probed against actual implementations of real usage algorithms is still an open challenge;

* As introduced in Section 4.2.2, complexity properties of circuits constitute a fundamental aspect of quantum certification, decisive with regards to both the physical reliability of a computation and the quantum advantage it may provide. In the present state of development, SQIR does not offer a solution for this type of specifications. Still, this could be merely implemented in SQIR as additional functionality.

## 7.4 Conclusion about Formal Verification of Quantum Programs

In Table 5 we sum up the main concrete case study realizations of formally verified quantum algorithms: instances of Grover algorithm from QBRICKS, SQIR and QHL, Deutsch-Jozsa and QPE instances from QBRICKS and SQIR, and Shor-OF implementation from QBRICKS. For each of these implementations, we give the length of the code (column LoC) and a measure of the human proof effort required for the specification proofs. It was obtained by adding the length of the program specifications (Spec stands for the number of lines of specifications and intermediary lemmas) and the number of proof commands that were required to prove these specifications (column Cmd).

<table><caption>Table 5: Compared implementations of formally verified quantum algorithms</caption><thead><tr><th rowspan="2"></th><th colspan="2">QBRICKS[38]</th><th colspan="2">SQIR [90, 91]</th><th colspan="2">QHL[131]</th></tr><tr><th>LoC</th><th>Spec+Cmd</th><th>LoC</th><th>Spec+Cmd</th><th>LoC</th><th>Spec+Cmd</th></tr></thead><tbody><tr><td>DJ</td><td>11</td><td>85</td><td>10</td><td>261</td><td></td><td></td></tr><tr><td>Grover</td><td>39</td><td>279</td><td>15</td><td>926</td><td>90</td><td>2975</td></tr><tr><td>QPE</td><td>23</td><td>246</td><td>40</td><td>812</td><td></td><td></td></tr><tr><td>Shor-OF</td><td>132</td><td>1212</td><td></td><td></td><td></td><td></td></tr></tbody></table>

To the best of our knowledge Table 5 is comprehensive regarding parametrized formally proved quantum algorithm<fnref n="14" />. Let us stress out how young the field is (in complement to the reduced

<footnote n="14">¹⁴ An additional formalization of Deutsch Jozsa algorithm is presented by Bordg et al. [30]. We do not include it in Table 5 since it is not generated by a programming language but directly led as an algebraic proof. The total length of the proof is over 1 700 lines. Additionally, the online SQIR repository contains a Shor algorithm folder, but to the best of our knowledge, it was never explicitly presented nor described. It seems, by the way, hardly comparable with the QBRICKS implementation since it focuses on different aspects by bringing additional classical post-processing functions but lacking the oracle implementation.</footnote>
number of concrete realizations, note that none of them is dated earlier than 2019). Nevertheless, it
has already brought promising results.

One of the main challenges for formal verification is to reduce the human proof effort that is required for the certification of programs. As Table 5 shows, comparing this effort to the length of effective programs, QBRICKS offers a quite stable ratio ≈ 10. In a quite regular way, SQIR adds a ≈ 3.5 factor to this ratio and QHL, for the case of Grover algorithm, requires ≈ 10 times more human effort<fnref n="15" />

# 8 Discussion and Bibliographical Notes

We end up this survey by providing some additional references for usage of formal methods in
quantum information and quantum computing.

## 8.1 Deductive Verification

Deductive verification appears to be the most promising direction for the development of formal methods in quantum computing. In particular, it is particularly adequate for the formal verification of functional specifications, which is crucial for quantum programming and prone to play, there, a role similar to that of testing and debugging in classical computing (see Section 4.1). It is worth noting that, currently, all existing formally verified quantum algorithms descriptions [131] or implementations [38, 91] are based either on deductive verification or interactive proofs.

## 8.2 Model Checking

Attempts for functional verification of quantum algorithm with model checking techniques were also led before these developments [78, 197, 196]. They enabled to verify toy examples of quantum processes in a completely automated way. Nevertheless, this direction is limited by its high scale sensitivity, which is specifically problematic for quantum programs, since they are designed to tackle large problems instances.

## 8.3 Type Checking

Apart from functional specification, specialized type systems for quantum programming languages also facilitate programming and debugging. In Section 4.1 we introduced the verification of structural constraints and the non-duplicability of quantum information. Type checking may also have further use in quantum computing.

Recently, the SILQ language was proposed. It is based on a linear type system which, upon other features, enables to verify, for any quantum circuit, whether it can be *uncomputed*, a computation feature required at many stages of quantum implementations. Based on this type system, SILQ enables to automatically generate the uncomputation steps of circuits. This partial automation of the development lowers the expertise requirements for developers and the length of programs with regards to languages such as Q# or Quipper.

<footnote n="15">¹⁵Note that the QHL implementation of Grover algorithm concerns a restricted case, with regards to the two others figuring in Table 5. Furthermore, it does not contain the gate-to-gate circuit building but uses large circuit portions as primitives instead. Therefore, factor ≈ 10 is actually an underestimate.</footnote>
number of concrete realizations, note that none of them is dated earlier than 2019). Nevertheless, it
has already brought promising results.

One of the main challenges for formal verification is to reduce the human proof effort that is required for the certification of programs. As Table 5 shows, comparing this effort to the length of effective programs, QBRICKS offers a quite stable ratio ≈ 10. In a quite regular way, SQIR adds a ≈ 3.5 factor to this ratio and QHL, for the case of Grover algorithm, requires ≈ 10 times more human effort<fnref n="15" />

# 8 Discussion and Bibliographical Notes

We end up this survey by providing some additional references for usage of formal methods in
quantum information and quantum computing.

## 8.1 Deductive Verification

Deductive verification appears to be the most promising direction for the development of formal methods in quantum computing. In particular, it is particularly adequate for the formal verification of functional specifications, which is crucial for quantum programming and prone to play, there, a role similar to that of testing and debugging in classical computing (see Section 4.1). It is worth noting that, currently, all existing formally verified quantum algorithms descriptions [131] or implementations [38, 91] are based either on deductive verification or interactive proofs.

## 8.2 Model Checking

Attempts for functional verification of quantum algorithm with model checking techniques were also led before these developments [78, 197, 196]. They enabled to verify toy examples of quantum processes in a completely automated way. Nevertheless, this direction is limited by its high scale sensitivity, which is specifically problematic for quantum programs, since they are designed to tackle large problems instances.

## 8.3 Type Checking

Apart from functional specification, specialized type systems for quantum programming languages also facilitate programming and debugging. In Section 4.1 we introduced the verification of structural constraints and the non-duplicability of quantum information. Type checking may also have further use in quantum computing.

Recently, the SILQ language was proposed. It is based on a linear type system which, upon other features, enables to verify, for any quantum circuit, whether it can be *uncomputed*, a computation feature required at many stages of quantum implementations. Based on this type system, SILQ enables to automatically generate the uncomputation steps of circuits. This partial automation of the development lowers the expertise requirements for developers and the length of programs with regards to languages such as Q# or Quipper.

<footnote n="15">¹⁵Note that the QHL implementation of Grover algorithm concerns a restricted case, with regards to the two others figuring in Table 5. Furthermore, it does not contain the gate-to-gate circuit building but uses large circuit portions as primitives instead. Therefore, factor ≈ 10 is actually an underestimate.</footnote>
## 8.4 Runtime assertion Checking

First, recall from Section 1 that proving quantum programs is mainly meant to replace the standard classical debugging method of testing and assertion checking. Apart from the development of formal proofs as an alternative, efforts are led to adapt this classical strategy to the quantum case. There, we still decorate programs with formal specifications (called *assertions* in this context) describing the evolution of the system state through an execution. But instead of mathematical proofs, these assertions are probed by statistical testing over program fragments. The challenges faced by such methods are mainly twofold:

**Destructive measurement**: memory reading destructs the superposition of a quantum state, therefore one cannot continue the execution after checking. Hence, assertion checking can be applied only to fragments of an execution.

**Non-determinism**: what we aim to check is a superposition of states, which induces a probability distribution of outcomes when a measurement is performed. Then, checking an assertion requires a number of testing runs large enough to build up a representative statistical distribution.

To overcome these difficulties, a first strategy is to reduce the specifications so as to express only properties that may be handled by assertion checking. Huang and Martonosi propose a “runtime-monitoring like” verification method for quantum circuits [96]. The annotation language is reduced so as to specify, for a quantum register, to be either in a classical state, in a superposition or entangled, without any concern about further description of the state.

More recently, Li et al. [126] developed an assertion-checking based method for the verification of fine quantum registers states properties, including functional descriptions of circuit behaviors. This method is based on:

* an assertion language, based on QHL projections (see Section 7.1), enabling functional specifications about computations at stake;

* the use and formalization of *gentle measurements*: quantum registers are not measured in the usual computation basis, but in a basis containing an output that is very close to the expected state;

* an appropriate formalization of the notion of distance between quantum states, enabling verification in terms of confidence interval between the current state of the system and its expected value.

Hence, gentle measurement enables to test executions over full functional state specifications. In addition to bringing expressivity to the specifications, it lowers the undesired effects of destructive measurements: since a gentle measurement operator contains an eigenstate that is an approximation of the expected quantum state, in most cases the measurement effect on the system state can be considered negligible and the execution can be pursued. Furthermore, the test result probability distribution is centered on a specific value. Therefore, a much-reduced set of runs bring valuable statistical conclusions.

However, verification following this strategy only holds for a particular instance of a circuit, instead of a family of quantum circuits with unassigned parameters as in propositions from Section 7. Furthermore, in the general case, gentle measurements are implemented by applying (1) a unitary $U$ uncomputing the system state into a ket of the computational basis (2) a measurement in the computational basis (3) unitary $U^\dagger$, to recover the initial state. Then, assertion checking inputs unitaries
## 8.4 Runtime assertion Checking

First, recall from Section 1 that proving quantum programs is mainly meant to replace the standard classical debugging method of testing and assertion checking. Apart from the development of formal proofs as an alternative, efforts are led to adapt this classical strategy to the quantum case. There, we still decorate programs with formal specifications (called *assertions* in this context) describing the evolution of the system state through an execution. But instead of mathematical proofs, these assertions are probed by statistical testing over program fragments. The challenges faced by such methods are mainly twofold:

**Destructive measurement**: memory reading destructs the superposition of a quantum state, therefore one cannot continue the execution after checking. Hence, assertion checking can be applied only to fragments of an execution.

**Non-determinism**: what we aim to check is a superposition of states, which induces a probability distribution of outcomes when a measurement is performed. Then, checking an assertion requires a number of testing runs large enough to build up a representative statistical distribution.

To overcome these difficulties, a first strategy is to reduce the specifications so as to express only properties that may be handled by assertion checking. Huang and Martonosi propose a “runtime-monitoring like” verification method for quantum circuits [96]. The annotation language is reduced so as to specify, for a quantum register, to be either in a classical state, in a superposition or entangled, without any concern about further description of the state.

More recently, Li et al. [126] developed an assertion-checking based method for the verification of fine quantum registers states properties, including functional descriptions of circuit behaviors. This method is based on:

* an assertion language, based on QHL projections (see Section 7.1), enabling functional specifications about computations at stake;

* the use and formalization of *gentle measurements*: quantum registers are not measured in the usual computation basis, but in a basis containing an output that is very close to the expected state;

* an appropriate formalization of the notion of distance between quantum states, enabling verification in terms of confidence interval between the current state of the system and its expected value.

Hence, gentle measurement enables to test executions over full functional state specifications. In addition to bringing expressivity to the specifications, it lowers the undesired effects of destructive measurements: since a gentle measurement operator contains an eigenstate that is an approximation of the expected quantum state, in most cases the measurement effect on the system state can be considered negligible and the execution can be pursued. Furthermore, the test result probability distribution is centered on a specific value. Therefore, a much-reduced set of runs bring valuable statistical conclusions.

However, verification following this strategy only holds for a particular instance of a circuit, instead of a family of quantum circuits with unassigned parameters as in propositions from Section 7. Furthermore, in the general case, gentle measurements are implemented by applying (1) a unitary $U$ uncomputing the system state into a ket of the computational basis (2) a measurement in the computational basis (3) unitary $U^\dagger$, to recover the initial state. Then, assertion checking inputs unitaries
$U$ and $U^\dagger$ that are themselves prone to error. More precisely, to test against the exact expected value of the state, operator $U^\dagger$ should be equivalent to the computation under test. Practically, gentle measurements approximate the state under test. This enables a simplification of the measurement operator, at the cost of the robustness of the procedure.

## 8.5 Verification of Quantum Communication Protocols

Another challenge for formal methods is the verification of quantum information processes concerns quantum protocols.

Quantum key distribution protocols [164, 22, 128, 134] enable secured information exchanges between two parties. These protocols exploit the fact that, due to the destructive measurement, physics laws prevent almost any $^{16}$ possibility for a potential eavesdropping in the exchange of quantum information. In particular, several formally verified implementations of the BB84 quantum key distribution protocol [22] have been proposed in the literature, based either on process calculus [137, 117], formalization in Coq [28] or model checking [63, 68].

Bordg et al. [30] propose a formalization of quantum information in the ISABELLE/HOL proof assistant. They illustrate their methods through the cases of quantum teleportation and the quantum prisoner dilemma. This work also contains a formally verified implementation of the Deutsch-Jozsa algorithm in ISABELLE/HOL.

In a more fundamental prospect, Echenim et al. [61] provide an ISABELLE/HOL proof for the CHSH inequalities [45]. These are probability distributions about crossed measurement results of quantum observables. They provide a proof for the Bell theorem [21], inducing that no classical theory could account for the entanglement phenomenon (hence that quantum physics cannot be reduced to local classical theories).

# 9 Conclusion

## 9.1 Summary

Throughout this survey, we introduced the context, the main challenges and the most promising results in formally verified quantum programmatic. The current state of affairs in this emerging domain can be summed up as follows:

* Quantum computing is an emerging domain, with huge potential application fields and promises. Progresses in the development of concrete machines are reaching the practical relevance landmark: prototypes are getting powerful enough to overpass classical computers. Consequently, quantum software development is becoming a crucial industrial short-term need;

* Quantum software deals with an entirely new programming paradigm. Upon its main particularities are the dual nature of information (either classical or quantum), the destructive measurement and irreducibly probabilistic computations;

* These specificities make programming particularly non-intuitive and prone to error. Furthermore, they make it very hard to directly import usual debugging methods from the classical

<footnote>$^{16}$These protocols are based on the fact that, in the general case, a potential eavesdropper destructs a quantum message he attempts to intercept, so that the parties can detect the attempt. Nevertheless, it is based on probabilities and there is always a chance for an eavesdropper to perform only conservative measurements. The corresponding probability is bounded by $r^n$, with $r \in ]0, 1[$ and $n$ the length of the sent message.</footnote>
$U$ and $U^\dagger$ that are themselves prone to error. More precisely, to test against the exact expected value of the state, operator $U^\dagger$ should be equivalent to the computation under test. Practically, gentle measurements approximate the state under test. This enables a simplification of the measurement operator, at the cost of the robustness of the procedure.

## 8.5 Verification of Quantum Communication Protocols

Another challenge for formal methods is the verification of quantum information processes concerns quantum protocols.

Quantum key distribution protocols [164, 22, 128, 134] enable secured information exchanges between two parties. These protocols exploit the fact that, due to the destructive measurement, physics laws prevent almost any $^{16}$ possibility for a potential eavesdropping in the exchange of quantum information. In particular, several formally verified implementations of the BB84 quantum key distribution protocol [22] have been proposed in the literature, based either on process calculus [137, 117], formalization in Coq [28] or model checking [63, 68].

Bordg et al. [30] propose a formalization of quantum information in the ISABELLE/HOL proof assistant. They illustrate their methods through the cases of quantum teleportation and the quantum prisoner dilemma. This work also contains a formally verified implementation of the Deutsch-Jozsa algorithm in ISABELLE/HOL.

In a more fundamental prospect, Echenim et al. [61] provide an ISABELLE/HOL proof for the CHSH inequalities [45]. These are probability distributions about crossed measurement results of quantum observables. They provide a proof for the Bell theorem [21], inducing that no classical theory could account for the entanglement phenomenon (hence that quantum physics cannot be reduced to local classical theories).

# 9 Conclusion

## 9.1 Summary

Throughout this survey, we introduced the context, the main challenges and the most promising results in formally verified quantum programmatic. The current state of affairs in this emerging domain can be summed up as follows:

* Quantum computing is an emerging domain, with huge potential application fields and promises. Progresses in the development of concrete machines are reaching the practical relevance landmark: prototypes are getting powerful enough to overpass classical computers. Consequently, quantum software development is becoming a crucial industrial short-term need;

* Quantum software deals with an entirely new programming paradigm. Upon its main particularities are the dual nature of information (either classical or quantum), the destructive measurement and irreducibly probabilistic computations;

* These specificities make programming particularly non-intuitive and prone to error. Furthermore, they make it very hard to directly import usual debugging methods from the classical

<footnote>$^{16}$These protocols are based on the fact that, in the general case, a potential eavesdropper destructs a quantum message he attempts to intercept, so that the parties can detect the attempt. Nevertheless, it is based on probabilities and there is always a chance for an eavesdropper to perform only conservative measurements. The corresponding probability is bounded by $r^n$, with $r \in ]0, 1[$ and $n$ the length of the sent message.</footnote>
practice (based on test and assertion checking). The technique presented in Section 8.4 might
bring some hope, but this is still so far at a very preliminary stage;

* Formal methods appear as the privileged alternative for debugging strategies. Apart from providing solutions to the destructive measurement challenge, they have additional decisive advantages: mainly, they provide absolute guarantee of the correction of programs, and they hold for any instance of programs they verify;

* During the last ten years (the *genesis* of formal quantum programming), this new field has shown promising results in the different stages of software development: high-level program designs, circuit building languages, verification, compilation, optimization, etc.

## 9.2 Main Current Challenges

Although encouraging, these early successes draw the road map for rising the field from academic proof of concepts to practically usable programming solutions. We present the main coming challenges for this development in three categories: providing relevant integrated development solutions for the NISQ era, offering practical wide spreadable user experience and developing a full-fledged formally verified quantum compilation toolchain.

**Provide relevant integrated development solutions for the NISQ era.** So far, quantum formal verification mainly proved its relevance by offering solutions for the unitary core of quantum computations. As a matter of fact, illustrations and concrete implementations using these techniques primarily treated historical emblematic algorithms such as Shor [174], QPE [111] or Grover search [84]. The classical treatment in these algorithms can be completely decoupled from their quantum core.

However, the first generation of quantum computing machine (the *NISQ era*, see Section 2.3.2) hints towards a radically distinct mode of operation. NISQ machines will have limited, noisy resources. A major consequence is that these quantum processors are too small to support the error correction mechanisms required for Shor's and Grover's algorithms. Such NISQ processors aim instead at different kinds of algorithms: hybrid algorithms such as variational algorithms [135]. Hybrid algorithms tightly mix quantum and classical data treatments: one cannot decouple the quantum part of the algorithm from its classical part.

Adapting the quantum formal methods to the NISQ setting to support hybrid quantum/classical computation is a challenge and an active current research avenue.

**Offer practical wide spreadable user experience: formalism, language design, automation.**

In the present state of development, programming languages enabling formal verification usually sacrifice their expressivity to formal reasoning. In particular, all the solutions that have been probed against actual parametric quantum algorithms fail to satisfy essential elements of the requirements listed in Section 6.1.2 for scalable quantum programming languages: in addition to classical processing mentioned above, they cannot manipulate quantum registers and wire references. Verified programming should address these limitations.

Another issue, while concerning any method of quantum programming, is especially critical in the case of formally verified programming. It concerns the level of qualifications required from developers. The interpretation of quantum computations indeed requires unusual and non-intuitive mathematical formalism (including Kronecker products, complex phase amplitudes, probabilistic reasoning, etc). While the need for qualified programmers is prone to grow rapidly in the coming
practice (based on test and assertion checking). The technique presented in Section 8.4 might
bring some hope, but this is still so far at a very preliminary stage;

* Formal methods appear as the privileged alternative for debugging strategies. Apart from providing solutions to the destructive measurement challenge, they have additional decisive advantages: mainly, they provide absolute guarantee of the correction of programs, and they hold for any instance of programs they verify;

* During the last ten years (the *genesis* of formal quantum programming), this new field has shown promising results in the different stages of software development: high-level program designs, circuit building languages, verification, compilation, optimization, etc.

## 9.2 Main Current Challenges

Although encouraging, these early successes draw the road map for rising the field from academic proof of concepts to practically usable programming solutions. We present the main coming challenges for this development in three categories: providing relevant integrated development solutions for the NISQ era, offering practical wide spreadable user experience and developing a full-fledged formally verified quantum compilation toolchain.

**Provide relevant integrated development solutions for the NISQ era.** So far, quantum formal verification mainly proved its relevance by offering solutions for the unitary core of quantum computations. As a matter of fact, illustrations and concrete implementations using these techniques primarily treated historical emblematic algorithms such as Shor [174], QPE [111] or Grover search [84]. The classical treatment in these algorithms can be completely decoupled from their quantum core.

However, the first generation of quantum computing machine (the *NISQ era*, see Section 2.3.2) hints towards a radically distinct mode of operation. NISQ machines will have limited, noisy resources. A major consequence is that these quantum processors are too small to support the error correction mechanisms required for Shor's and Grover's algorithms. Such NISQ processors aim instead at different kinds of algorithms: hybrid algorithms such as variational algorithms [135]. Hybrid algorithms tightly mix quantum and classical data treatments: one cannot decouple the quantum part of the algorithm from its classical part.

Adapting the quantum formal methods to the NISQ setting to support hybrid quantum/classical computation is a challenge and an active current research avenue.

**Offer practical wide spreadable user experience: formalism, language design, automation.**

In the present state of development, programming languages enabling formal verification usually sacrifice their expressivity to formal reasoning. In particular, all the solutions that have been probed against actual parametric quantum algorithms fail to satisfy essential elements of the requirements listed in Section 6.1.2 for scalable quantum programming languages: in addition to classical processing mentioned above, they cannot manipulate quantum registers and wire references. Verified programming should address these limitations.

Another issue, while concerning any method of quantum programming, is especially critical in the case of formally verified programming. It concerns the level of qualifications required from developers. The interpretation of quantum computations indeed requires unusual and non-intuitive mathematical formalism (including Kronecker products, complex phase amplitudes, probabilistic reasoning, etc). While the need for qualified programmers is prone to grow rapidly in the coming
years, integrating formal verification should come with the development of user-friendly specification languages and highly automated mathematical reasoning engines.

**Formally verified quantum compilation toolchain.** In addition to the preceding considerations, in its early academic ages, quantum formal verification focused on idealized representations of quantum circuits, directly extracted from algorithm descriptions. As introduced in Section 2.3.2, these logical qubits are merely abstract models for actual computations to be run. A major addition that is left for future works in quantum formal verification is error correction, with formal verification that the state of the system preserves the functional correctness of computations (assuming a given error model, and possibly with probabilistic specifications). Presented in Section 5.4, VOQC is a first step towards this goal.

Another future direction concerns integration in a widespread classical development environment. Recall from Section 6.1.3 that many widespread quantum programming languages benefit from embeddings in usual programming languages—such as Python. Today most formal verification solutions are embedded in a more academic functional development environment (such as Haskell, Ocaml, proof assistants or deductive verification environments). Interfaces should be developed to integrate formally verified quantum computations into comprehensive projects.

At the other extremity of the development stack, formal verification should accompany the implementation of compiled programs on concrete machines. This induces verified solutions for the qubit mapping problem and gate simulation (see Section 2.3.3), depending on the particular target material and its proper constraints.

## Acknowledgments

This work was supported in part by the French National Research Agency (ANR) under the research project SoftQPRO ANR-17-CE25-0009-02, by the DGE of the French Ministry of Industry under the research project PIA-GDN/QuantEx P163746-484124, by the STIC-AmSud project Qapla' 21-SITC-10 and by the Carnot project Qstack. We thank the anonymous reviewers for helpful comments on earlier drafts of the manuscript.

## References

[1] Scott Aaronson and Alex Arkhipov. The computational complexity of linear optics. In *Proceedings of the forty-third annual ACM symposium on Theory of computing*, pages 333–342, 2011.

[2] Samson Abramsky and Bob Coecke. Categorical quantum mechanics. In *Handbook of Quantum Logic and Quantum Structures*, pages 261–323. Elsevier, 2009.

[3] Thorsten Altenkirch and Alexander S Green. The quantum IO monad. *Semantic Techniques in Quantum Computation*, pages 173–205, 2010.

[4] Matthew Amy. *Formal Methods in Quantum Circuit Design*. PhD thesis, University of Waterloo, Ontario, Canada, 2019.

[5] Matthew Amy. Towards large-scale functional verification of universal quantum circuits. In *Peter Selinger and Giulio Chiribella, editors, Proceedings 15th International Conference on*
years, integrating formal verification should come with the development of user-friendly specification languages and highly automated mathematical reasoning engines.

**Formally verified quantum compilation toolchain.** In addition to the preceding considerations, in its early academic ages, quantum formal verification focused on idealized representations of quantum circuits, directly extracted from algorithm descriptions. As introduced in Section 2.3.2, these logical qubits are merely abstract models for actual computations to be run. A major addition that is left for future works in quantum formal verification is error correction, with formal verification that the state of the system preserves the functional correctness of computations (assuming a given error model, and possibly with probabilistic specifications). Presented in Section 5.4, VOQC is a first step towards this goal.

Another future direction concerns integration in a widespread classical development environment. Recall from Section 6.1.3 that many widespread quantum programming languages benefit from embeddings in usual programming languages—such as Python. Today most formal verification solutions are embedded in a more academic functional development environment (such as Haskell, Ocaml, proof assistants or deductive verification environments). Interfaces should be developed to integrate formally verified quantum computations into comprehensive projects.

At the other extremity of the development stack, formal verification should accompany the implementation of compiled programs on concrete machines. This induces verified solutions for the qubit mapping problem and gate simulation (see Section 2.3.3), depending on the particular target material and its proper constraints.

## Acknowledgments

This work was supported in part by the French National Research Agency (ANR) under the research project SoftQPRO ANR-17-CE25-0009-02, by the DGE of the French Ministry of Industry under the research project PIA-GDN/QuantEx P163746-484124, by the STIC-AmSud project Qapla' 21-SITC-10 and by the Carnot project Qstack. We thank the anonymous reviewers for helpful comments on earlier drafts of the manuscript.

## References

[1] Scott Aaronson and Alex Arkhipov. The computational complexity of linear optics. In *Proceedings of the forty-third annual ACM symposium on Theory of computing*, pages 333–342, 2011.

[2] Samson Abramsky and Bob Coecke. Categorical quantum mechanics. In *Handbook of Quantum Logic and Quantum Structures*, pages 261–323. Elsevier, 2009.

[3] Thorsten Altenkirch and Alexander S Green. The quantum IO monad. *Semantic Techniques in Quantum Computation*, pages 173–205, 2010.

[4] Matthew Amy. *Formal Methods in Quantum Circuit Design*. PhD thesis, University of Waterloo, Ontario, Canada, 2019.

[5] Matthew Amy. Towards large-scale functional verification of universal quantum circuits. In *Peter Selinger and Giulio Chiribella, editors, Proceedings 15th International Conference on*
*Quantum Physics and Logic*, QPL 2018, volume 287 of *Electronic Proceedings in Theoretical Computer Science*, pages 1–21, Halifax, Canada, 2019. EPTCS.

[6] Matthew Amy, Jianxin Chen, and Neil J. Ross. A finite presentation of CNOT-dihedral operators. In *Bob Coecke and Aleks Kissinger, editors, Proceedings 14th International Conference on Quantum Physics and Logic, Nijmegen, The Netherlands, 3-7 July 2017, volume 266 of Electronic Proceedings in Theoretical Computer Science*, pages 84–97, 2018.

[7] Matthew Amy, Dmitri Maslov, and Michele Mosca. Polynomial-time T-depth optimization of Clifford+T circuits via matroid partitioning. *IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems*, 33(10):1476–1489, 2014.

[8] Krzysztof R. Apt and Ernst-Rüdiger Olderog. Fifty years of Hoare's logic. *Formal Aspects Comput.*, 31(6):751–807, 2019.

[9] Frank Arute, Kunal Arya, Ryan Babbush, Dave Bacon, Joseph C. Bardin, Rami Barends, Rupak Biswas, Sergio Boixo, Fernando G. S. L. Brandao, David A. Buell, et al. Quantum supremacy using a programmable superconducting processor. *Nature*, 574(7779):505–510, 2019.

[10] Miriam Backens. The ZX-calculus is complete for stabilizer quantum mechanics. In *New Journal of Physics*, volume 16, page 093021. IOP Publishing, Sep 2014.

[11] Miriam Backens, Hector Miller-Bakewell, Giovanni de Felice, Leo Lobski, and John van de Wetering. There and back again: A circuit extraction tale. *Quantum*, 5:421, 2021.

[12] Thomas Ball, Byron Cook, Vladimir Levin, and Sriram K. Rajamani. Slam and static driver verifier: Technology transfer of formal methods inside microsoft. In *Integrated Formal Methods, 4th International Conference, IFM 2004*. Springer, 2004.

[13] Alexandru Baltag, Jort Bergfeld, Kohei Kishida, Joshua Sack, Sonja Smets, and Shengyang Zhong. Plqp & company: decidable logics for quantum algorithms. *International Journal of Theoretical Physics*, 53(10):3628–3647, 2014.

[14] Alexandru Baltag and Sonja Smets. LQP: the dynamic logic of quantum information. *Mathematical Structures in Computer Science*, 16(3):491–525, 2006.

[15] Alexandru Baltag and Sonja Smets. The logic of quantum programs. CoRR, abs/2109.06792, 2021.

[16] Henk P. Barendregt. *The Lambda-Calculus, its Syntax and Semantics*, volume 103 of *Studies in Logic and the Foundation of Mathematics*. North Holland, second edition, 1984.

[17] Mike Barnett, Manuel Fähndrich, K. Rustan M. Leino, Peter Müller, Wolfram Schulte, and Herman Venter. Specification and verification: the SPEC# experience. *Commun. ACM*, 54(6):81–91, 2011.

[18] Clark Barrett and Cesare Tinelli. Satisfiability modulo theories. In *Handbook of model checking*, pages 305–343. Springer, 2018.

[19] Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, and Li Zhou. Relational proofs for quantum programs. Proc. ACM Program. Lang., 4(POPL):21:1–21:29, 2020.
*Quantum Physics and Logic*, QPL 2018, volume 287 of *Electronic Proceedings in Theoretical Computer Science*, pages 1–21, Halifax, Canada, 2019. EPTCS.

[6] Matthew Amy, Jianxin Chen, and Neil J. Ross. A finite presentation of CNOT-dihedral operators. In *Bob Coecke and Aleks Kissinger, editors, Proceedings 14th International Conference on Quantum Physics and Logic, Nijmegen, The Netherlands, 3-7 July 2017, volume 266 of Electronic Proceedings in Theoretical Computer Science*, pages 84–97, 2018.

[7] Matthew Amy, Dmitri Maslov, and Michele Mosca. Polynomial-time T-depth optimization of Clifford+T circuits via matroid partitioning. *IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems*, 33(10):1476–1489, 2014.

[8] Krzysztof R. Apt and Ernst-Rüdiger Olderog. Fifty years of Hoare's logic. *Formal Aspects Comput.*, 31(6):751–807, 2019.

[9] Frank Arute, Kunal Arya, Ryan Babbush, Dave Bacon, Joseph C. Bardin, Rami Barends, Rupak Biswas, Sergio Boixo, Fernando G. S. L. Brandao, David A. Buell, et al. Quantum supremacy using a programmable superconducting processor. *Nature*, 574(7779):505–510, 2019.

[10] Miriam Backens. The ZX-calculus is complete for stabilizer quantum mechanics. In *New Journal of Physics*, volume 16, page 093021. IOP Publishing, Sep 2014.

[11] Miriam Backens, Hector Miller-Bakewell, Giovanni de Felice, Leo Lobski, and John van de Watering. There and back again: A circuit extraction tale. *Quantum*, 5:421, 2021.

[12] Thomas Ball, Byron Cook, Vladimir Levin, and Sriram K. Rajamani. Slam and static driver verifier: Technology transfer of formal methods inside microsoft. In *Integrated Formal Methods, 4th International Conference, IFM 2004*. Springer, 2004.

[13] Alexandru Baltag, Jort Bergfeld, Kohei Kishida, Joshua Sack, Sonja Smets, and Shengyang Zhong. Plqp & company: decidable logics for quantum algorithms. *International Journal of Theoretical Physics*, 53(10):3628–3647, 2014.

[14] Alexandru Baltag and Sonja Smets. LQP: the dynamic logic of quantum information. *Mathematical Structures in Computer Science*, 16(3):491–525, 2006.

[15] Alexandru Baltag and Sonja Smets. The logic of quantum programs. CoRR, abs/2109.06792, 2021.

[16] Henk P. Barendregt. *The Lambda-Calculus, its Syntax and Semantics*, volume 103 of *Studies in Logic and the Foundation of Mathematics*. North Holland, second edition, 1984.

[17] Mike Barnett, Manuel Fähndrich, K. Rustan M. Leino, Peter Müller, Wolfram Schulte, and Herman Venter. Specification and verification: the SPEC# experience. *Commun. ACM*, 54(6):81–91, 2011.

[18] Clark Barrett and Cesare Tinelli. Satisfiability modulo theories. In *Handbook of model checking*, pages 305–343. Springer, 2018.

[19] Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, and Li Zhou. Relational proofs for quantum programs. *Proc. ACM Program. Lang.*, 4(POPL):21:1–21:29, 2020.