Skip to Main content Skip to Navigation
Poster communications

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.
Document type :
Poster communications
Complete list of metadata

https://hal-mines-paristech.archives-ouvertes.fr/hal-01176726
Contributor : Claire Medrala <>
Submitted on : Wednesday, July 15, 2015 - 5:25:01 PM
Last modification on : Thursday, September 24, 2020 - 4:36:01 PM
Long-term archiving on: : Wednesday, April 26, 2017 - 5:50:24 AM

File

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

Identifiers

  • 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⟩

Share

Metrics

Record views

206

Files downloads

60