Haskell alterantives for Isabelle or ACL2

[Brian McBride]

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