Received: from scaup.cl.cam.ac.uk by Steve.CL.Cam.AC.UK with SMTP/TCP/IP over Ethernet id a011431; 9 Dec 88 6:07 GMT Via: uk.ac.ucl.cs.nss; 9 Dec 88 6:05 GMT (UK.AC.Cam.Cl.scaup) Received: from clover.ucdavis.edu by NSS.Cs.Ucl.AC.UK via Satnet with SMTP id aa02004; 9 Dec 88 5:30 GMT Received: from uunet.UU.NET by clover.ucdavis.edu (5.59/UCD.EECS.1.1) id AA06706; Thu, 8 Dec 88 21:34:42 PST Received: from mcvax.UUCP by uunet.UU.NET (5.59/1.14) with UUCP id AA29804; Fri, 9 Dec 88 00:33:16 EST Received: by mcvax.cwi.nl via EUnet; Fri, 9 Dec 88 06:05:44 +0100 (MET) Received: from logitek by kestrel.Ukc.AC.UK with UUCP id aa14780; 8 Dec 88 23:14 GMT Received: by logitek.co.uk (smail 2.5 [x25]) id AA01151; 8 Dec 88 12:01:32 EST (Thu) From: David Shepherd Date: Thu, 8 Dec 88 10:25:46 GMT Message-Id: <16219.8812081025@brwa.inmos.co.uk> To: info-hol@edu.ucdavis.clover Subject: HOL in Common Lisp Sender: mcvax!inmos!des Status: RO If HOL does have to go over to Common Lisp I would prefer KCL as I have been informed that this is reasonably portable so I might be able to get it onto the transputer based systems we will want to use. Otherwise we will stick with the last Franz Version and wait until the "proper" upgrade is done and the SML version is ready --- is a simplistic SML port really that complicated -- perhaps that's the way to go rather than Common Lisp --- RAL have done a SML in Franz Lisp port of LCF so much of the ML translations may already be available. david shepherd p.s. in any case this talk of Common Lisp is giving me another excuse for trying to recompile KCL for the transputer!!