Higher-order semantics for quantum programming languages with classical control

TL;DR

This thesis develops a categorical framework for quantum programming languages by extending a lambda calculus with classical control, enabling formal reasoning about quantum algorithms and their classical interactions.

Contribution

It introduces the dagger lambda calculus and enhances it with classical control structures, bridging categorical quantum theory with practical quantum programming.

Findings

Created the dagger lambda calculus for dagger compact categories.

Extended the calculus with classical control using classical structures and dualisers.

Applied the calculus to solve well-known problems in quantum computation.

Abstract

This thesis studies the categorical formalisation of quantum computing, through the prism of type theory, in a three-tier process. The first stage of our investigation involves the creation of the dagger lambda calculus, a lambda calculus for dagger compact categories. Our second contribution lifts the expressive power of the dagger lambda calculus, to that of a quantum programming language, by adding classical control in the form of complementary classical structures and dualisers. Finally, our third contribution demonstrates how our lambda calculus can be applied to various well known problems in quantum computation.