Dedukti:un vérificateur de preuves universel - Archive ouverte HAL Accéder directement au contenu
Poster Année :

Dedukti:un vérificateur de preuves universel

(1) , (1) , (2, 1)
1
2

Résumé

Dedukti est un vérificateur de types pour le λΠ-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-526-poster.pdf (1.01 Mo) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-01086609 , version 1 (24-11-2014)

Identifiants

  • HAL Id : hal-01086609 , version 1

Citer

Ali Assaf, Raphaël Cauderlier, Ronan Saillard. Dedukti:un vérificateur de preuves universel. Journées nationales GDR - GPL - CIEL - AFADL, Apr 2013, Nancy, France. ⟨hal-01086609⟩
229 Consultations
39 Téléchargements

Partager

Gmail Facebook Twitter LinkedIn More