Dedukti:un vérificateur de preuves universel - Mines Paris Accéder directement au contenu
Poster Année :

Dedukti:un vérificateur de preuves universel

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.

Domaines

Théorie et langage formel [cs.FL] Logique en informatique [cs.LO]
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)

Claire Medrala  : Connectez-vous pour contacter le contributeur

https://hal-mines-paristech.archives-ouvertes.fr/hal-01086609

Soumis le : lundi 24 novembre 2014-15:10:44

Dernière modification le : mardi 25 octobre 2022-16:22:43

Archivage à long terme le : mercredi 25 février 2015-11:05:58

Télécharger pour visualiser

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⟩

Exporter

BibTeX TEI Dublin Core DC Terms EndNote Datacite

Collections

INSTITUT-TELECOM ENSMP INRIA ENSMP_CRI PARISTECH INRIA2 PSL ENSMP_DR
239 Consultations
41 Téléchargements

Partager

Gmail Facebook Twitter LinkedIn More