Dedukti:un vérificateur de preuves universel

Abstract : 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.
Type de document :
Poster
Journées nationales GDR - GPL - CIEL - AFADL, Apr 2013, Nancy, France
Liste complète des métadonnées

https://hal-mines-paristech.archives-ouvertes.fr/hal-01086609
Contributeur : Claire Medrala <>
Soumis le : lundi 24 novembre 2014 - 15:10:44
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : mercredi 25 février 2015 - 11:05:58

Fichier

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

Identifiants

  • HAL Id : hal-01086609, version 1

Collections

Citation

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〉

Partager

Métriques

Consultations de la notice

252

Téléchargements de fichiers

84