The Logic of Quantum Programs

Abstract

We present a logical calculus for reasoning about information flow in quantum programs. In particular we introduce a dynamic logic that is capable of dealing with quantum measurements, unitary evolutions and entanglements in compound quantum systems. We give a syntax and a relational semantics in which we abstract away from phases and probabilities. 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 linear operators. As an example we sketch an analysis of the teleportation protocol.

arXiv comment18 pages, date 2004, presented at the 2nd International Workshop on Quantum Programming Languages, affiliated to LICS 2004

Cited by in corpus (7)

• Weakly complete axiomatization of exogenous quantum propositional logic
• Quantum Temporal Logic
• Hoare Logic for Quantum Programs
• Semantics for first-order superposition logic
• LQP: The Dynamic Logic of Quantum Information
• Logic Column 13: Reasoning Formally about Quantum Systems: An Overview
• A Quantum Interpretation of Bunched Logic for Quantum Separation Logic