PhD Thesis

A Verified Software Toolchain For Quantum Programming

Quantum computing is steadily moving from theory into practice, with small-scale quantum computers available for public use. Now quantum programmers are faced with a classical problem: How can they be sure that their code does what they intend it to …

On a Categorically Sound Quantum Programming Language for Circuit Description

This thesis contains contributions to the mathematical foundations of quantum programming languages. The likely arrival of scalable quantum computers in the not so distant future has resulted in a flurry of activity in the development of quantum …

Development of Quantum Applications

The aim of this thesis is to identify practical applications where quantum computing could have an advantage over what is achievable with conventional means of computing, and what advances are needed in order to actualize that potential. We …

Formal Methods in Quantum Circuit Design

The design and compilation of correct, efficient quantum circuits is integral to the future operation of quantum computers. This thesis makes contributions to the problems of optimizing and verifying quantum circuits, with an emphasis on the …

Formally Verified Quantum Programming

The field of quantum mechanics predates computer science by at least ten years, the time between the publication of the Schrodinger equation and the Church-Turing thesis. It took another fifty years for Feynman to recognize that harnessing quantum …

Linear/Non-Linear Types for Embedded Domain-Specific Languages

Domain-specific languages are often embedded inside of general-purpose host languages so that the embedded language can take advantage of host-language data structures, libraries, and tools. However, when the domain-specific language uses linear …

Algebraic and Logical Methods in Quantum Computation

This thesis contains contributions to the theory of quantum computation. We first define a new method to efficiently approximate special unitary operators. Specifically, given a special unitary U and a precision epsilon 0, we show how to efficiently …

Towards a Formally Verified Functional Quantum Programming Language

This thesis looks at the development of a framework for a functional quantum programming language. The framework is first developed in Haskell, looking at how a monadic structure can be used to explicitly deal with the side-effects inherent in the …

Structured Quantum Programming

Describes QCL