Home » Liste des logiciels par équipes


Equipe Gallinette

NomDépôtPropriétéLicenceNbre de
téléchargement
DescriptionLien
CoqInriaopen 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)Inriaopen 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.

Haut de page


Copyright : LS2N 2017 - Mentions Légales - 
 -