A Quantum Programming Language for Coherent Control

We introduce a programming language that allows for the coherent control of arbitrary quantum operations. The problem of defining coherent control beyond the unitary case, using, for example, a quantum conditional in the presence of recursion or iteration has long been known to be a major difficulty. We resolve this problem by defining an operational semantics based on appropriate Kraus decompositions and a denotational semantics based on vacuum-extensions. We show that the language is universal for vacuum-extensions and that the two semantics are adequate. Moreover, we define a notion of observational equivalence: two programs are equivalent if their probability of termination is the same in any context. The denotational semantics is shown to be fully abstract for observational equivalence.