In 2004-2006 we designed new dynamic quantum logic to reason about compound quantum systems in [A. Baltag and S. Smets, The Logic of Quantum Programs, In QPL2004, TUCS General Publication, vol.33, pp.39-56, Turku Center for Computer Science, 2004] and [A. Baltag and S. Smets, LQP: The Dynamic Logic of Quantum Information, in Mathematical Structures in Computer Science, 16(3):491-525, 2006].Â
This work brings together ideas from the quantum logic tradition with concepts from (dynamic) modal logic and from quantum computation. The Logic of Quantum Programs (LQP) is capable of expressing important features of quantum measurements and unitary evolutions of multi-partite states, as well as giving logical characterisations to various forms of entanglement (for example, the Bell states, the GHZ states etc.). In this work we offered a finitary syntax, a relational semantics and a sound proof system for the LQP logic. As applications, we use the logical system to give formal correctness proofs for the Teleportation protocol and for a standard Quantum Secret Sharing protocol; a whole range of other quantum circuits and programs, including other well-known protocols (for example, superdense coding, entanglement swapping, logic-gate teleportation etc.), can be similarly verified using this logical system.