  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.
