Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Fri, 25 Aug 1995 13:31:47 +0100
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA080003456;
          Fri, 25 Aug 1995 06:24:16 -0600
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: list
Received: from vanuata.dcs.gla.ac.uk by leopard.cs.byu.edu 
          with ESMTP (1.37.109.15/16.2) id AA079973454;
          Fri, 25 Aug 1995 06:24:14 -0600
Received: from gozo.dcs.gla.ac.uk by vanuata.dcs.gla.ac.uk with LOCAL SMTP (PP);
          Fri, 25 Aug 1995 13:20:26 +0100
To: Donald Syme <Donald.Syme@cl.cam.ac.uk>
Cc: hol2000@leopard.cs.byu.edu, tfm@dcs.gla.ac.uk
Subject: Re: Discussion on meta-language for HOL
In-Reply-To: Your message of "Fri, 25 Aug 1995 12:58:03 BST." <"swan.cl.cam.:250290:950825115808"@cl.cam.ac.uk>
Date: Fri, 25 Aug 1995 13:20:23 +0100
From: Tom Melham <tfm@dcs.gla.ac.uk>
Message-ID: <"swan.cl.cam.:265960:950825123231"@cl.cam.ac.uk>


> BTW, perhaps Andy Gordon could give us the run down on whether 
> Miranda would be practical to use for a theorem prover??

I don't know about Miranda, but the folks around here seem to
think Haskell would be suitable. I had a student implement a 
simple LCF-style prover in Haskell last year, and it all seemed
quite feasible -- using the standard monadic tricks to handle
failure.  However, the interface was not very developed, and
so the toy system he wrote didn't require much (any) state.

I believe that Keith Hanna has quite a bit of experience with
implementing provers in a `pure' function language.

Tom