Accéder directement au contenu Accéder directement à la navigation
Pré-publication, Document de travail

Bringing Theorem Proving to the (sonic) Masses

Abstract : We explore the intersection of interactive theorem proving and digital signal processing through the use of web-based, rich interfaces. Traditionally, the barrier to entry to interactive theorem proving has been high. Provers are complex systems using obscure programming languages, and libraries may be underdocumented and use formalisms and notations far from the standard domain-specific practice. Thus, it doesn't come at a surprise that interactive theorem proving has seldom been explored in the the digital signal processing community. In previous work [1,2], we formalized several DSP tools and concepts using the Coq theorem prover [3]. [1] presents a simplified model Faust [4], a programming language tailored to audio DSP. The formalization allows to reason about Faust programs and prove typical properties like filter stability. In [2], we mechanized some theory of the Discrete Fourier Transform, following [5], and proving the main theorems. In our opinion, both developments are suitable as teaching material, either as an introduction to theorem proving or to students interested in DSP theory. However, in their current form, the student or reader must work with two versions of the document. The paper-and-ink version: which misses the interactive component of the theorem proving process, and the Coq proof scripts, that being plain text files usually miss convenient formatting and structure. This problem is also common in other teaching material (see for instance [6]), and while efforts to improve this situation have been made ([7] is one of the latest), the situation is still far from optimal, as most initiatives have been limited by implementation and platform choices. Our take on the problem --- inspired by the long tradition of interactive documents found in the computer music domain --- is to enrich the Coq document model to the full power of HTML5. Our goal is to have an integral solution, free of external components, so we have ported Coq to javascript, and we are writing a custom IDE for enriched proof documents. Thus, the once painful Coq installation and setup has become now a page load in the browser, document navigation and interaction can take advantage of browser support, and our documents can take advantage of most available JS libraries for extensibility. For instance, our model would allow to incorporate a javascript-based score like [8] and relate its output to a particular Coq datatype in a quite straightforward way. The primary design goal of the web-based user interface is supporting education and interactive papers, focusing on supporting excellent user feedback, comprehensive documentation search, and good notational/navigational facilities. The current prototype can be accessed at [9]. It supports full Coq functionality, but the user interface is still in heavy development. While support for the enriched document model won't likely be available at the time of this submission, the main technical difficulties of the development have been solved, thus we are confident on getting usable versions in the workshop timeframe.
Type de document :
Pré-publication, Document de travail
Liste complète des métadonnées

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

https://hal-mines-paristech.archives-ouvertes.fr/hal-01254456
Contributeur : Claire Medrala <>
Soumis le : vendredi 22 janvier 2016 - 10:25:55
Dernière modification le : mercredi 14 octobre 2020 - 03:52:20
Archivage à long terme le : : vendredi 11 novembre 2016 - 00:04:00

Fichier

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

Identifiants

  • HAL Id : hal-01254456, version 1

Citation

Emilio Jesús Gallego Arias, Benoît Pin, Pierre Jouvelot. Bringing Theorem Proving to the (sonic) Masses. 2015. ⟨hal-01254456⟩

Partager

Métriques

Consultations de la notice

218

Téléchargements de fichiers

85