Haskell alterantives for Isabelle or ACL2

[Iavor Diatchki]

hello,

there is also the Yarrow proof assitant
http://www.cs.kun.nl/~janz/yarrow/
but like so many other haskell tools it is somewhat ancient (the source 
seems to be in haskell 1.3)
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
>