STTfaXport

Notoriété 10 %

STTfaXport est un outil permettant d'exporter des théories écrites dans le langage de déduction Dedukti vers d'autres assistants de preuve en utilisant l'encodage de STTfa. Il nécessite OCaml, Dedukti et dune pour fonctionner.

Dépôt de code

https://github.com/Deducteam/sttfaxport (nouvelle fenêtre)2 étoiles

Cas d'utilisation métiers

Traduction de fichiers dans le format d'encodage de STTfa vers Coq : rechercher des initiatives proches
Exportation de théories écrites en Dedukti vers d'autres assistants de preuve : rechercher des initiatives proches

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 : voir les initiatives de ses organisations qui l'ont aussi

Description générée le lundi 18 mars 2024 à 20:48:12

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