  A logical system derived from linear logic and called QMLL is introduced and
shown able to capture all unitary quantum circuits. Conversely, any proof is
shown to compute, through a concrete GoI interpretation, some quantum circuits.
The system QMLL, which enjoys cut-elimination, is obtained by endowing
multiplicative linear logic with a quantum modality.
