Skip to Main content Skip to Navigation
Poster communications

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.
Complete list of metadata

https://hal-mines-paristech.archives-ouvertes.fr/hal-01086609
Contributor : Claire Medrala Connect in order to contact the contributor
Submitted on : Monday, November 24, 2014 - 3:10:44 PM
Last modification on : Friday, January 21, 2022 - 3:15:25 AM
Long-term archiving on: : Wednesday, February 25, 2015 - 11:05:58 AM

File

A-526-poster.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01086609, version 1

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⟩

Share

Metrics

Record views

229

Files downloads

39