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, 17 Mar 1995 22:54:07 +0000 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA193199343; Fri, 17 Mar 1995 12:42:23 -0700 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-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 AA193169336; Fri, 17 Mar 1995 12:42:16 -0700 Received: from gozo.dcs.gla.ac.uk by vanuata.dcs.gla.ac.uk with LOCAL SMTP (PP); Fri, 17 Mar 1995 19:13:19 +0000 To: Konrad Slind Cc: info-hol@leopard.cs.byu.edu, tfm@dcs.gla.ac.uk Subject: Re: memory consumption of load_theory in HOL90.7 In-Reply-To: Your message of "Fri, 17 Mar 1995 17:15:04 +0100." <95Mar17.171508met.8081@sunbroy14.informatik.tu-muenchen.de> Date: Fri, 17 Mar 1995 19:13:13 +0000 From: Tom Melham Message-ID: <"swan.cl.cam.:109650:950317225450"@cl.cam.ac.uk> Re: C vs SML. ============= Let's not forget, of course, the LCF tradition behind the implementation of HOL! Strong typing and abstract data types are *essential* to the approach. Higher-order functions (for tactics) are required too. Tom