CoqInE

Update:

Ali Assaf is working on a new implementation of Coqine with support for type universes. You can find it at the InriaForge project here, in the develop branch.

Also check out Krajono project, a translation of Matita proofs to Dedukti.

What is CoqInE?

CoqInE permits to produce Dedukti proofs from Coq proofs. It is developed by Mathieu Boespflug, Guillaume Burel and Quentin Carbonneaux.

Get CoqInE

Download this file. Unzip and extract it

tar xvzf coqine.tar.gz

Change directory

cd coqine

Make sure you have OCaml installed or install it. Make sure you have have Coq installed (in order to be able to generate .vo files used by CoqInE, using the coqc command). 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. Make sure you have Dedukti installed or install it.

Then configure and compile CoqInE:

./configure
make

(Type ./configure -help for available configuration options.)

Start enjoying

cd t
coqc test.v
../bin/coqine -h test.vo
dedukti Coq1univ.dk test.dk | lua -l dedukti -

A development version of CoqInE can also been retrieved via github.

Documentation

A succinct manual (not up-to-date) 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