predicativize

Notoriété 19 %

Predicativize is a tool used to translate proofs from an impredicative type system to a predicative one. It was used to translate Matita's arithmetic library to Agda, and can be used with Dedukti to translate other libraries as well.

Dépôt de code

https://github.com/Deducteam/predicativize (nouvelle fenêtre)8 étoiles

Cas d'utilisation métiers

Facilitation of proof sharing between different systems : rechercher des initiatives proches
Translation of proofs from impredicative to predicative systems : rechercher des initiatives proches

Cas d'utilisation fonctionnel

Utilise de l'intelligence artificielle : voir les initiatives de ses organisations qui l'ont aussi

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 mardi 19 mars 2024 à 20:11:29

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