Topic: Dedukti?

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.

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.