Revisiting the Fast Fourier Transform in Rocq
Laurent Th\'ery (STAMP)
TL;DR
This paper formalizes and verifies the correctness of the standard Fast Fourier Transform algorithm within the Coq proof assistant, ensuring its mathematical soundness through formal proof techniques.
Contribution
It introduces a formal proof of the FFT algorithm's correctness in Coq, enhancing trustworthiness and rigor in its implementation.
Findings
Successful formal verification of FFT in Coq
Enhanced confidence in FFT correctness
Framework for verifying similar algorithms
Abstract
This notes explains how a standard algorithm that constructs the discrete Fourier transform has been formalised and proved correct in the Coq proof assistant using the SSReflect extension.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsModeling and Simulation Systems