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; Mon, 21 Aug 1995 15:49:24 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA274096100; Mon, 21 Aug 1995 08:41:40 -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 AA274066088; Mon, 21 Aug 1995 08:41:28 -0600 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Mon, 21 Aug 1995 15:40:42 +0100 X-Uri: To: hol2000@leopard.cs.byu.edu Subject: Paper available: "HOL Done Right" Date: Mon, 21 Aug 1995 15:40:38 +0100 From: John Harrison Message-Id: <"swan.cl.cam.:251800:950821144045"@cl.cam.ac.uk> The following paper, based on a talk I gave in Cambridge last month, is now available on the Web. URL: http://www.cl.cam.ac.uk/users/jrh/papers/holright.dvi.gz PAGES: 15 ABSTRACT: In our opinion, history and compatibility considerations have rendered existing HOL implementations rather messy and badly organized. We describe how, building on joint work with Konrad Slind, we have produced a re-engineered HOL. Various experiments have been tried on this `toy' version, and we will report the results. All comments welcome, though I don't have much time for discussions right now. John.