Encoding Proofs in Dedukti: the case of Coq proofs
In: Proc. HaTT ; Proceedings Hammers for Type Theories ; https://inria.hal.science/hal-01330980 ; Proceedings Hammers for Type Theories, Jul 2016, Coimbra, Portugal ; http://hatt2016.inria.fr/, 2016
Online
Konferenz
Zugriff:
International audience ; 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 proofsystems, 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.
Titel: |
Encoding Proofs in Dedukti: the case of Coq proofs
|
---|---|
Autor/in / Beteiligte Person: | Assaf, Ali ; Dowek, Gilles ; Jouannaud, Jean-Pierre ; Liu, Jiaxiang ; Inc, Google ; Research at Google ; Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM) ; Laboratoire Spécification et Vérification Cachan (LSV) ; École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria) ; École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS) ; Laboratoire d'informatique de l'École polytechnique Palaiseau (LIX) ; École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS) ; Tsinghua University Beijing (THU) ; Voronkov, Andrei |
Link: | |
Zeitschrift: | Proc. HaTT ; Proceedings Hammers for Type Theories ; https://inria.hal.science/hal-01330980 ; Proceedings Hammers for Type Theories, Jul 2016, Coimbra, Portugal ; http://hatt2016.inria.fr/, 2016 |
Veröffentlichung: | HAL CCSD ; Easy Chair, 2016 |
Medientyp: | Konferenz |
Schlagwort: |
|
Sonstiges: |
|