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; Tue, 15 Nov 1994 18:25:11 +0000 Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA18741; Tue, 15 Nov 1994 11:11:19 -0700 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with SMTP (1.38.193.4/16.2) id AA18736; Tue, 15 Nov 1994 11:11:03 -0700 Received: from auk.cl.cam.ac.uk (user drs1004 (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Tue, 15 Nov 1994 18:01:42 +0000 To: info-hol@leopard.cs.byu.edu Subject: Thesis and HUG93 paper available via ftp Date: Tue, 15 Nov 1994 18:01:11 +0000 From: Donald Syme Message-Id: <"swan.cl.cam.:004820:941115180200"@cl.cam.ac.uk> Wow, my first mailing to info-hol in 18 months. I have, at last, re-latexed my 1992 undergraduate thesis entitled "Mechanized Reasoning about Standard ML using HOL" and it is now available for anonymous ftp from ftp://ftp.cl.cam.ac.uk/hvg/papers/MLinHOL.thesis.ps.gz Also available is the postscript for my paper submitted to the 1993 HOL users groups conference on the same topic ftp://ftp.cl.cam.ac.uk/hvg/papers/MLinHOL.hug93.ps.gz Both are accessible from my home page: http://www.cl.cam.ac.uk/users/drs1004/ Sooner or later I will tidy up my code and make it available as a HOL contrib library for HOL88. It shares many concepts and techniques with Elsa Gunter and Myra VanInwegen's contrib on the same topic for HOL90. Let me know if there are any problems. Cheers, Donald Syme ----------------------------------------------------------------------------- The Computer Laboratory Trinity Hall New Museums Site CB2 1TJ University of Cambridge Cambridge, UK -----------------------------------------------------------------------------