Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Quantum Fourier Transform

view this post on Zulip Email Gateway (Feb 21 2025 at 14:18):

From: "Thiemann, René" <cl-isabelle-users@lists.cam.ac.uk>
Dear all,

I’m happy to announce a new AFP entry.

Quantum Fourier Transform
by Pablo Manrique

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.

https://www.isa-afp.org/entries/Quantum_Fourier_Transform.html

Enjoy,
René

Last updated: Mar 09 2025 at 12:28 UTC