Nantes Functional Programming Group Archive Categories Tags

Présentation de Coq, un assistant de preuves formelles.

Maxime présentera Coq le 27 novembre, à partir de 19h30.

Inscrivez-vous sur EventBrite http://nantesfp-coq.eventbrite.com/

Quand : 27/11/2012 de 19h30 à 21h00 (voire plus, autour d’une bière).

: La Cantine, Impasse Juton, 44000 Nantes

Coq

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. 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.

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.

Fork me on GitHub