Bit commitment is a cryptographic task in which Alice commits a bit to Bob such that she cannot change the value of the bit after her commitment and Bob cannot learn the value of the bit before Alice opens her commitment. According to the Mayers–Lo–Chau (MLC) no-go theorem, ideal bit commitment is impossible within quantum theory. In the information theoretic-reconstruction of quantum theory, the impossibility of quantum bit commitment is one of the three information-theoretic constraints that characterize quantum theory. In this paper, we first provide a very simple proof of the MLC no-go theorem and its quantitative generalization. Then, we formalize bit commitment in the theory of dagger monoidal categories. We show that in the setting of dagger monoidal categories, the impossibility of bit commitment is equivalent to the unitary equivalence of purification.

The long-term goal of our research is to develop a powerful quantum logic which is useful in the formal verification of quantum programs and protocols. In this paper we introduce the basic idea of our categorical logic of quantum programs (CLQP): It combines the logic of quantum programming (LQP) and categorical quantum mechanics (CQM) such that the advantages of both LQP and CQM are preserved while their disadvantages are overcome. We present the syntax, semantics and proof system of CLQP. As a proof-of-concept, we apply CLQP to verify the correctness of Deutsch’s algorithm and the concealing property of quantum bit commitment.