Accéder directement au contenu Accéder directement à la navigation
Communication dans un congrès

Dedukti : a Universal Proof Checker

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.
Type de document :
Communication dans un congrès
Liste complète des métadonnées

https://hal-mines-paristech.archives-ouvertes.fr/hal-00833992
Contributeur : Claire Medrala <>
Soumis le : vendredi 14 juin 2013 - 14:57:31
Dernière modification le : jeudi 24 septembre 2020 - 16:36:01
Archivage à long terme le : : mardi 4 avril 2017 - 21:42:18

Fichiers

Identifiants

  • HAL Id : hal-00833992, version 1

Citation

Ronan Saillard. Dedukti : a Universal Proof Checker. Foundation of Mathematics for Computer-Aided Formalization Workshop, Jan 2013, Padova, Italy. ⟨hal-00833992⟩

Partager

Métriques

Consultations de la notice

380

Téléchargements de fichiers

240