Haskell alterantives for Isabelle or ACL2

[Iavor Diatchki]

hello,
as far as i know there are no real theorem provers using haskell as a 
metalanguage.
there also aren't any text editors that can be programmed in haskell, i 
wonder how many people have wanted to program their emacs in haskell :-)

bye iavor

Brian McBride wrote:
> This is a newbie question.
> 
> I'm interested in exploring the use of automatic theorem provers for 
> helping with the formal specification of software systems (in my case 
> semantics of languages and protocols).
> 
> I've found ACL2 and Isabelle (and a few others) - the former uses Lisp 
> as its meta langauge and the latter SML.  For various reasons, some 
> non-technical, I'd rather work in Haskell.  Are there any systems 
> similar to ACL2 or Isabelle that I should consider.  Are there any 
> alternative Haskell based approaches I should consider.
> 
> Brian McBride
> HPLabs, Bristol
> 
> _______________________________________________
> Haskell mailing list
> Haskell@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell
>