Topic: Dedukti?

Yesterday someone pointed me to the Dedukti project:

http://deducteam.gforge.inria.fr/index.html
https://github.com/Deducteam/Dedukti

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.

Re: Dedukti?

Dedukti might be a good starting point, but Dalilcoin should really support a modern type theory prover like Agda or Coq. I've been thinking about this lately and plan to write a longer post, probably in the general discussion board.