The formalization of discrete Fourier transform in HOL
From MaRDI portal
Publication:1666338
DOI10.1155/2015/687152zbMath1394.68353OpenAlexW1880321261WikidataQ59118930 ScholiaQ59118930MaRDI QIDQ1666338
Jie Zhang, Liming Li, Yong Guan, Zhiping Shi, Yu-Peng Zhang
Publication date: 27 August 2018
Published in: Mathematical Problems in Engineering (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1155/2015/687152
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (1)
Uses Software
Cites Work
- Constructing the real numbers in HOL
- Formalization of function matrix theory in HOL
- Formal reasoning about finite-state discrete-time Markov chains in HOL
- Formal Methods in Computer-Aided Design
- The correctness of the fast Fourier transform: A structured proof in ACL2
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: The formalization of discrete Fourier transform in HOL