> 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
