Xiaodi Wu

Latest

• Verified Compilation of Quantum Oracles
• Algebraic Reasoning of Quantum Programs via Non-Idempotent Kleene Algebra
• A Formally Certified End-to-End Implementation of Shor's Factorization Algorithm
• A Verified Optimizer for Quantum Circuits
• Invariants of Quantum Programs: Characterisations and Generation