Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Message-Id: <199506301359.GAA02036@dworshak.cs.uidaho.edu>
To: info-hol@cs.uidaho.edu, lambda-usergroup@dcs.ed.ac.uk, 
    theorem-provers@mc.lcs.mit.edu, isabelle-users@cl.cam.ac.uk, 
    academic-staff@dcs.gla.ac.uk, research-staff@dcs.gla.ac.uk, 
    research-students@dcs.gla.ac.uk, jwright@aton.abo.fi, jgrundy@aton.abo.fi
Cc: tfm@dcs.gla.ac.uk
Subject: Course about Program Semantics and Refinement in HOL
Date: Fri, 30 Jun 1995 14:58:51 +0100
From: Tom Melham <tfm@dcs.gla.ac.uk>

Please forward the attached course announcement as  you see fit. 

This course forms part of Glasgow's Computing Science
Research Festival.  For further information, see

   http://www.dcs.gla.ac.uk/research/festival.html

or contact me at tfm@dcs.gla.ac.uk after 17 July. 

Please accept my apologies for any multiple copies due to 
overlapping mailing lists.

Tom Melham

============================================================================
============================================================================

                       University of Glasgow

           Introduction to Program Semantics and Refinement 
                   using the HOL Theorem prover

                          3-4 August 1995


Background and Aims
~~~~~~~~~~~~~~~~~~~

The HOL system is a powerful and widely used computer-aided tool for
constructing formal specifications and proofs in mathematical logic.  One
prominent area of application is support for reasoning about programs,
using, for example, program refinement calculi. This is typically based
on a programming language semantics defined formally in HOL.

This course is designed to give the participants an introduction to the
latest techniques in this exciting and promising area of research.  A
basic introduction to HOL will be included, so no prior knowledge of the
system is needed.

You should consider attending if:

   * you are interested in research in program verification/refinement,
     and want to see what theorem proving might do for you

   * you are working in an area such as computer security, safety-critical 
     systems, or communication protocols, where formal methods are becoming
      an important part of the job,

   * you would like to learn more about the value of using formal
     methods and gain exposure to a leading formal specification
     and verification system.

To get the most out of this course, you should have some familiarity with
predicate calculus at an elementary level.


Outline of the Course
~~~~~~~~~~~~~~~~~~~~~

The course will run over one and a half days during 3-4 August 1995. Sessions
will begin at 9:00 on Thursday 3 August and end by 14:00 on Friday 4 August,
in order to allow participants to get home for the weekend.  The main topics
covered will be

   Introduction to the HOL theorem prover
   Defining program semantics formally in HOL 
   Program refinement techniques in a theorem prover
   Using window inference to reason about programs 

If possible, we will arrange for the participants to have some hands-on 
practical experience with the system.


Course Tutors
~~~~~~~~~~~~~

The course will be presented by 

  Dr Tom Melham           Dr Joakim von Wright     Dr Jim Grundy
  University of Glasgow   Abo Akademi University   Abo Akademi University


Dr Melham has extensive experience in the applications and development
of the HOL system. He conducted tutorials and training courses on HOL at
numerous industrial and academic sites.

Dr von Wright has conducted wide-ranging research using the HOL system;
together with Prof Ralph Back, he pioneered the mechanization of 
refinement in HOL. Later work includes research on verifying modular
programs in HOL.

Dr Grundy's research interests span theory and practice, including work
on research on a novel approach to interactive proof construction called
window inference and application to program refinement. Grundy's work in
these areas has been rigorously implemented in HOL, with a view to practical
application.


Fees and Accommodation
~~~~~~~~~~~~~~~~~~~~~~

There is no fee for attending this course.  You must, however, register
in advance of the course to attend (see below).  Participants must make
their own arrangements for accommodation and meals.

If you need accommodation in Glasgow, there are numerous Bed & Breakfasts
and small Hotels near the University. For further details and assistance
with booking, please contact Isabel Graham at isabel@dcs.gla.ac.uk.


Location
~~~~~~~~

The course will be held at the University of Glasgow's Department of
Computing Science.  Glasgow is easily accessible by rail or air from
the U.K. as well as abroad.

This course forms part of Glasgow's Computing Science Research Festival.


Registration
~~~~~~~~~~~~

Registration in advance is required to attend. The number of places on the
course is limited, so please register early. To register, please return
the attached registration form to Tom Melham (tfm@dcs.gla.ac.uk) no later
than Monday, 31 July 1995. It may be possible to register on the day, if
there are sufficient places, but this cannot be guaranteed.

------------------------------------------------------------------------------
I would like to attend the course on 3-4 August.

  Name         : 
  Full Address :
  Telephone no :
  Fax no       :
  Email        :
------------------------------------------------------------------------------