  We define syntax and semantics of quantum circuits, allowing measurement
gates and classical channels. We define circuit-based quantum algorithms and
prove that, semantically, any such algorithm is equivalent to a single
measurement that depends only on the underlying quantum circuit. Finally, we
use our formalization of quantum circuits to state precisely and prove the
principle of deferred measurements.
