Software

dedukti

Dedukti is a universal proof checker, based on the λΠ-calculus modulo formalism.
The project is named after the word for "to deduce" in Esperanto.
Dedukti has its own webpage.

CoqInE

CoqIne is a translator from Coq to dedukti.
It wil be released very soon.

Hol2DK

Hol2DK is a translator from HOL Light to dedukti.
It wil be released very soon.