Calcul et calcul formel dans un assistant à la preuve.

Une des spécificités du système Coq est la place que la notion de calcul occupe dans le formalisme logique sous-jacent à cet assistant à la preuve. Une conséquence en est que l'on dispose dans ce système d'un véritable langage de programmation fonctionnel, qui peut être utilisé pour modéliser mais aussi pour exécuter (relativement efficacement) des programmes, garantissant ainsi la correction des valeurs calculées. Cette utilisation du calcul, combinée avec le développement récent d'un nombre substantiel de bibliothèques de mathématiques formalisées, est particulièrement propice à l'implémentation et à la certification en Coq d'algorithmes issus du calcul formel. Dans cet exposé, après une brève introduction au système, et aux techniques pour exploiter cette place du calcul dans les preuves formelles, nous proposerons un tour (nécessairement non exhaustif) de quelques expériences en cours autour du mariage entre preuves formelles et calcul formel. Cet exposé ne présuppose aucune connaissance de Coq ou de culture en théorie des types.

---

Virginie Collette
Last modified: Tue Jan 31 11:32:50 CET 2012