Accéder directement au contenu Accéder directement à la navigation
Communication dans un congrès

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.
Type de document :
Communication dans un congrès
Liste complète des métadonnées

Littérature citée [17 références]  Voir  Masquer  Télécharger

https://hal-mines-paristech.archives-ouvertes.fr/hal-01251147
Contributeur : Claire Medrala <>
Soumis le : mardi 5 janvier 2016 - 16:44:26
Dernière modification le : jeudi 24 septembre 2020 - 16:36:02
Archivage à long terme le : : jeudi 7 avril 2016 - 15:30:56

Fichier

A-624.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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⟩

Partager

Métriques

Consultations de la notice

200

Téléchargements de fichiers

97