Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Wed, 21 Apr 1993 08:33:08 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA19313; Wed, 21 Apr 93 00:20:59 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA19308; Wed, 21 Apr 93 00:20:48 -0700 Received: from albatross.cl.cam.ac.uk (user mjcg (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Wed, 21 Apr 1993 08:20:39 +0100 Received: by albatross.cl.cam.ac.uk (4.1/SMI-3.0DEV3) id AA03146; Wed, 21 Apr 93 08:20:34 BST Date: Wed, 21 Apr 93 08:20:34 BST From: Mike.Gordon@cl.cam.ac.uk Message-Id: <9304210720.AA03146@albatross.cl.cam.ac.uk> To: coe@panther.cs.uidaho.edu Cc: info-hol@ted.cs.uidaho.edu In-Reply-To: Mike Coe's message of Tue, 20 Apr 93 20:24:22 PDT <199304210324.AA23344@panther.cs.uidaho.edu> Subject: ml in HOL The original denotatational semantics of a predecessor of Classic ML (namely the ML of Edinburgh LCF) existed on a whiteboard at Edinburgh for some years during the 1970s .. but, alas, never got written down. From what I recall it was a fairly routine continuation based semantics. Mike