Yesterday someone pointed me to the Dedukti project:
It's apparently a proof checker written in ocaml. It might not be too difficult to modify Dedukti to output definitions and proofs in the format Dalilcoin wants. Since it's written in ocaml, a direct integration might even be possible.
I'll add it to a list of things to look into at some point, unless someone else volunteers to look into it first.