Familiarity with quantum mechanics will not be assumed

The current methods available for developing quantum algorithms and protocols are deficient on two main levels. Firstly, they are too low-level. Quantum algorithms are currently mainly described using the `network model' corresponding to circuits in classical computation. One finds a plethora of ad hoc calculations with `bras' and `kets', normalizing constants, matrices etc. The arguments for the benefits of a high-level, conceptual approach to designing, programming and reasoning about quantum computational systems are just as compelling as for classical computation. Moreover, there is the whole issue of integrating quantum and classical features, which would surely be mandatory in any practicable system. At a more fundamental level, the standard mathematical framework for quantum mechanics is actually insufficiently comprehensive for informatic purposes: in particular, the flow of information from quantum to classical arising from measurements, and the dependence of subsequent stages of the computation on this information, is not adequately covered by the standard formalism. As quantum protocols and computations grow more elaborate and complex, this point is likely to prove of increasing importance.

In [Abramsky and Coecke 2004] we addressed these problems, the key ingredient being a categorical axiomatization of quantum mechanics. The concepts of abstract quantum mechanics are formulated in any strongly compact closed category with biproducts (of which the category FdHilb of finite dimensional Hilbert spaces and linear maps is an example). Preparations, measurements, and classical data exchange are all morphisms in the category, and their types fully reflect their kinds. Correctness properties of standard quantum protocols can be proved at this abstract level. Although this setting seems purely qualitative, in fact even the Born rule, which specifies how probabilities are calculated, can be derived. There are also connections to logic; the calculations in abstract quantum mechanics can be performed as cut elimination on (possibly cyclic) proof nets; loops generate scalars (typically, probabilities or probability amplitudes).

The talk will be in two parts: the first part, given by Abramsky, will give an overview of our work, and the second part, by Coecke, will supply more detail, and examine a case study of verifying the teleportation protocol.

References

J. von Neumann. Mathematische Grundlagen der Quantenmechanik. Springer-Verlag (1932). English translation in Mathematical Foundations of Quantum Mechanics. Princeton University Press (1955).

S. Abramsky and B. Coecke. A categorical semantics of quantum protocols. In the proceedings of LiCS'04 (2004). An extended version is available at arXiv:quant-ph/0402130.