John Matthews [johnm@cse.ogi.edu] writes: The only thing I could find was the following implementation of a first order logic resolution theorem prover, written in Haskell. I don't know anything about it beyond what is on the web page: http://www.cs.yale.edu/homes/cc392/report.html Now, if Brian wants to *reason* about Haskell programs (rather than program in a theorem prover written in Haskell) then the most suitable choice I know of is to use the HOLCF logic in the Isabelle theorem prover. HOLCF combines LCF and HOL, allowing you to prove properties of cpos, least fixedpoints, etc., but also to reason in HOL about purely logical properties at the same time. However, the LCF term language is quite spartan compared to Haskell. For example, you can define continuous datatypes and match against values using case expressions, but there is no support for defining continuous functions by pattern matching. However, there is support for defining purely logical HOL functions via pattern matching. I also know that one of Tom Melham's students formalized aspects of Haskell in the HOL theorem prover, but I don't know the details. Simon | -----Original Message----- | From: haskell-admin@haskell.org [mailto:haskell-admin@haskell.org] On Behalf Of Iavor Diatchki | Sent: 13 May 2003 18:41 | To: Brian McBride | Cc: haskell@haskell.org | Subject: Re: Haskell alterantives for Isabelle or ACL2 | | 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 | > | | | _______________________________________________ | Haskell mailing list | Haskell@haskell.org | http://www.haskell.org/mailman/listinfo/haskell