digger

Outil permettant de convertir du code Coq écrit dans un style impératif en code C ou en une représentation intermédiaire sous forme de code Coq. Il utilise une extraction interne pour obtenir le code Coq sous forme de JSON.

Dépôt de code

https://gitlab.univ-lille.fr/2xs/digger (nouvelle fenêtre)

Cas d'utilisation métiers

Preuve automatique de théorèmes mathématiques : rechercher des initiatives proches
Analyse de code Coq écrit en style impératif : rechercher des initiatives proches
Génération de code C à partir de preuves formelles : 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
    - Universités - Ministère chargé de l'Enseignement supérieur
      - Université de Lille (organisation rattachée)

Outil utilisé

JSON : voir les initiatives de ses organisations qui l'ont aussi

Description générée le lundi 18 mars 2024 à 10:53:07

D'autres initiatives de la même organisation

www.univ-lille.fr
powerapi
github.com/powerapi-ng/powerapi
pyRAPL
github.com/powerapi-ng/pyRAPL
pyJoules
github.com/powerapi-ng/pyJoules