Accéder directement au contenu Accéder directement à la navigation
Poster

Dedukti : un vérificateur de preuves universel

Ronan Saillard 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.
Liste complète des métadonnées

https://hal-mines-paristech.archives-ouvertes.fr/hal-01176726
Contributeur : Claire Medrala <>
Soumis le : mercredi 15 juillet 2015 - 17:25:01
Dernière modification le : jeudi 24 septembre 2020 - 16:36:01
Archivage à long terme le : : mercredi 26 avril 2017 - 05:50:24

Fichier

A-611-poster.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01176726, version 1

Citation

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

Partager

Métriques

Consultations de la notice

189

Téléchargements de fichiers

51