2014/12/30 by Robin Adams
Computer Science · #cs.LO #cs.ET
paper · pdf · doi:10.4204/eptcs.172.10
published as EPTCS 172, 2014, pp. 133-153 · In Proceedings QPL 2014, arXiv:1412.8102
arxiv created 2014/12/30 · arxiv updated 2014/12/31
We present the syntax and rules of deduction of QPEL (Quantum Program and Effect Language), a language for describing both quantum programs, and properties of quantum programs - effects on the appropriate Hilbert space. We show how semantics may be given in terms of state-and-effect triangles, a categorical setting that allows semantics in terms of Hilbert spaces, C*-algebras, and other categories. We prove soundness and completeness results that show the derivable judgements are exactly those provable in all state-and-effect triangles.