Bienvenue aux Mines Paristech
Bienvenue à MINES ParisTech
Newsletter International
Website
Théorie & Pratique
Vous êtes

rechercher
une actualité

Ecole
Entreprise
Formation
International
Recherche
Sciences de la terre et
de l'environnement
Energétique et procédés
Mécanique et matériaux
Mathématiques et systèmes
Economie, management
et société
Partager

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

agenda

Du 10 septembre au 27 novembre 2018 Mooc Conversion thermodynamique de la…

Du 18 septembre au 14 décembre 2018 Musique aux Mines 2018

Du 1 octobre 2018 au 31 janvier 2019 Mai 68 aux Mines

Du 1 octobre au 10 décembre 2018 MOOC - Problèmes Énergétiques Globaux

Du 22 octobre au 3 décembre 2018 Mooc Conversion thermodynamique de la…

+ Tous les événements

webTV

Lecture

Séminaire PSL - Écosystèmes de médias I Session 4 Partie 4

Lecture

Séminaire PSL - Écosystèmes de médias I Session 4 Partie 2

Lecture

Séminaire PSL - Écosystèmes de médias I Session 4 Partie 3

Lecture

Séminaire PSL - Écosystèmes de médias I Session 4 Partie 1

Lecture

Lancement de la Chaire DEEP unissant HUTCHINSON, l'ESPCI et MINES ParisTech

+ Toutes les vidéos

actus / Sciences de la terre et l'environnement

Consulter les actus de cette thématique

actus / Énergétique et procédés

Consulter les actus de cette thématique

actus / Mécanique et matériaux

Consulter les actus de cette thématique

actus / Mathématique et systèmes

Consulter les actus de cette thématique

actus / Économie, management et société

Consulter les actus de cette thématique
Plan du site
MINES
ParisTech

60, Boulevard Saint-Michel
75272 PARIS Cedex 06
Tél. : +33 1 40 51 90 00

Implantations
Formation
Mentions légales | efil.fr | ©2012 MINES ParisTech | +33 1 40 51 90 00 |