Towards a semantics for higher-order quantum computation

Abstract

The search for a semantics for higher-order quantum computation leads naturallyto the study of categories of normed cones. In the first part of this paper, we develop the theory of continuous normed cones, and prove some of their basic properties, includinga Hahn-Banach style theorem. We then describe two different concrete *-autonomous categories of normed cones. The first of these categories is built from completelypositive maps as in the author's semantics of first-order quantum computation. The second category is a reformulation of Girard's quantum coherent spaces. We also pointout why ultimately, neither of these categories is a satisfactory model of higher-order quantum computation.