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

https://hal.inria.fr/hal-01330980
Contributor : Jean-Pierre Jouannaud <>
Submitted on : Monday, June 13, 2016 - 11:49:03 AM
Last modification on : Wednesday, June 2, 2021 - 3:41:06 AM

File

HaTT_2016_paper_3.pdf
Files produced by the author(s)

Identifiers

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

Share

Metrics

Record views

401

Files downloads

140