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; Sat, 7 May 1994 20:54:48 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA16034; Sat, 7 May 1994 13:41:33 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA16030; Sat, 7 May 1994 13:41:24 -0600 Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) id AA00925; Sat, 7 May 1994 12:42:29 -0700 Received: from cormorant.cl.cam.ac.uk (user mjcg (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Sat, 7 May 1994 20:42:11 +0100 Received: by cormorant.cl.cam.ac.uk (4.1/SMI-3.0DEV3) id AA15207; Sat, 7 May 94 20:42:06 BST Date: Sat, 7 May 94 20:42:06 BST From: Mike.Gordon@cl.cam.ac.uk Message-Id: <9405071942.AA15207@cormorant.cl.cam.ac.uk> To: info-hol@cs.uidaho.edu Subject: HOL2000 HOL2000 ======= Under the slogan "ML2000" a group of people from the ML community are investigating ideas for a major revision of ML. Their aim is to design a language in the ML tradition that builds on current experience with Standard ML and Caml as well as recent theoretical work on language design and semantics (such as type systems for object oriented programming). The time seems ripe for a HOL2000 initiative analogous to ML2000. HOL is now well over 10 years old and is fairly stable. There is much accumulated wisdom among users about its strengths and weaknesses. Several other general purpose interactive theorem proving systems have substantial user communities (eg Alf, Balzac/Zola, Coq, Eves, IMPS, Isabelle, LAMBDA, LEGO, LP, Nqthm, Nuprl, PVS). The experience gained from this diverse collection of systems must contains many useful lessons for HOL. The goal would be to put together a design for the next generation of HOL-like theorem proving environments. This should not be a redesign from first principles, but an evolution from the current state done in a framework that preserves the existing HOL implementations as workhorses for the rest of the decade. A first step could be to try to come to a consensus about the strong and weak points of HOL. Next, various design proposals could be considered and implementation experiments conducted. Ultimately, some mechanism and resources will be needed to support the specification, publication and implementation of the resulting design; however, this is something to be faced later rather than now. A mailing list for discussions related to HOL2000 has been created, which you can join by sending a message to: hol2000-request@lal.cs.byu.edu You can send a message to the list by sending mail to: hol2000@lal.cs.byu.edu --------------------------------------------------------------------------