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