coq-hol-light

Notoriété 21 %

Le projet coq-hol-light est une bibliothèque Coq contenant une traduction automatique de la bibliothèque HOL-Light, utilisant hol2dk et lambdapi. Cette bibliothèque fournit des axiomes pour les théorèmes traduits, permettant une vérification rapide dans Coq. Elle vise à fournir une bibliothèque directement utilisable dans Coq, alignant les fonctions et prédicats HOL-Light sur ceux définis dans la bibliothèque standard Coq.

Dépôt de code

https://github.com/Deducteam/coq-hol-light (nouvelle fenêtre)9 étoiles

Cas d'utilisation métiers

Preuve automatique de théorèmes mathématiques
Vérification de preuves dans Coq
Traduction de bibliothèques logicielles formelles

Organisation

Administration centrale
- Gouvernement (Premier ministre et ministères)
  - Ministère de l’Enseignement supérieur, de la Recherche et de l'Espace
    - Établissements d'enseignement supérieur et de recherche - Ministère chargé de l'Enseignement supérieur
      - École normale supérieure Paris-Saclay (organisation rattachée)

Description générée le lundi 18 mars 2024 à 09:07:50

D'autres initiatives de la même organisation

lambdapi
github.com/Deducteam/lambdapi
Logipedia
github.com/Deducteam/Logipedia
Agda2Dedukti
github.com/Deducteam/Agda2Dedukti
Zenon Modulo
github.com/Deducteam/zenon_modulo