This event has ended

Présentation de Coq

Clément Delafargue

Tuesday, November 27, 2012 from 7:30 PM to 11:00 PM (CET)

Nantes, France

Présentation de Coq

Ticket Information

Type End     Quantity
Ticket Ended Free  

Who's Going

Loading your connections...

Share Présentation de Coq

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.

Have questions about Présentation de Coq? Contact Clément Delafargue

When & Where



La cantine
Impasse Juton
44000 Nantes
France

Tuesday, November 27, 2012 from 7:30 PM to 11:00 PM (CET)


  Add to my calendar

Please log in or sign up

In order to purchase these tickets in installments, you'll need an Eventbrite account. Log in or sign up for a free account to continue.