Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, Epiciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [17 references]  Display  Hide  Download
Contributor : Jean-Pierre Jouannaud Connect in order to contact the contributor
Submitted on : Monday, June 13, 2016 - 11:49:03 AM
Last modification on : Friday, February 4, 2022 - 3:19:02 AM


Files produced by the author(s)


  • HAL Id : hal-01330980, version 1


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. ⟨hal-01330980⟩



Record views


Files downloads