Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 26 May 1994 19:17:36 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA26671; Thu, 26 May 1994 12:14:44 -0600 Sender: hol2000-request@lal.cs.byu.edu Errors-To: hol2000-request@lal.cs.byu.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA26667; Thu, 26 May 1994 12:14:40 -0600 Received: from merganser.cl.cam.ac.uk (user rjb (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Thu, 26 May 1994 14:18:58 +0100 To: hol2000@leopard.cs.byu.edu Subject: More Tools (Re: User interface versus expanding the logic) In-Reply-To: Your message of "Thu, 26 May 94 12:41:10 EDT." <"i80fs2.ira.481:26.04.94.10.41.14"@ira.uka.de> Date: Thu, 26 May 94 14:18:38 +0100 From: Richard Boulton Message-Id: <"swan.cl.cam.:075640:940526131907"@cl.cam.ac.uk> I agree with Ralf Reetz that more specialized theorem proving and other tools are required. I expect most people do. More specifically, Ralf writes: > In my point of view, we do need a better user interface and more > specialized proving facilities ON TOP of an existing hol. Take e.g. > ARITH_CONV: we might like to have something similar for ==`:integer`==, > ==`:list`==, an so on. A graphical user interface has been developed, but I can't say when it will be publicly available. (Laurent, if you're listening, can you?) It is on my long-term agenda to write proof procedures for integers, lists, and one or two other things, and to try to combine them. However, don't hold your breath! > Take e.g. deep embedding of new languages: we might like to have something > which automates e.g. syntax embedding (look at compiler compilers: a lot > has been automated). I am currently developing SML code to automatically generate ML datatype declarations for abstract syntax trees, HOL type declarations for abstract syntax trees, parsers, pretty-printers, and useful functions from a single specification of syntax. It is not clear yet how well this will all work, but the results so far are promising. Richard.