Certifying the Fast Fourier Transform with Coq

Venanzio Capretta. Certifying the Fast Fourier Transform with Coq. In Richard J. Boulton, Paul B. Jackson, editors, Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Edinburgh, Scotland, UK, September 3-6, 2001, Proceedings. Volume 2152 of Lecture Notes in Computer Science, pages 154-168, Springer, 2001. [doi]

@inproceedings{Capretta01,
  title = {Certifying the Fast Fourier Transform with Coq},
  author = {Venanzio Capretta},
  year = {2001},
  url = {http://link.springer.de/link/service/series/0558/bibs/2152/21520154.htm},
  researchr = {https://researchr.org/publication/Capretta01},
  cites = {0},
  citedby = {0},
  pages = {154-168},
  booktitle = {Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Edinburgh, Scotland, UK, September 3-6, 2001, Proceedings},
  editor = {Richard J. Boulton and Paul B. Jackson},
  volume = {2152},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-42525-X},
}