Skip to Main content Skip to Navigation
Poster communications

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.
Complete list of metadata

https://hal-mines-paristech.archives-ouvertes.fr/hal-01100519
Contributor : Claire Medrala <>
Submitted on : Tuesday, January 6, 2015 - 3:30:18 PM
Last modification on : Thursday, September 24, 2020 - 4:36:02 PM
Long-term archiving on: : Friday, September 11, 2015 - 12:46:08 AM

File

A-585-poster.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01100519, version 1

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⟩

Share

Metrics

Record views

1127

Files downloads

121