Revisiting the Fast Fourier Transform in Rocq
Logic in Computer Science
2025-08-15 v5
Authors:
Laurent Théry
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.
Cite
@article{arxiv.2210.05225,
title = {Revisiting the Fast Fourier Transform in Rocq},
author = {Laurent Théry},
journal= {arXiv preprint arXiv:2210.05225},
year = {2025}
}
Related papers
View all related →
Data Structures and Algorithms · Computer Science
A Formalisation of Algorithms for Sorting Network
Laurent Théry
2022-03-04
Artificial Intelligence · Computer Science
Verifying an algorithm computing Discrete Vector Fields for digital imaging
Jónathan Heras, María Poza, Julio Rubio
2012-07-16
Logic in Computer Science · Computer Science
Formalizing Higher-Order Termination in Coq
Deivid Vale, Niels van der Weide
2021-12-14
Logic in Computer Science · Computer Science
Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant
Théo Zimmermann, Hugo Herbelin
2015-07-10
Logic in Computer Science · Computer Science
Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
Assia Mahboubi, Cyril Cohen
2015-07-01
Programming Languages · Computer Science
MirrorShard: Proof by Computational Reflection with Verified Hints
Gregory Malecha, Adam Chlipala, Thomas Braibant, Patrick Hulin +1
2013-05-29
Logic in Computer Science · Computer Science
A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq
Reynald Affeldt, Zachary Stone
2024-07-02
Numerical Analysis · Mathematics
Approximating the Analytic Fourier Transform with the Discrete Fourier Transform
Jeremy Axelrod
2015-08-07
Logic in Computer Science · Computer Science
Towards Automatic Transformations of Coq Proof Scripts
Nicolas Magaud
2024-01-23
Programming Languages · Computer Science
Accelerating Verified-Compiler Development with a Verified Rewriting Engine
Jason Gross, Andres Erbsen, Jade Philipoom, Rajashree Agrawal +1
2025-03-12
Numerical Analysis · Mathematics
The Fourier Cosine Method for Discrete Probability Distributions
Xiaoyu Shen, Fang Fang, Chengguang Liu
2024-10-10
Logic in Computer Science · Computer Science
A formalization of convex polyhedra based on the simplex method
Xavier Allamigeon, Ricardo D. Katz
2018-08-14
Data Structures and Algorithms · Computer Science
Discrete and Fast Fourier Transform Made Clear
Peter Zeman
2019-08-21
Numerical Analysis · Mathematics
Fast complexified quaternion Fourier transform
Salem Said, Nicolas Le Bihan, Stephen J. Sangwine
2008-03-19
Programming Languages · Computer Science
Verified Self-Explaining Computation
Jan Stolarek, James Cheney
2019-07-15
Logic in Computer Science · Computer Science
Structural abstract interpretation, A formal study using Coq
Yves Bertot
2008-10-20
Machine Learning · Computer Science
Fast Partial Fourier Transform
Yong-chan Park, Jun-Gi Jang, U Kang
2020-08-31
Mathematical Physics · Physics
Form factor (Fourier shape transform) of polygon and polyhedron
Joachim Wuttke
2021-06-01
Combinatorics · Mathematics
Fourier transforms of polytopes, solid angle sums, and discrete volume
Ricardo Diaz, Quang-Nhat Le, Sinai Robins
2018-08-02
Logic in Computer Science · Computer Science
Machine-Checked Categorical Diagrammatic Reasoning
Benoît Guillemet, Assia Mahboubi, Matthieu Piquerez
2024-03-01
Discrete Mathematics · Computer Science
New Algorithms for Computing a Single Component of the Discrete Fourier Transform
G. Jerônimo da Silva, R. M. Campello de Souza, H. M. de Oliveira
2018-01-24
Logic in Computer Science · Computer Science
General Automation in Coq through Modular Transformations
Valentin Blot, Louise Dubois de Prisque, Chantal Keller, Pierre Vial
2021-07-07
Quantum Physics · Physics
Discrete quantum Fourier transform in coupled semiconductor double quantum dot molecules
Ping Dong, Ming Yang, Zhuo-Liang Cao
2009-11-13
Numerical Analysis · Mathematics
Discrete Weierstrass Fourier Transform and Experiments
Sheng Zhang, Brendan Harding
2016-01-07
Signal Processing · Electrical Eng. & Systems
Discrete Fourier Transform Approximations Based on the Cooley-Tukey Radix-2 Algorithm
D. F. G. Coelho, R. J. Cintra
2024-02-27