PhD Proposal: Towards Trustworthy Distributed Quantum Computing: From Programming, Semantics, and Verification to Executable Programs

Distributed quantum computing is a leading approach to scaling quantum computation beyond the capacity of a single quantum processing unit. At the same time, this setting introduces programming, semantics, and verification challenges as quantum communications have environment-dependent costs, measurements induce probabilistic control flow, and distributed execution introduces scheduling nondeterminism. These features make it difficult to reason end-to-end from high-level, large-scale quantum programs to executable implementations and machine-checkable correctness arguments.
To address these challenges, I propose four complementary frameworks for trustworthy distributed quantum computing: (1) Quantum Shared Memory (QSM), a programming-runtime abstraction boundary for adaptive distributed execution; (2) DisQ, a distributed semantic model with refinement support for relating implementations to higher-level specifications; (3) a compositional LOCC verification framework based on quantum Hoare logic over entangled resources, with ongoing Coq mechanization for reusable proof infrastructure; and (4) a certified lowering framework from verified LOCC programs to distributed executable artifacts, which will define a restricted lowering function and prove that admissible target executions preserve the source-level postcondition under an explicit schedule policy.