To: info-hol@edu.uidaho.cs.ted
Subject: Formal methods awareness club.
Date: Fri, 31 May 91 16:21:10 +0100
From: Tom.Melham@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.724:31.04.91.15.21.16"@cl.cam.ac.uk>

_____________________________________________________________________
Awareness Club in Computer Assisted Formal Reasoning

Inaugural Meeting, 12th June 1991

The meeting will start at 10am in Room 308 in the Department of
Computing, Imperial College, London. Enter at 180 Queensgate. The room
will be signposted from there. If anyone is coming and hasn't yet told
me can you please do so ASAP

So far about 150 people have registered an interest in the club. This
electronic message will be followed up next week by a hard copy
mailshot. I enclose a copy of the registration form for the club. Can
you pass this on to any colleagues who may be interested.

George Cleland
______________________________________________________________________

Agenda

10.00   Welcome and introduction

10.05   Tom Melham, Cambridge:  "A survey of recent applications of
the HOL theorem prover and developments in HOL-based research,
including an overview of work in progress on a mechanized theory of
the pi-calculus in higher order logic using HOL.

10.45   Konrad Slind, (visiting) Cambridge: Site Report: University of
Calgary

11.00   Eleanor Mayger, Abstract Hardware: "The LAMBDA/DIALOG design
assistant"

11.15   Coffee

11.30   Stuart Anderson, Edinburgh (LFCS): "Using Lambda to Reason about a
Shutdown System."

12.00   Mark Dawson, Imperial College: "An Overview of the Imperial Logic
Environment"

12.30   Zhaohui Luo, Edinburgh (LFCS): "The use of Type Theory as a
general language for specification, programming and reasoning, and the
use of the Lego system as an environment for the development of
programs and proofs.

1.00    Lunch followed by demo session

        Demos:  Imperial Software Technology's Genesis Z Tool and Proof System
                The Imperial (College) Logic Environment
                Abstract Hardware's Lambda/Dialog System
                The Lego System - Edinburgh

2.30    Alan Bundy, Edinburgh (AI):"Why inductive proof is crucial in the
application of formal methods and how it can be automated."

3.00    Harold Simmons, Manchester and SERC: Update on the Logic for
IT Initiative

3.15    "Proof" Club Business Meeting:  1. New Name
                                        2. Club Organisation
                                        3. Club Financing
                                        4. Club Subject Area
                                        5. Future Meetings
                                        6. Other Activities

3.30    Tea

3.45    Katherine Norrie, RHBNC, London: "Equational Reasoning for
LOTOS Specifications."

4.15    Brian Ritchie, Rutherford Appleton Labs: "A Sketch of MuRAL."


If you havn't already done so can you inform George Cleland at the
address below if you will be attending. There will be no charge for
this meeting.

George Cleland,
LFCS,
Dept. of Computer Science,
University of Edinburgh,
The King's Buildings,
Edinburgh EH9 3JZ
Tel (+44) 031-650-5199
Fax: (+44) 031-667-7209
E-mail: cleland@lfcs.ed.ac.uk

_____________________________________________________________________


                             "Proof" Club
                    Awareness Club in Computer Assisted
                             Formal Reasoning

To register an interest and ensure that you continue to receive
Information on the "Proof" Club please complete and return the
following details below for our records:


Name:

Organisation:

Address:


Telephone Number:

E-Mail Address:

Fax Number:


I shall/shall not be attending the 1st project meeting on 12th June.

Return this form to:

George Cleland,
Assistant Director,LFCS,
Dept. of Computer Science
University of Edinburgh
The King's Buildings,
Edinburgh
Tel  (+44) 031-650-5199
Fax:  (+44) 031-667-7209
E-mail: cleland@lfcs.ed.ac.uk