Equipe / Team : Gallinette
Participants : Matthieu Sozeau, Pierre-Marie Pédrot, Gaëtan Gilbert
Licence : open source LGPL-2.1
Mots clés : Preuve , Certification , Formalisation
Résumé :
Un assistant de preuve interactif pour la formalisation mathématique et la preuve de programmes.
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...
