ACL2 Seminar, Nov. 3, 2017

Mertcan Temel

DFT and FFT implementations and proofs using ACL2

Abstract:

We will give ACL2 implementations for discrete Fourier transform (DFT)
and and fast Fourier transform (FFT), and some examples of ACL2 proofs
about these functions. We will show that inverse-DFT of DFT of a
vector gives the vector itself. Additionally, we will give the ACL2
proof to show that decimation-in-time FFT implementation is equivalent
to DFT.