[plt-scheme] Schemebelle?

From: Paulo J. Matos (pocmatos at gmail.com)
Date: Mon Apr 27 13:49:56 EDT 2009

On Mon, Apr 27, 2009 at 5:30 PM, Sam TH <samth at ccs.neu.edu> wrote:
> On Mon, Apr 27, 2009 at 1:19 PM, Paulo J. Matos <pocmatos at gmail.com> wrote:
>> Now, I am wondering, how hard would it be to get something done for
>> Scheme (and is there any interest from the community)?
>> I would guess one major issue would be typing, but I would guess
>> typed-scheme would makes things easier for a possible schemebelle?
> I doubt it.  Typed Scheme has a (very) different type system from
> Isabelle, and Haskell and Isabelle are both pure languages, whereas
> Scheme is not.
> If you want to go the "translate Scheme into a theorem prover" route,
> ACL2 might be a better option.

Yes, I agree... I guess having dracula integrated with plt-scheme
helps but I was more wondering what would the research challenges one
would face?

I am research-wise more familiar with model checking than with theorem
proving so this might well be out of my league here but I was just
curious if anyone knows about this.


Paulo Matos

> --
> sam th
> samth at ccs.neu.edu

Paulo Jorge Matos - pocmatos at gmail.com
Webpage: http://www.personal.soton.ac.uk/pocm

Posted on the users mailing list.