Haskell alterantives for Isabelle or ACL2

[Simon Peyton-Jones]

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
|=20
| 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
:-)
|=20
| bye iavor
|=20
| 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
| >
|=20
|=20
| _______________________________________________
| Haskell mailing list
| Haskell@haskell.org
| http://www.haskell.org/mailman/listinfo/haskell