Sites Inria

English version

Equipe de recherche COQ

Spécifications et preuves de programmes

  • Responsable : Christine Paulin-mohring
  • Centre(s) de recherche : CRI de Paris
  • Domaine : Génie logiciel et calcul symbolique
  • Thème : Sémantique et programmation

Présentation de l'équipe

L'objectif du projet Coq est l'élaboration d'un langage et d'un environnement pour développer des preuves formelles. Cet environnement est destiné au développement et à la certification de logiciels zéro défaut dans les domaines sécuritaires (logiciels embarqués, protocoles de communication, commerce électronique, etc.).

Le projet développe un environnement (Coq) permettant de construire interactivement des spécifications et des preuves. Il repose sur un langage issu de la théorie des types. Dans ce langage, les fonctions sont représentables par des algorithmes, les prédicats peuvent être définis inductivement par un ensemble de clauses et les preuves sont des objets.

Coq a été un projet commun avec le Laboratoire de l'Informatique du Parallélisme (URA CNRS 1398) de l'École Normale Supérieure de Lyon de janvier 1994 à septembre 1997. Il est en instance de devenir un projet commun avec le Laboratoire de Recherche en Informatique (URA CNRS 410) de l'université Paris Sud.

Axes de recherche

  • Élaboration de concepts de haut-niveau dans les langages de preuve : modules, sous-typage, définitions par filtrage, structures infinies.
  • Représentation interne des termes de preuve rendant efficace les opérations de réduction et de démonstration.
  • Développement de théories classiques des mathématiques et de programmes certifiés (en particulier le noyau du système Coq).

Relations industrielles et internationales

  • Participation au working group " Types " dans le programme Esprit LTR.
  • Participation à l'action Génie Dassault-INRIA sur la technologie de preuves de programmes.
  • Collaboration avec le centre de recherche Bull sur les preuves de protocole au sein du GIE Dyade.
  • Collaboration avec le Cnet-Lannion sur la mécanisation des preuves.
  • Participation a l'action incitative CFC-Calcul Formel Certifie.

Mots-clés : Typage Logique Calcul formel Lambda-calcul Langage fonctionnel Spécification formelle Preuve de programme Synthèse de programme Déduction automatique Protocole sécuris&eacu

Suivez Inria