Dedukti : a Universal Proof Checker - Archive ouverte HAL Accéder directement au contenu
Communication Dans Un Congrès Année :

Dedukti : a Universal Proof Checker

(1)
1
Ronan Saillard
  • Fonction : Auteur
  • PersonId : 763215
  • IdRef : 191295574

Résumé

Dedukti est un vérificateur de types pour le lambda-Pi -calcul modulo, un formalisme alliant types dépendants et réécriture qui permet d'exprimer et de vérifier les preuves de nombreux systèmes logiques. Nous proposons d'utiliser DEDUKTI comme un vérificateur de preuves universel en traduisant HOL, Coq et FoCaLize vers DEDUKTI.
Fichier principal
Vignette du fichier
A-527.pdf (148.14 Ko) Télécharger le fichier
Vignette du fichier
A-525-slides.pdf (293.09 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Format : Autre

Dates et versions

hal-00833992 , version 1 (14-06-2013)

Identifiants

  • HAL Id : hal-00833992 , version 1

Citer

Ronan Saillard. Dedukti : a Universal Proof Checker. Foundation of Mathematics for Computer-Aided Formalization Workshop, Jan 2013, Padova, Italy. ⟨hal-00833992⟩
221 Consultations
182 Téléchargements

Partager

Gmail Facebook Twitter LinkedIn More