Abstract
We program the Fast Fourier Transform in type theory, using the tool Coq. We prove its correctness and the correctness of the Inverse Fourier Transform. A type of trees representing vectors with interleaved elements is defined to facilitate the definition of the transform by structural recursion. We define several operations and proof tools for this data structure, leading to a simple proof of correctness of the algorithm. The inverse transform, on the other hand, is implemented on a different representation of the data, that makes reasoning about summations easier. The link between the two data types is given by an isomorphism. This work is an illustration of the two-level approach to proof development and of the principle of adapting the data representation to the specific algorithm under study. CtCoq, a graphical user interface of Coq, helped in the development. We discuss the characteristics and usefulness of this tool.
I worked on the formalization of FFT during a two-month stay at the INRIA research center in Sophia Antipolis, made possible by a grant from the Dutch Organization for Scientific Research (NWO, Dossiernummer F 62-556). I am indebted to the people of the Lemme group for their support and collaboration. In particular, I want to thank Yves Bertot for his general support and for teaching me how to use CtCoq, and Loïc Pottier for his help in formulating the Fast Fourier Transform in type theory.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Antonia Balaa and Yves Bertot. Fix-point equations for well-founded recursion in type theory. In J. Harrison and M. Aagaard, editors, Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000, volume 1869 of Lecture Notes in Computer Science, pages 1–16. Springer-Verlag, 2000.
Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Yann Coscoy, David Delahaye, Daniel de Rauglaudre, Jean-Christophe Filliâtre, Eduardo Giménez, Hugo Herbelin, Gérard Huet, Henri Laulhère, César Muñoz, Chetan Murthy, Catherine Parent-Vigouroux, Patrick Loiseleur, Christine Paulin-Mohring, Amokrane Saïbi, and Benjanin Werner. The Coq Proof Assistant Reference Manual. Version 6.3. INRIA, 1999.
G. Barthe, M. Ruys, and H. P. Barendregt. A two-level approach towards lean proof-checking. In S. Berardi and M. Coppo, editors, Types for Proofs and Programs (TYPES’95), volume 1158 of LNCS, pages 16–35. Springer, 1995.
Yves Bertot. The CtCoq system: Design and architecture. Formal aspects of Computing, 11:225–243, 1999.
Yves Bertot, Gilles Kahn, and Laurent Théry. Proof by pointing. In Symposium on Theoretical Aspects Computer Software (STACS), Sendai (Japan), volume 789 of LNCS. Springer, April 1994.
Samuel Boutin. Using reflection to build efficient and certified decision procedures. In MartÃn Abadi and Takayasu Ito, editors, Theoretical Aspects of Computer Software. Third International Symposium, TACS’97, volume 1281 of LNCS, pages 515–529. Springer, 1997.
Ana Bove and Venanzio Capretta. Nested general recursion and partiality in type theory. http://www.cs.kun.nl/venanzio/publications/nested.ps.gz, 2001.
James W. Cooley and John W. Tukey. An algorithm for the machine calculation of complex Fourier series. Mathematics of Computation, 19(90):297–301, April 1965.
Paul de Mast, Jan-Marten Jansen, Dick Bruin, Jeroen Fokker, Pieter Koopman, Sjaak Smetsers, Marko van Eekelen, and Rinus Plasmeijer. Functional Programming in Clean. Computing Science Institute, University of Nijmegen.
Ruben A. Gamboa. The correctness of the Fast Fourier Transform: a structured proof in ACL2. Formal Methods in System Design, Special Issue on UNITY, 2001. in print.
Jayadev Misra. Powerlist: a structure for parallel recursion. TOPLAS, 16(6):1737–1767, November 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Capretta, V. (2001). Certifying the Fast Fourier Transform with Coq. In: Boulton, R.J., Jackson, P.B. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2001. Lecture Notes in Computer Science, vol 2152. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44755-5_12
Download citation
DOI: https://doi.org/10.1007/3-540-44755-5_12
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42525-0
Online ISBN: 978-3-540-44755-9
eBook Packages: Springer Book Archive