Holide

What is Holide?

Holide translates HOL proofs to Dedukti proofs, using the OpenTheory standard (common to HOL Light and HOL4). It is developed and maintained by Ali Assaf and Guillaume Burel.

Get Holide

The source code is available online at INRIA Forge. You can also download it here.

Make sure you have OCaml and Dedukti installed. To compile, simply run 

cd holide
make
Here is an example of a proof in OpenTheory. 
./holide bool-def-1.8/bool-def.art -o dedukti/bool_def.dk
cd dedukti
dkcheck -e hol.dk bool_def.dk