@Inbook{Good1997,
author="Good, I. J.",
editor="Kotz, Samuel
and Johnson, Norman L.",
title="Introduction to Cooley and Tukey (1965) An Algorithm for the Machine Calculation of Complex Fourier Series",
bookTitle="Breakthroughs in Statistics",
year="1997",
publisher="Springer New York",
address="New York, NY",
pages="201--216",
abstract="Fourier (frequency) analysis is important in statistics, mathematics, and all the hard sciences (as in x-ray crystallography), and in signal processing, so Fast Fourier Transforms (FFTs) are widely applicable. For example, Costain (1974) said the FFTs are regarded as an economic breakthrough in geo­physics, especially in seismology.",
isbn="978-1-4612-0667-5",
doi="10.1007/978-1-4612-0667-5_9",
url="https://doi.org/10.1007/978-1-4612-0667-5_9"
}


@book{10.5555/1614191,
author = {Cormen, Thomas H. and Leiserson, Charles E. and Rivest, Ronald L. and Stein, Clifford},
title = {Introduction to Algorithms, Third Edition},
year = {2009},
isbn = {0262033844},
publisher = {The MIT Press},
edition = {3rd},
abstract = {If you had to buy just one text on algorithms, Introduction to Algorithms is a magnificent choice. The book begins by considering the mathematical foundations of the analysis of algorithms and maintains this mathematical rigor throughout the work. The tools developed in these opening sections are then applied to sorting, data structures, graphs, and a variety of selected algorithms including computational geometry, string algorithms, parallel models of computation, fast Fourier transforms (FFTs), and more. This book's strength lies in its encyclopedic range, clear exposition, and powerful analysis. Pseudo-code explanation of the algorithms coupled with proof of their accuracy makes this book is a great resource on the basic tools used to analyze the performance of algorithms.}
}

@misc{cryptoeprint:2016/504,
      author = {Patrick Longa and Michael Naehrig},
      title = {Speeding up the Number Theoretic Transform for Faster Ideal Lattice-Based Cryptography},
      howpublished = {Cryptology ePrint Archive, Paper 2016/504},
      year = {2016},
      note = {\url{https://eprint.iacr.org/2016/504}},
      url = {https://eprint.iacr.org/2016/504}
}

@inproceedings{NipkowEH-ATVA20,
author = {Tobias Nipkow and Manuel Eberl and Maximilian P. L. Haslbeck},
title = {Verified Textbook Algorithms. {A} Biased Survey},
booktitle = {ATVA 2020, Automated Technology for Verification and Analysis},
editor = {Dang Van Hung and Oleg Sokolsky},
publisher = {Springer},
series = {LNCS},
volume = {12302},
pages = {25-53},
year =2020,
note = {Invited paper}
}

@misc{ntt_intro,
 author = {Nayuki},
 title = {Number-theoretic transform (integer DFT)},
  year = {2022},
 howpublished = {\url{https://www.nayuki.io/page/number-theoretic-transform-integer-dft}}
}

@misc{funalgs,
author ="{Tobias Nipkow, Jasmin Blanchette, Manuel Eberl, Alejandro Gómez-Londoño, Peter Lammich, Christian Sternagel, Simon Wimmer, Bohua Zhan}",
title = {Functional Algorithms, Verified!},
year = 2021,
howpublished = {\url{https://functional-algorithms-verified.org/}}
}

@article{FFT-AFP,
  author  = {Clemens Ballarin},
  title   = {Fast Fourier Transform},
  journal = {Archive of Formal Proofs},
  month   = {October},
  year    = {2005},
  note    = {\url{https://isa-afp.org/entries/FFT.html},
            Formal proof development},
  ISSN    = {2150-914x},
}

@article{Dirichlet_Series-AFP,
  author  = {Manuel Eberl},
  title   = {Dirichlet Series},
  journal = {Archive of Formal Proofs},
  month   = {October},
  year    = {2017},
  note    = {\url{https://isa-afp.org/entries/Dirichlet_Series.html},
            Formal proof development},
  ISSN    = {2150-914x},
}


