Haskell alterantives for Isabelle or ACL2

[Marko van Eekelen]

At 12:02 13-5-2003 +0100, you 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

Dear Brian,

You might consider working with Sparkle, a proof assistant with some degree of automation.
Sparkle is used with Clean, a pure, lazy, functional, Haskell-like language. 
See www.cs.kun.nl/~clean

Marko van Eekelen.