Skip to Main content Skip to Navigation
Conference papers

Adventures in the (not so) Complex Space

Abstract : We report on the progress of a constructive mechanization for a small subset of signal processing theory, built upon the SSREFLECT and MATHCOMP libraries. The development was started to provide mechanized semantics for audio programming languages. Currently, we have formalized several standard properties of the Discrete Fourier Transform, such as its unitary matrix form and its power and convolution theorems. Future goals include transfer functions and constant overlap-add processing. At the workshop, we aim to discuss the needs and limits of our current approach, surveying some mathematical concepts not covered by existing libraries, and similar efforts in other frameworks and theorem provers.
Document type :
Conference papers
Complete list of metadatas

Cited literature [17 references]  Display  Hide  Download

https://hal-mines-paristech.archives-ouvertes.fr/hal-01251147
Contributor : Claire Medrala <>
Submitted on : Tuesday, January 5, 2016 - 4:44:26 PM
Last modification on : Thursday, September 24, 2020 - 4:36:02 PM
Long-term archiving on: : Thursday, April 7, 2016 - 3:30:56 PM

File

A-624.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01251147, version 1

Citation

Emilio Jesús Gallego Arias, Pierre Jouvelot. Adventures in the (not so) Complex Space . The 7th Coq Workshop, Jun 2015, Sophia Antipolis, France. ⟨hal-01251147⟩

Share

Metrics

Record views

201

Files downloads

100