La preuve de théorèmes pour les masses (soniques)

Emilio Jesús Gallego Arias (1, 2) , Benoît Pin (1, 2) , Pierre Jouvelot (1, 2)

1 Mines Paris - PSL (École nationale supérieure des mines de Paris)
2 CRI - Centre de Recherche en Informatique

Après avoir motivé la nécessité d’introduire des outils interactifs pour l’enseignement en informatique musicale et, plus généralement, dans les disciplines scientifiques, nous décrivons jsCoq, notre nouvelle interface utilisateur pour le logiciel de preuve mathématique Coq. Cet outil fournit aux enseignants un moyen efficace pour concevoir et mettre en œuvre des cours qui combinent textes, audio, images et preuve interactive de théorèmes. Nous présentons deux études de cas d’utilisation dans le domaine audio et les résultats d’une évaluation de jsCoq sur le terrain.

Mots clés: pédagogie interactive; documents hybrides; preuve de théorèmes; Coq.

Domaines: Informatique [cs]; Son [cs.SD]; Traitement du signal et de l'image [eess.SP]

Emilio Jesús Gallego Arias, Benoît Pin, Pierre Jouvelot. La preuve de théorèmes pour les masses (soniques). Revue Francophone d'Informatique et Musique, 2018, N°6, 14 p. ⟨hal-01877004⟩