Dagger Compact Closed Categories and Completely Positive Maps

Dagger compact closed categories were recently introduced by Abramsky and Coecke, under the name strongly compact closed categories, as an axiomatic framework for quantum mechanics. We present a graphical language for dagger compact closed categories, and sketch a proof of its completeness for equational reasoning. We give a general construction, the CPM construction, which associates to each dagger compact closed category its category of completely positive maps, and we show that the resulting category is again dagger compact closed. We apply these ideas to Abramsky and Coecke's interpretation of quantum protocols, and to D'Hondt and Panangaden's predicate transformer semantics.