Détail d'une fiche   Version PDF

COQ (SR0221NR)

Spécifications et preuves de programmes

COQ →  LOGICAL (SR0248RR)


Statut: Terminée

Responsable : Christine Paulin

Mots-clés de "A - Thèmes de recherche en Sciences du numérique - 2023" : Aucun mot-clé.

Mots-clés de "B - Autres sciences et domaines d'application - 2023" : Aucun mot-clé.

Domaine : Génie logiciel et calcul symbolique
Thème : Sémantique et programmation

Période : 01/01/1993 -> 31/12/2000
Dates d'évaluation :

Etablissement(s) de rattachement : <sans>
Laboratoire(s) partenaire(s) : <sans UMR>

CRI : Centre Inria de Paris
Localisation : Rocquencourt
Code structure Inria :

Numéro RNSR : 199322064T
N° de structure Inria: SR0221NR

Présentation

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.