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; Fri, 25 Aug 1995 10:15:28 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA074871557; Fri, 25 Aug 1995 03:05:57 -0600 Sender: hol2000-request@lal.cs.byu.edu Errors-To: hol2000-request@lal.cs.byu.edu Precedence: list Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA074841555; Fri, 25 Aug 1995 03:05:55 -0600 Received: from mallard.cl.cam.ac.uk (user adg (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Fri, 25 Aug 1995 10:06:39 +0100 To: Konrad Slind Cc: hol2000@leopard.cs.byu.edu Subject: Re: Paper available: "HOL Done Right" In-Reply-To: Your message of "Thu, 24 Aug 1995 19:38:00 +0200." <95Aug24.193806met_dst.8087@sunbroy14.informatik.tu-muenchen.de> Date: Fri, 25 Aug 1995 10:06:31 +0100 From: Andrew Gordon Message-Id: <"swan.cl.cam.:170380:950825090644"@cl.cam.ac.uk> Konrad wrote: >Maybe we could draw up a list of concerns from our (the theorem prover) >community and submit it for the ML2000 cabal to chew on. The ML2000 group would welcome this. They give a seminar at the Newton Institute in Cambridge last Friday on the aims and strategy of the ML2000 effort. I raised the issue of whether they aimed to support the large community of theorem-prover people using ML/SML/CAML. They are in fact particularly interested in supporting activities like systems programming and oject-oriented programming, that are comparatively rare with SML, and in competing directly with C. But they were concerned to continue to support theorem-proving. John Mitchell said they'd welcome a list such as the one Konrad proposes. Andy.