Higher-order semantics for quantum programming languages with classical control

Thesis

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: Quantum Key Distribution, the quantum Fourier transform, and the teleportation protocol./

Authors: Atzemoglou, GP

• Publication date: 2012
• Type of award: DPhil
• Level of award: Doctoral
• Awarding institution: University of Oxford
• Language: English
• Keywords: quantum computing; programming languages; category theory; logic; lambda calculus; computer science
• Subjects: Mathematical logic and foundations; Computer science (mathematics); Quantum theory (mathematics); Theory and automated verification