Preuve mécanisée

Mots-clés

• preuve automatique
• preuve interactive
• interopérabilité des systèmes de preuve
• cadres logiques
• vérification croisée
• Dedukti
• LambdaPi

Description

Cette équipe regroupe les concepteurs des outils de preuve mécanisée, des systèmes eux-mêmes jusqu'aux bibliothèques, assurant ainsi un continuum. Elle s'organise en trois axes :

1. la conception et le développement de systèmes de preuves, notamment :
   • la conception du formalisme du λΠ-calcul modulo théories, mis en pratique à travers du vérificateur de preuves Dedukti et de l'assistant de preuve LambdaPi
   • la participation au développement de l'assistant de preuve Isabelle
   • la participation au développement de la Méthode B et Event-B
2. l'interopérabilité entre systèmes de preuves, par la conception, l'utilisation et la transformation de certificats de preuve
3. le développement de bibliothèques et formalisations pour des thématiques variées :
   • pour les données
   • pour les mathématiques
   • pour la preuve de programmes

Logiciels

Publications

Liste complète sur HAL : https://hal.science/LMF-PM

Séminaires, groupes de travail

• Séminaire Deducteam régulier le jeudi après-midi

Projets

Members

Permanent

PhD Students

PostDoc