Equipe Gallinette
| Nom | Dépôt | Propriété | Licence | Nbre de téléchargement | Description | Lien |
| Coq | Inria | open source LGPL-2.1 | 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... | |||
| M-Comp (Math-Components) | Inria | open source CeCILL-B | Mathematical Components library La bibliothèque Mathematical Components est un ensemble de bibliothèques Coq couvrant les prérequis pour la vérification du théorème de l'ordre impair. |
