Dedukti : un vérificateur de preuves universel
Résumé
• Dedukti est un vérificateur de type pour λΠ-calcul modulo. • Le λΠ-calcul modulo est une extension du λ-calcul avec des types dépendants et une relation de conversion etendue par des r` egles de réécriture. • Dedukti est capable de vérifier les preuves provenant de prouveurs de théor emes (Zenon, iProver) et d'assistants de preuves (Coq, HOL, Focalize). • On montrè a travers plusieurs exemples que l'utilisation de la réécriture caractéristique du λΠ-calcul modulo permet d'obtenir des preuves plus petites et plus rapides a vérifier. Contexte et objectif Pour vérifier une preuve avec Dedukti, il faut d'abord l'exprimer dans le λΠ-calcul modulo. Pour cela, on utilise des traducteurs spécialisés : • Holide traduit les preuves de l'assistant de preuve HOL Light. • Coqine traduit les preuves de l'assistant de preuve Coq. • Zenonide traduit les preuves du prouveur de premier ordre Zenon. • Focalide traduit les programmes certifiés de FoCaLiZe. • Une extension du prouveur iProver permet de traduire ses preuves. Ces logiciels sont développés au sein de l'´ equipe Deducteam de INRIA par Ali Assaf, Guillaume Burel, Raphaël Cauderlier, Frédéric Gilbert et Pierre Halmagrand.
Origine : Fichiers produits par l'(les) auteur(s)