Resource verification of quantum circuit description languages

Quantum computing promises to enable a range of tasks currently deemed intractable by classical means, and as such it constitutes a blooming field of research. One important research direction in this area is that of quantum circuit description languages. These are classical programming languages in which quantum operations are buffered to a quantum circuit, which can eventually be executed, or reused to describe larger circuits. This approach allows for the implementation of sophisticated algorithms, which can involve trillions of gates and millions of qubits. Unfortunately, existing quantum architectures are small and noisy, which means that quantum circuit description programs often generate circuits that are simply too large for the underlying hardware. To address this issue, it is essential to develop static analysis techniques for the resource consumption of these programs. The contribution of this thesis is twofold. On one hand, we show how type systems with effects and refinements can be used to analyze the resource consumption of functional circuit description languages, such as Quipper. We present a type-and-effect system which is capable of deriving upper bounds on the size of the circuits generated by a program, according to varying notions of size. We also show that the type system is correct, under reasonable assumptions about the underlying size metric, and we provide an implementation of the theory in the form of a resource analysis tool called QuRA, which we show to be able to automatically verify the resource consumption of real-world quantum algorithms. On the other hand, we show how Hoare logics can be easily adapted to analyze the resource consumption of imperative circuit description languages, such as Qiskit. We formalize the circuit building semantics of the language and define a deduction system for Hoare triples, which we prove to be correct in the partial sense.