  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.
