CoqInE is a plugin for the Coq software translating Coq proofs into Dedukti type-checkable terms. It provides a signature file faithfully encoding the underlying theory of Coq (or a sufficiently large subset of it). The generated ouput is meant to be type-checkable using the latest version of Dedukti.
It was developed by Ali Assaf, Mathieu Boespflug, Guillaume Burel, Quentin Carbonneaux, Gaspard Férey and François Thiré. It is currently developed by Gaspard Férey and François Thiré. Current development is mostly focused on implementing support for Coq universe polymorphism.
Previous versions of the project can be found on:
- InriaForge in the
developbranch. - Github
Also check out Krajono project, a translation of Matita proofs to Dedukti.
Make sure the following dependencies are installed
Warning: the version of OCaml used to compile CoqInE must be the same as the one used to compile the Coq program that generates the .vo files you want to translate.
Installation steps:
git clone https://github.com/Deducteam/CoqInE.git
cd CoqInE
make
Adding the following line to your ~\.coqrc file can help solve some issues (/path/to/coqine should be replaced with the actual path to your CoqInE repository folder).
Add ML Path "/path/to/coqine/master/src".
Examples of library translations are located in the run folder.
- To build debug files:
make debug - To build test files:
make test - To build part of the GeoCoq library:
make geocoq
Generated .dk files are in the corresponding out folder.
A succinct (outdated) manual is provided with the sources (doc/coqine.1.gz).
The translation itself is explained in the following paper:
Mathieu Boespflug and Guillaume Burel. CoqInE: Translating the Calculus of Inductive Constructions into the lambda Pi-calculus Modulo , presented at the PxTP'12 workshop. .pdf