> I'm also interested in what Stefan Tampe is doing, because I believehe's implementing a
> formal logic system in Guile. Stefan, does yourproject connect to this one?
 
Yes I'm implementing the leanCop first order logic prover. Now this might not be the same
as implementing a new Coq system. I don't know the difference. Also there is a prover example in the kanren framework.

If you need to stick with scheme only use kanren as a base.

You could use my development if you can stand to load in a shared compiled library. I prefere to have both systems available in a toolbox, kanren has it's pros and cons and as well as a
more traditional prolog system has it's pros and cons.

For the typechecker. Check out what I'm doing in guile-unify as well. There a big part of
the features in typed racket implemented. Currently it demands that everything is typed
but I plan to loosen this as well in order to allow for untyped arguments e.g. can be anything.

/Stefan