LiberAbaci
Enseigner les mathématiques à l'aide de Coq
LiberAbaci est un projet collaboratif visant à améliorer
l'accessibilité du système de preuve interactif Coq pour un
public d'étudiants en mathématiques dans les premières années
universitaires.
Evénements et résultats notables
Réunion de lancement
La réunion de lancement a eu lieu le 20 septembre 2022 dans les
locaux de l'Inria Paris. Le programme
de cette réunion permet
d'avoir accès aux présentations qui ont été faites.
Tâches
Tâche 1 : Collaborations avec des enseignants
Nous cherchons à établir des contacts avec des enseignants en mathématique et des chercheurs en didactique.
Page dédiée
Tâche 2 : Fondements de la théorie des types
Tâche 3 : Structures, inférence et hiérarchies
Tâche 4 : Notations extensibles et langage de surface
Cette tâche cherche à expérimenter de nouveaux mécanismes de notations et de langage de preuve,
afin de se rapprocher autant que possible des notations usuelles dans un cours de mathématique.
Page dédiée
Tâche 5 : Traitements automatiques
Tâche 6 : Environnements interactifs
Tâche 7 : Création de bibliothèque sur des domaines précis
Mettre à jour cette page
Les instructions sont
disponibles ici.