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; Thu, 24 Aug 1995 18:01:21 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA022523027; Thu, 24 Aug 1995 10:50:27 -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 AA022483001; Thu, 24 Aug 1995 10:50:01 -0600 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Thu, 24 Aug 1995 17:42:20 +0100 X-Uri: To: Konrad Slind Cc: jgrundy@ra.abo.fi, hol2000@leopard.cs.byu.edu, John.Harrison@cl.cam.ac.uk Subject: Re: Paper available: "HOL Done Right" In-Reply-To: Your message of "Thu, 24 Aug 1995 17:50:32 +0200." <95Aug24.175042met_dst.8087@sunbroy14.informatik.tu-muenchen.de> Date: Thu, 24 Aug 1995 17:42:15 +0100 From: John Harrison Message-Id: <"swan.cl.cam.:129790:950824164229"@cl.cam.ac.uk> It shouldn't be hard to work at the level of *abstract* syntax without any code differences, since there are relatively few semantic differences between the cores of SML and CAML (as far as I know). But when one starts using special features of each language (e.g. SML's functors or CAML's Lisp-EQ test) things become troublesome. Really, it's crazy that there should be any source changes needed at all for soi-disant "Standard" ML compilers. I guess it's the ISO Pascal problem: without a whole host of additional facilities, the core language isn't much use in the real world. But I seem to recall some library standardization effort in the SML world. For our purposes, standards for quotations and toplevel printers would be the most important thing. John.