Présentation de Coq

Nantes, France

Bummer! Sales have ended.

Unfortunately, tickets for this event are no longer on sale.

View upcoming events Create an event

Event Details

Coq, un assistant de preuves formelles.

En quelques mots, Coq permet de définir des objets mathématiques à l'aide
du langage Gallina (qui est purement fonctionnel). Ces objets peuvent
globalement prendre la forme de types, fonctions ou propositions
mathématiques. Dans un deuxième temps, Coq permet, à l'aide d'un
environnement de démonstration bien fourni, d'effectuer la preuve des
diverses propositions que vous avez avancées.

L'utilisation de Coq peut aller très loin. On peut notamment s'en servir
pour prouver des programmes impératifs à l'aide de logique de Hoare par
exemple [2]. Il a aussi permis la démonstration de certains théorèmes, donc
le plus célèbre est le théorème des quatre couleurs [3].

Son lien étroit avec la programmation fonctionnelle, outre le langage
Gallina, se situe au niveau d'une notion qu'on appelle l'isomorphisme de
Curry-Howard, qui stipule la présence d'une correspondance entre preuve et
fonction mathématique. Cette correspondance est un peu subtile, mais je
vous propose de la découvrir au terme de cette séance, ou d'une seconde
séance si nécessaire.