L’INTELLIGENCE SCIENTIFIQUE AU CŒUR D’UN MONDE NUMÉRIQUE
MENU
« Fiabiliser logiciels et mathématiques grâce à la preuve assistée par ordinateur. »
Rattachée au Laboratoire des Sciences du Numérique de Nantes, LS2N, cette équipe participe à l’ambition du laboratoire de structurer la recherche numérique en Pays de la Loire.
Elle mobilise des compétences scientifiques de haut niveau pour répondre aux défis scientifiques actuels en synergie avec des partenaires académiques et industriels.
Dynamique scientifique de l’équipe
Structuration par pôles
Science du Logiciel et des Systèmes Distribués – SLSExploiter la puissance des sciences du logiciel et des systèmes distribués pour une informatique durable, sûre et ouverte.
Composante(s) d’expertise associée(s) à l’équipe
Les équipes du pôle :
Périmètre scientifique de l’équipe
Objectifs Scientifiques
Équipe-projet commune Inria et LS2N, Gallinette a pour ambition de développer une nouvelle génération d’assistants à la preuve, avec la conviction que les expérimentations pratiques doivent aller de pair avec des investigations fondamentales autour de la correspondance de Curry-Howard. Une approche distinctive consiste à implémenter de nouveaux paradigmes de programmation et logiques au-dessus du démonstrateur Rocq en le considérant comme un langage cible pour la compilation.
Domaines d’application
- Logiciels sûrs et certifiés,
- Mathématiques formalisées,
- Développement logiciel assisté par IA de confiance (Trusted AI-assisted software development / Trusted Vibe Coding).
Plateformes logicielles et matérielles
Logiciels
ROCQ PROVER
Rocq Prover est un démonstrateur de théorèmes interactif, un assistant de preuve.
Rocq Prover fournit aux utilisateurs un langage formel pour l’écriture de définitions mathématiques, d’algorithmes exécutables et de théorèmes.
Il propose un environnement pour le développement semi-interactif de preuves, vérifiées par la machine.