logo EDITE Raphael CAUDERLIER
Identité
Raphael CAUDERLIER
État académique
Thèse soutenue le 2016-10-10
Sujet: Mécanismes objets et changement de représentation de données pour l'interopérabilité entre prouveurs
Direction de thèse:
Laboratoire:
Voisinage
Ellipse bleue: doctorant, ellipse jaune: docteur, rectangle vert: permanent, rectangle jaune: HDR. Trait vert: encadrant de thèse, trait bleu: directeur de thèse, pointillé: jury d'évaluation à mi-parcours ou jury de thèse.
Productions scientifiques
oai:hal.archives-ouvertes.fr:hal-01171360
Checking Zenon Modulo Proofs in Dedukti
International audience
Dedukti has been proposed as a universal proof checker. It is a logical framework based on the λΠ-calculus modulo that is used as a backend to verify proofs coming from theorem provers, especially those implementing some form of rewriting. We present a shallow embedding into Dedukti of proofs produced by Zenon Modulo, an extension of the tableau-based first-order theorem prover Zenon to deduction modulo and typing. Zenon Modulo is applied to the verification of programs in both academic and industrial projects. The purpose of our embedding is to increase the confidence in automatically generated proofs by separating untrusted proof search from trusted proof verification.
Fourth Workshop on Proof eXchange for Theorem Proving (PxTP) https://hal.inria.fr/hal-01171360 Fourth Workshop on Proof eXchange for Theorem Proving (PxTP), Aug 2015, Berlin, Germany. 2015, <http://pxtp15.lri.fr/> http://pxtp15.lri.fr/ARRAY(0x7f03ffde6860) 2015-08-01
oai:hal.archives-ouvertes.fr:hal-01097444
Objects and subtyping in the λΠ-calculus modulo
HASH(0x7f04004be2b8)
https://hal.inria.fr/hal-01097444 2015ARRAY(0x7f0400cee658) 2015-06-13
oai:hal.archives-ouvertes.fr:hal-01141789
Mixing HOL and Coq in Dedukti (Rough Diamond)
HASH(0x7f03ffde6a88)
https://hal.inria.fr/hal-01141789 2015ARRAY(0x7f04014614e8) 2015
Soutenance
Thèse: Mécanismes objets et changement de représentation de données pour l'interopérabilité entre prouveurs
Soutenance: 2016-10-10