[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: A Plan for Hacking

From: Stefan Israelsson Tampe
Subject: Re: A Plan for Hacking
Date: Mon, 26 Sep 2011 12:31:48 +0200

> 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.


reply via email to

[Prev in Thread] Current Thread [Next in Thread]