Encoding Proofs in Dedukti: the case of Coq proofs

Abstract : A main ambition of the Inria project Dedukti is to serve as a common language for representing and type checking proof objects originating from other proof systems. Encoding these proof objects makes heavy use of the rewriting capabilities of LambdaPiModulo, the formal system on which Dedukti is based. So far, the proofs generated by two automatic proof systems, Zenon and iProver, have been encoded, and can therefore be read and checked by Dedukti. But Dedukti goes far beyond this so-called hammering technique of sending goals to automated provers. Proofs from HOL and Matita can be encoded as well. Some Coq’s proofs can be encoded already, when they do not use universe polymorphism. Our ambition here is to close this remaining gap. To this end, we describe a rewrite-based encoding in LambdaPiModulo of the Calculus of Constructions with a cumulative hierarchy of predicative universes above Prop, which is confluent on open terms.
Type de document :
Communication dans un congrès
Proceedings Hammers for Type Theories, Jul 2016, Coimbra, Portugal. Easy Chair, Proc. HaTT, 2016, Proc. Higher-Order rewriting Workshop. 〈http://hatt2016.inria.fr/〉
Liste complète des métadonnées

Littérature citée [17 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01330980
Contributeur : Jean-Pierre Jouannaud <>
Soumis le : lundi 13 juin 2016 - 11:49:03
Dernière modification le : jeudi 10 mai 2018 - 02:06:25

Fichier

HaTT_2016_paper_3.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01330980, version 1

Citation

Ali Assaf, Gilles Dowek, Jean-Pierre Jouannaud, Jiaxiang Liu. Encoding Proofs in Dedukti: the case of Coq proofs. Proceedings Hammers for Type Theories, Jul 2016, Coimbra, Portugal. Easy Chair, Proc. HaTT, 2016, Proc. Higher-Order rewriting Workshop. 〈http://hatt2016.inria.fr/〉. 〈hal-01330980〉

Partager

Métriques

Consultations de la notice

263

Téléchargements de fichiers

77