Haskell alterantives for Isabelle or ACL2
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
hello, as far as i know there are no real theorem provers using haskell as a metalanguage. there also aren't any text editors that can be programmed in haskell, i wonder how many people have wanted to program their emacs in haskell :-) 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
On Tue, 13 May 2003, Iavor Diatchki wrote:
hello, as far as i know there are no real theorem provers using haskell as a metalanguage. there also aren't any text editors that can be programmed in haskell, i wonder how many people have wanted to program their emacs in haskell :-)
Claus Reineke (if I'm remembering the attribution correctly; I often get it embarassingly wrong) said maybe a year ago that he'd got some Haskell scriptability for vi working. ___cheers,_dave_________________________________________________________ www.cs.bris.ac.uk/~tweed/ | `It's no good going home to practise email:tweed@cs.bris.ac.uk | a Special Outdoor Song which Has To Be work tel:(0117) 954-5250 | Sung In The Snow' -- Winnie the Pooh
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.
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
participants (5)
-
Brian McBride -
D. Tweed -
Ferenc Wagner -
Iavor Diatchki -
Marko van Eekelen