Dedukti : un vérificateur de preuves universel

Abstract : - Dedukti est un veri cateur de type pour -calcul modulo. - Le -calcul modulo est une extension du -calcul avec des types dépendants et une relation de conversion étendue par des règles de reecriture. - Dedukti est capable de verifi er les preuves provenant de prouveurs de théorèmes (Zenon, iProver) et d'assistants de preuves (Coq, HOL, Focalize). - On montre a travers plusieurs exemples que l'utilisation de la rééecriture caractéristique du -calcul modulo permet d'obtenir des preuves plus petites et plus rapides à vérifi er.
Type de document :
Poster
Journées de seconde année de l'Ecole Doctorale à Mines ParisTech, Jun 2014, Paris, France
Liste complète des métadonnées

https://hal-mines-paristech.archives-ouvertes.fr/hal-01100519
Contributeur : Claire Medrala <>
Soumis le : mardi 6 janvier 2015 - 15:30:18
Dernière modification le : lundi 12 novembre 2018 - 10:57:02
Document(s) archivé(s) le : vendredi 11 septembre 2015 - 00:46:08

Fichier

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

Identifiants

  • HAL Id : hal-01100519, version 1

Collections

Citation

Ronan Saillard. Dedukti : un vérificateur de preuves universel. Journées de seconde année de l'Ecole Doctorale à Mines ParisTech, Jun 2014, Paris, France. 〈hal-01100519〉

Partager

Métriques

Consultations de la notice

996

Téléchargements de fichiers

89