Coq

Notoriété 72 %

Coq est un système de gestion de preuves formelles. Il fournit un langage formel pour écrire des définitions mathématiques, des algorithmes exécutables et des théorèmes, ainsi qu'un environnement pour le développement semi-interactif de preuves formelles vérifiables par machine.

Dépôts de code

https://github.com/coq/coq (nouvelle fenêtre)4 997 étoiles
https://github.com/coq/coq.github.io (nouvelle fenêtre)
https://github.com/coq/opam (nouvelle fenêtre)133 étoiles

Cas d'utilisation métiers

Création de théorèmes et preuves formelles
Développement d'algorithmes exécutables et vérifiables
Vérification de preuves formelles en mathématiques

Organisation

Administration centrale
- Gouvernement (Premier ministre et ministères)
  - Ministère de l’Économie, des Finances et de la Souveraineté industrielle, énergétique et numérique
    - Organismes rattachés - Ministère chargé de l'Économie et des Finances et de la Souveraineté industrielle et énergétique
      - Institut national de recherche en informatique et en automatique (organisation rattachée)

Outils utilisés

Zulip
OCaml
GitLab CI
Discourse

Description générée le mercredi 20 mars 2024 à 10:13:02

D'autres initiatives de la même organisation

Inria
inria.fr
Insee
insee.fr
Catala
github.com/CatalaLang/catala
spoon
github.com/INRIA/spoon