Français Anglais
Accueil Annuaire Plan du site
Accueil > Production scientifique > Logiciels et brevets
Production scientifique
Logiciel Coq
Coq - L'assistant de preuve Coq
Date de dernière version : 17 février 2018

Responsable : MELQUIOND Guillaume


Coq offre tout à la fois un langage de programmation fonctionnelle à types dépendants et un formalisme logique qui, ensemble, permettent tout autant le développement de théories mathématiques que la spécification et la certification de propriétés de programmes. Coq fournit aussi un ensemble vaste et extensible de méthodes de preuve. Les programmes de Coq sont extractibles vers OCaml, Haskell, Scheme...

Pour en savoir plus: https://coq.inria.fr/

Logiciel



Activités de recherche

Membres
  FILLIÂTRE Jean-Christophe
  PAULIN-MOHRING Christine
  MELQUIOND Guillaume

Equipe
  Vérification d'Algorithmes, Langages et Systèmes

Equipe-projet Inria
  Toccata
Logiciels et brevets
DNADNA
Deep Neural Networks for DNA

TOUCHTOKENS
Low-cost Solution for Tangible Interfaces

LODATLAS
Browsing Linked Data Catalogs with LODAtlas