 |
 |
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.
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
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)