Actualités / Introduction / Oratrices et orateurs / Comité d'organisation / Planning et détails
À l'occasion des JNIM 2024, nous organisons une demi-journée thématique sur les assistants de preuve, à Grenoble le 19 mars 2024.
Cette demi-journée, sur la thématique des assistants de preuve, vise à partir des aspects mathématiques (logiques et algébriques) de la théorie des types pour aller jusqu'à la formalisation des mathématiques et l'usage des assistants dans l'enseignement des mathématiques et de l'informatique.
La demi-journée sera principalement centrée sur l'assistant de preuve Coq (https://coq.inria.fr) mais présentera plus largement un panorama des différents assistants de preuve pour aller. Le sujet a acquis une maturité et une diffusion qui conduit à en faire une thématique inévitable pour l'IM, dans les liens qu'elle entretient en amont comme en aval entre informatique et mathématiques. Pour citer quelques uns des principaux faits marquants de la dernière décennie, on retiendra pêle-mêle:
La pertinence de la thématique pour le GDR-IFM tient aussi au fait que les interactions entre mathématiques et informatique y prennent des formes multiples: des fondements mathématiques de ces logiciels (théorie de la démonstration, théorie de l'homotopie, …) à ses applications comme outil servant à la production ou à la certification de mathématiques mais également comme outil pour un enseignement en mathématiques ou informatique, tout en entretenant une interaction riche avec des problématiques technologiques.
En cela, la demi-journée thématique a pour objectif d'illustrer plusieurs des dynamiques entre mathématiques et informatique qui sont à l’oeuvre dans le GDR (c’est ce qui explique d'ailleurs que, si la proposition de demi-journée émane du GT Scalp, le thème concerne directement d'autres groupes de travail du GDR, comme LHC, ARITH et Vérif notamment).
L'équipe INRIA Picube sur laquelle s'appuie principalement l'organisation de la journée est directement impliquée dans ces différents aspects; le comité d'organisation comporte en outre des membres proches, complétant les expertises. Par ailleurs, les organisatrices et organisateurs sont impliqués dans le défi Liberabaci, une action entre les équipes INRIA qui contribuent à Coq, visant à développer des contenus pédagogiques en Coq couvrant les premières années de Licence de mathématiques.
Pour une prise en main rapide d'un assistant de preuve avec un objectif d'enseignement, on recommande de tester Software Foundations avec jscoq qui permet d'exécuter directement dans un navigateur cette série de cours d'informatique intégralement formalisés en Coq, sous forme de scripts Coq à compléter, qui est largement diffusée et utilisée aux États-Unis (le livre original est ici).
Voici des liens vers quelques références ou ressources citées lors de la demi-journée: