Dedukti : un vérificateur de preuves universel - Archive ouverte HAL Accéder directement au contenu
Poster Année :

Dedukti : un vérificateur de preuves universel

(1)
1

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.
Fichier principal
Vignette du fichier
A-611-poster.pdf (127.05 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-01176726 , version 1 (15-07-2015)

Identifiants

  • HAL Id : hal-01176726 , version 1

Citer

Ronan Saillard. Dedukti : un vérificateur de preuves universel. Journées nationales du GDR GPL 2015, Jun 2015, Bordeaux, France. ⟨hal-01176726⟩
143 Consultations
33 Téléchargements

Partager

Gmail Facebook Twitter LinkedIn More