Accueil

webTV

Lecture

Conférence éthique et intelligence artificielle : Elise Berlinski

Lecture

Certificat exécutif : digital native, 3 questions à...

Lecture

Carlos Adrian Correa Florez, MINES ParisTech PhD, PERSEE center

Lecture

Certificat exécutif : digital native, 3 questions à...

Lecture

Lancement de la Chaire industrielle ANR TOPAZE

+ TOUS

contact

Retrouvez nos coordonnées
sur la page
Informations pratiques

Actualité de la délégation de Fontainebleau

Retrouvez toutes les actualités et faits marquants ...

Formation

Recherche

14/03/2016

jsCoq, ou Coq dans un navigateur

jsCoq, ou Coq dans un navigateur

Dans le cadre du projet FEEVER, le Centre de recherche en informatique (CRI) de MINES ParisTech travaille à l'utilisation pour l'informatique musicale de l'assistant Coq de preuves développé par Inria. Le but est de pouvoir profiter de cet outil d'aide à la preuve de propriétés mathématiques, utilisé dans les milieux académique et industriel, pour s'assurer de la correction de programmes de traitement du signal audionumérique, en particulier ceux écrits dans le langage Faust développé à Grame. Afin de faciliter l'accès à la plateforme Coq, le CRI a développé jsCoq, qui permet de réaliser des documents interactifs contenant à la fois textes, programmes et preuves en Coq et qui sont exécutés automatiquement par le navigateur.

Dans la copie d'écran suivante, tirée d'une session utilisant jsCoq, on voit un document multimédia réalisé avec ce nouvel outil et donc disponible directement dans n'importe quel navigateur. Il traite de la manipulation de signaux, et en particulier de la preuve que l'opération de décalage sur signaux est une bijection, et donc une injection. Dans un même écran, on peut donc inclure à la fois du texte, des formules mathématiques, du graphisme et des extraits de programme Coq, avec leurs preuves ; dans le cas présent, celles-ci sont exprimées en ssreflect, et mobilisent deux panneaux (à gauche, avec spécification et preuve, et à droite, avec l'étape actuelle de déroulement de celle-ci). À noter que l'utilisateur peut exécuter pas-à-pas la preuve des théorèmes et lemmes.

Notre outil a reçu un accueil enthousiaste de la communauté des utilisateurs de Coq, qui l'a adopté immédiatement à des fins d'enseignement.


jsCoq est disponible sur github (ou ici, pour des versions prêtes à l'emploi). Une démo peut être visualisée ici.

jsCoq, ou Coq dans un navigateur - MINES ParisTech

Actualité de la délégation de Fontainebleau - MINES ParisTech
Partager

actualité

Le Rapport d'activité 2020 est en ligne

Formation Le Rapport d'activité 2020 est en ligne Image de couverture du RA 2020, inspirée par des recherches du…
> En savoir +

Une santé de fer !<br>
Minéraux et santé, de l'Antiquité à nos jours

Formation Une santé de fer ! Minéraux et santé, de l'Antiquité à… Oeuvre originale d'Alice Besson-Léaud et Constance de…
> En savoir +

Pourquoi éclipser le solaire ?

Formation Pourquoi éclipser le solaire ? Philippe Blanc : « rétablir certaines vérités sur le…
> En savoir +

DigiTraining lance un appel aux musées européens

International DigiTraining lance un appel aux musées européens DigiTraining veut mettre les nouvelles technologies au…
> En savoir +

EcorcAir et les platanes du Quartier latin

Formation EcorcAir et les platanes du Quartier latin Prélèvement d'écorces de platane par Christine Franke, pilote du…
> En savoir +

Rentrée 2021 du MS MSIT (Mines - Dauphine)

Formation Rentrée 2021 du MS MSIT (Mines - Dauphine) 2o ans d'expérience et un nouveau départ pour le MS…
> En savoir +

+ Toutes les actualités

agenda

Le 30 septembre 2021 Scénarios d'une France « renouvelable »

Le 23 septembre 2021 Poésie des pierres

Du 15 septembre au 14 octobre 2021 Festival Musique aux Mines

Du 20 juillet 2021 au 3 janvier 2022 Rentrée 2021 - 2022

+ Tous les événements

Plan du site
Contacts Mentions légales efil.fr © 2014 MINES ParisTech