Return-Path: <John.Harrison-request@cl.cam.ac.uk>
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, 1 Nov 1994 14:29:42 +0000
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA21588;
          Tue, 1 Nov 1994 07:20:45 -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 AA21584;
          Tue, 1 Nov 1994 07:20:39 -0700
Received: from woodcock.cl.cam.ac.uk (user mjcg (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Tue, 1 Nov 1994 14:12:02 +0000
Received: by woodcock.cl.cam.ac.uk (4.1/SMI-3.0DEV3) id AA20975;
          Tue, 1 Nov 94 14:11:37 GMT
Date: Tue, 1 Nov 94 14:11:37 GMT
From: Mike.Gordon@cl.cam.ac.uk
Message-Id: <9411011411.AA20975@woodcock.cl.cam.ac.uk>
To: info-hol@leopard.cs.byu.edu
Cc: Piete.Brooks@cl.cam.ac.uk
Subject: Talk by John Harrison on MBONE


Anyone outside the UK who is interested in hearing John Harrison's
talk should send email to:

   Piete.Brooks@cl.cam.ac.uk

If you would like to hear Paul Curzon speak on "Experiences Verifying
the Fairisle Switching Elements" on November 9 please email Piete
Brooks also (it is not yet decided whether Paul's talk will be
multicast on MBONE).

Here is the announcement for John's talk that Piete sent out to the
MBONE world:

-----------------------------------------------------------------------

We are planning to transmit this week's seminar only within JIPS
(ac.uk), unless anyone outside JIPS would like it. If you would, email
me the name of your nearest MBone router (if you know it), and I'll
set the TTL accordingly.  Please also say if you want video (of the
speaker - slides available separately)


   NAME:	John Harrison, University of Cambridge, Computer Laboratory
   DATE:	Wednesday 2nd November 1994 at 4.15pm (16:15 UTC)
   PLACE:	Babbage Lecture Theatre
   TITLE:	Theorem Provers & Computer Algebra Systems

   Computer theorem provers and computer algebra systems
   are both aids to symbolic computation. Nevertheless they
   have quite different design philosophies and are 
   invariably used by different kinds of people. In this talk
   we draw some contrasts, particularly as regards
   correctness and ease of use, and suggest ways in which
   the strengths of both kinds of system can be combined.


This seminar will be multicast (audio and video) on the mbone as part of
our multimedia test programme. Further information is available at 
http://www.cl.cam.ac.uk/mbone/#cl.

