LQP: the dynamic logic of quantum information

13 years 6 months ago
LQP: the dynamic logic of quantum information
We present a dynamic logic for reasoning about information flow in quantum programs. In particular, we give a finitary syntax and a relational semantics for a Logic of Quantum Programs (LQP), that is capable of dealing with quantum measurements, unitary evolutions and entanglements in compound quantum systems. We present a sound proof system for this logic, and we show how to characterize by logical means various forms of entanglement (e.g. the Bell states) and various quantum gates. As an example of application, we use our logic to give a formal proof for the correctness of the Teleportation protocol (proof which can be easily adapted to check Logic-Gate Teleportation).
Alexandru Baltag, Sonja Smets
Added 14 Dec 2010
Updated 14 Dec 2010
Type Journal
Year 2006
Where MSCS
Authors Alexandru Baltag, Sonja Smets
Comments (0)