Logiciels autour de Dedukti et LambdaPi
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 :
- 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
- l'interopérabilité entre systèmes de preuves, par la conception, l'utilisation et la transformation de certificats de preuve
- 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
Formalisation autour des données en Coq
Bibliothèques pour la preuve de programmes
Plateforme pour le test et la preuve de programmes C en Isabelle
Bibliothèque universelle de preuves
Outils de vérification de preuves automatiques et d'automatisation pour Coq
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
Assistants de preuve basés sur la théorie des ensembles interopérables et sûrs
Réseau de Recherche Européen sur les Preuves Formelles
Members
Permanent
PhD Students
Luc Chabassier
Xavier Denis
Houda MOUHCINE
Melanie Taprogge
PostDoc
Alidra Abdelghani
Anthony Bordg
Matteo Manighetti