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.