  CoqQ is a framework for reasoning about quantum programs in the Coq proof
assistant. Its main components are: a deeply embedded quantum programming
language, in which classic quantum algorithms are easily expressed, and an
expressive program logic for proving properties of programs. CoqQ is
foundational: the program logic is formally proved sound with respect to a
denotational semantics based on state-of-art mathematical libraries (mathcomp
and mathcomp analysis). CoqQ is also practical: assertions can use Dirac
expressions, which eases concise specifications, and proofs can exploit local
and parallel reasoning, which minimizes verification effort. We illustrate the
applicability of CoqQ with many examples from the literature.
