CoqInE

Notoriété 22 %

CoqInE est un plugin pour le logiciel Coq qui traduit les preuves Coq en termes Dedukti vérifiables. Il fournit un fichier de signature fidèlement encodant la théorie sous-jacente de Coq. La sortie générée est destinée à être vérifiable à l'aide de la dernière version de Dedukti.

Dépôt de code

https://github.com/Deducteam/CoqInE (nouvelle fenêtre)11 étoiles

Cas d'utilisation métiers

Encodage de la théorie sous-jacente de Coq
Prise en charge de la polymorphie d'univers de Coq
Traduction de preuves Coq en termes Dedukti

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)

Outil utilisé

OCaml

Description générée le mardi 19 mars 2024 à 15:43:53

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