13 May
2003
13 May
'03
11:02 a.m.
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