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 <>
Submitted on : Monday, November 24, 2014 - 3:10:44 PM
Last modification on : Thursday, September 24, 2020 - 4:36:02 PM
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

492

Files downloads

116