  We define a language CQP (Communicating Quantum Processes) for modelling
systems which combine quantum and classical communication and computation. CQP
combines the communication primitives of the pi-calculus with primitives for
measurement and transformation of quantum state; in particular, quantum bits
(qubits) can be transmitted from process to process along communication
channels. CQP has a static type system which classifies channels, distinguishes
between quantum and classical data, and controls the use of quantum state. We
formally define the syntax, operational semantics and type system of CQP, prove
that the semantics preserves typing, and prove that typing guarantees that each
qubit is owned by a unique process within a system. We illustrate CQP by
defining models of several quantum communication systems, and outline our plans
for using CQP as the foundation for formal analysis and verification of
combined quantum and classical systems.
