2013/11/26 by Philip Atzemoglou, Atzemoglou, Philip
Computer Science · Mathematics · Physics and Astronomy · #Category Theory (math.CT) #Computability, Logic, AI Algorithms #FOS: Computer and information sciences #FOS: Mathematics #FOS: Physical sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Programming Languages (cs.PL) #Quantum Physics (quant-ph) #cs.LO #cs.PL #math.CT #quant-ph
paper · pdf · doi:10.48550/arxiv.1311.6563
DPhil Thesis. See full text for unabridged abstract
arxiv created 2013/11/26 · openalex publication_date 2013/11/26 · arxiv updated 2013/11/27 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.