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.