2025/07/14 by Barsse, Kathleen, Péchoux, Romain, Perdrix, Simon
#F.3.2 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.2507.10466
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.