Concurrent Quantum Separation Logic for Fine-Grained Parallelism

This conference talk presents a novel concurrent quantum separation logic for verifying fine-grained parallelism in quantum computing. Learn about a groundbreaking approach that enables modular reasoning about quantum programs executing parallel subroutines at a fine-grained level. The speakers, Yusuke Matsushita, Kengo Hirata, and Ryo Wakizaka from Kyoto University and University of Edinburgh, introduce innovative proof rules for linearly combining Hoare triples to reason about quantum superposition, along with fractional tokens for sharing qubits between parallel subroutines. Discover how this logic promotes partial ownership into full ownership through atomicity, and see its effectiveness demonstrated through verification of a non-trivial parallelized quantum program. This 24-minute presentation was delivered at the PLanQC 2025 workshop on January 25, 2025, sponsored by ACM SIGPLAN.