We provide axioms that guarantee a category is equivalent to that of continuous linear functions between Hilbert spaces. The axioms are purely categorical and do not presuppose any analytical structure. This addresses a question about the mathematica
l foundations of quantum theory raised in reconstruction programmes such as those of von Neumann, Mackey, Jauch, Piron, Abramsky, and Coecke.
We introduce the monoidal closed category qCPO of quantum cpos, whose objects are quantized analogs of omega-complete partial orders (cpos). The category qCPO is enriched over the category CPO of cpos, and contains both CPO, and the opposite of the c
ategory FdAlg of finite-dimensional von Neumann algebras as monoidal subcategories. We use qCPO to construct a sound model for the quantum programming language Proto-Quipper-M (PQM) extended with term recursion, as well as a sound and computationally adequate model for the Linear/Non-Linear Fixpoint Calculus (LNL-FPC), which is both an extension of the Fixpoint Calculus (FPC) with linear types, and an extension of a circuit-free fragment of PQM that includes recursive types.
