In this talk, we will present an overview of our work on the use of operator algebras as categorical models for quantum programming languages. Starting from a mathematical connection between operator theory and domain theory, we will detail some of the categorical properties of operator algebras, which can be represented as categories of presheaves. We present a general categorical framework for the semantics of embedded quantum programming languages as instances of enriched category theory, and establish some connection with probabilistic models, and Benton-style linear-non-linear models.

We explain how W*-algebras fit within this framework. In detail, the denotational semantics is described as follows: every program type is interpreted as a W*-algebra and every program is interpreted as a normal completely positive subunital map. These operator algebras were introduced by von Neumann himself, and motivated by his study of quantum mechanics. The theory of operator algebras has found direct application in various fields such as quantum information theory and quantum field theory.

We identify some relevant categorical properties of W*-algebras and show they form a suitable setting for the mathematical interpretation of a first-order quantum programming language with inductive datatypes. Since qubits are easily representable in a W*-algebra, the denotational semantics supports many features relevant to quantum programming languages. We finally consider applications to verification and categorical axiomatics for quantum computing.