Dedukti : a Universal Proof Checker - Mines Paris Accéder directement au contenu
Communication Dans Un Congrès Année : 2013

Dedukti : a Universal Proof Checker

Ronan Saillard
  • Fonction : Auteur
  • PersonId : 763215
  • IdRef : 191295574
Centre de Recherche en Informatique

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.

Domaines

Théorie et langage formel [cs.FL] Logique en informatique [cs.LO]
Fichier principal
Vignette du fichier
A-527.pdf (148.14 Ko) Télécharger le fichier
A-525-slides.pdf (293.09 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Format : Autre

Claire Medrala  : Connectez-vous pour contacter le contributeur

https://minesparis-psl.hal.science/hal-00833992

Soumis le : vendredi 14 juin 2013-14:57:31

Dernière modification le : vendredi 19 avril 2024-16:18:57

Archivage à long terme le : mardi 4 avril 2017-21:42:18

Télécharger pour visualiser

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⟩

Exporter

BibTeX XML-TEI Dublin Core DC Terms EndNote DataCite

Collections

INSTITUT-TELECOM ENSMP ENSMP_CRI PARISTECH PSL ENSMP_DR
227 Consultations
202 Téléchargements

Partager

Gmail Facebook X LinkedIn More