Formalizing the Semantics of a Classical-Quantum Imperative Language in Maude

Recent advancements in quantum computing have exhibited substantial promise across domains such as formal verification and quantum communication. However, formal verification of hybrid quantum-classical programs remains challenging due to the complex interactions between classical control logic and quantum operations. In this paper, we propose an executable operational semantics for the Classical-Quantum Imperative Language (QIMP), implemented using the Maude system. Our framework employs rewrite rules to precisely capture classical-quantum interactions, particularly the probabilistic branching induced by quantum measurements. Experimental validation using representative algorithms, such as Quantum Teleportation and the BB84 protocol, demonstrates the capability of our semantics to accurately simulate quantum behaviors including state evolution, collapse, and classical state updates, highlighting its applicability and scalability in formal verification tasks.