Quantum Fourier Transform

Abstract

This work presents a formalization of the Quantum Fourier Transform, a fundamental component of Shor's factoring algorithm, with proofs of its correctness and unitarity. The proof is carried out by induction, relying on the algorithm's recursive definition. This formalization builds upon the Isabelle Marries Dirac quantum computing library, developed by A. Bordg, H. Lachnitt, and Y. He.

License

BSD License

Topics

Related publications

Nielsen, M. A., & Chuang, I. L. (2012). Quantum Computation and Quantum Information. https://doi.org/10.1017/cbo9780511976667
Bordg, A., Lachnitt, H., & He, Y. (2020). Certified Quantum Computation in Isabelle/HOL. Journal of Automated Reasoning, 65(5), 691–709. https://doi.org/10.1007/s10817-020-09584-7
Peng, Y., Hietala, K., Tao, R., Li, L., Rand, R., Hicks, M., & Wu, X. (2022). A Formally Certified End-to-End Implementation of Shor's Factorization Algorithm (Version 1). arXiv. https://doi.org/10.48550/ARXIV.2204.07112

Session Quantum_Fourier_Transform

Depends on

Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information