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; Wed, 2 Nov 1994 13:53:42 +0000 Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA16755; Wed, 2 Nov 1994 06:46:02 -0700 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from vanuata.dcs.gla.ac.uk by leopard.cs.byu.edu with SMTP (1.38.193.4/16.2) id AA16751; Wed, 2 Nov 1994 06:45:59 -0700 Received: from switha.dcs.gla.ac.uk by vanuata.dcs.gla.ac.uk with LOCAL SMTP (PP); Wed, 2 Nov 1994 13:36:59 +0000 To: rahard@ee.umanitoba.ca Cc: info-hol@leopard.cs.byu.edu, tfm@dcs.gla.ac.uk Subject: Re: Looking for HOL video/tutorial In-Reply-To: Your message of "Wed, 02 Nov 1994 06:16:42 CST." <9411021216.AA00540@ic11.ee.umanitoba.ca> Date: Wed, 02 Nov 1994 13:36:52 +0000 From: Tom Melham Message-ID: <"swan.cl.cam.:181160:941102135424"@cl.cam.ac.uk> > I was wondering ... is there a HOL tutorial video ? > I am looking for various videos on functional programming/theorem provers. Actually... there is, but it's quite old by now and very out-of-date. Back in July 1987, Mike Gordon, John Herbert, and I conducted a course on Hardware Specification and Verification using HOL as part of the UT Year of Programming series. This was videotaped and the tapes marketed by the CS department at UT Austin. I can post further details, if anyone's really interested. Tom