Revisiting the Fast Fourier Transform in Rocq
arXiv:2210.05225
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.