Formal Semantics and Analysis of Quantum Programs

Programming quantum is a key skill, and quantum software engineering is emerging as a new frontier for programming language theory and formal methods. Unlike classical programs, quantum computations evolve over vector spaces and obey quantum-mechanical principles; phenomena such as superposition, entanglement, no-cloning, and implicit measurement introduce behaviors that analyses must capture. Abstract interpretation [CC77; Cou21b] and static analysis [RY20; NNH99] provide powerful reasoning tools but require substantial adaptation if applied to quantum programming languages. Similarly, as quantum computation reshapes program states and control flow, classical analysis techniques cannot be applied directly; new domains are needed for quantum-specific properties such as entanglement, and coherent control introduces semantic challenges with no classical analog. After reviewing prior work (Chapter 3), this thesis presents three new abstract interpretation based approaches addressing uncomputation, entanglement, and robustness of variational quantum circuits, together with a semantic framework for quantum control flow. The first contribution (Chapter 4) defines a framework for reasoning about the use and lifetime of quantum variables. Because of no-cloning and entanglement, copying and deletion require careful treatment; in particular, unused variables must be reset before being discarded, so as to avoid implicit measurement. Two data-flow analyses—a forward consuming analysis and a backward uncomputation analysis—relax linear typing while ensuring soundness and enabling automatic insertion of discard operations. The second contribution (Chapter 5) develops an abstract domain for reasoning about entanglement. It captures inseparability relations and qualitative features of qubit states (superposition, phase), enabling sound tracking without exponential blow-up and supporting entanglement-aware optimization. The third contribution (Chapter 6) extends formal verification to variational quantum circuits (VQCs). The thesis formalizes the robustness verification problem for VQCs, proves its NP-hardness, and defines concrete and abstract semantics for a VQC language. Refinement strategies—clipping, symbolic execution, and domain partitioning—improve interval precision, yielding a practical pipeline that certifies robustness guarantees. Finally, Chapter 7 introduces a denotational semantics for quantum loops. Since measurement based control is disallowed and unitary semantics cannot model unbounded behaviors, we introduce a linear semantics based on bounded operators to ensure convergence at the cost of a sound approximation of the concrete evolution, thus providing a foundation for reasoning about termination and divergence.