Sequent Calculus Representations for Quantum Circuits

Cameron Beebe

When considering a sequent-style proof system for quantum programs, there are certain elements of quantum mechanics that we may wish to capture, such as phase, dynamics of unitary transformations, and measurement probabilities. Traditional quantum logics which focus primarily on the abstract orthomodular lattice theory and structures of Hilbert spaces have not satisfactorily captured some of these elements. We can start from 'scratch' in an attempt to conceptually characterize the types of proof rules which should be in a system that represents elements necessary for quantum algorithms. This present work attempts to do this from the perspective of the quantum circuit model of quantum computation. A sequent calculus based on single quantum circuits is suggested, and its ability to incorporate important conceptual and dynamic aspects of quantum computing is discussed. In particular, preserving the representation of phase helps illustrate the role of interference as a resource in quantum computation. Interference also provides an intuitive basis for a non-monotonic calculus.

In Alastair A. Abbott and Dominic C. Horsman: Proceedings of the 7th International Workshop on Physics and Computation (PC 2016), Manchester, UK, 14 July 2016, Electronic Proceedings in Theoretical Computer Science 214, pp. 3–15.
Published: 21st June 2016.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: