Réunion de lancement Liber Abaci

Cette réunion de lancement a eu lieu le 20 septembre 2022 à l'Inria Paris

Programme

• 10:00-11:10 Accueil et présentation générale du défi (Y. Bertot) interventions de J.-F. Gerbeau.
• 11:10-11:40 : Tâche 1 Collaborations avec des enseignants en mathématiques
  Exposé de Pierre Rousselin, Université de Paris 13: expérience avec des étudiants de L1
• 11:40-13:30 Pause déjeuner
• 13:30-14:00 : Tâche 2 Fondements de la théorie des types
  Exposé de Matthieu Sozeau, Multiverses for a more math-friendly proof assistant
• 14:00-14:30 : Tâche 3 Primitives de structuration et d'héritage
  Exposé de Cyril Cohen Structurer les mathématiques, des primitives aux fonctionnalités, fichiers d'exemples demo.v et sets.v
• 14:30-15:00 : Tâche 4 Notations extensibles et langage de surface
  Exposé d'Arthur Charguéraud: Expérience avec des notations évoluées dans le cadre d'un stage étudiant
15:00-15:30Pause
• 15:30-16:00 : Tâche 6 Environnements de travail interactifs
  Exposé de Emilio Jesús Gallego Arias: lessons learned with JSCoq and perspectives on User-Interfaces
• 16:00-16:30 : Tâche 7 Contenus éducatifs sur des domaines précis
  Exposé de Sylvie Boldo: La bibliothèque coq-num-analysis
• 16:30-17:00 : Discussion Voir les notes de la réunion.