A promising approach to efficient quantum computation is to execute subroutines in parallel at a fine-grained level. While such parallelism is subject to tricky bugs, there was no quantum program logic that could modularly verify the correctness of such parallelism.

To overcome this situation, we propose novel concurrent quantum separation logic that can modularly reason about quantum programs under fine-grained parallelism. Our logic enables flexible reasoning about quantum superposition via new proof rules for linearly combining Hoare triples. Also, our logic introduces fractional tokens for sharing the same qubits between parallel subroutines, introducing new reasoning rules for promoting partial ownership into full ownership by atomicity. We demonstrate the effectiveness of our logic by verifying a non-trivial parallelized quantum program.