Skip to Main content Skip to Navigation
Conference papers

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

https://hal-mines-paristech.archives-ouvertes.fr/hal-00833992
Contributor : Claire Medrala <>
Submitted on : Friday, June 14, 2013 - 2:57:31 PM
Last modification on : Thursday, September 24, 2020 - 4:36:01 PM
Long-term archiving on: : Tuesday, April 4, 2017 - 9:42:18 PM

Files

Identifiers

  • 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⟩

Share

Metrics

Record views

396

Files downloads

252