Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
To: isabelle-users@cl.cam.ac.uk, info-hol@cs.uidaho.edu, THEORYNT@NDSUVM1.EARN, 
    theorem-provers@mc.lcs.mit.edu, bra-types@cs.chalmers.se
Subject: Isabelle course, 1995
Date: Thu, 30 Mar 1995 10:23:55 +0100
From: Lawrence C Paulson <Larry.Paulson@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:050800:950330092415"@cl.cam.ac.uk>

Dear Colleague,

Please forward the attached announcement of a course on the theorem prover
Isabelle.  This is a repeat of the successful course held last summer.  It
will be held the week before Mathematics of Program Construction (MPC '95).
Please send technical questions to Larry.Paulson@cl.cam.ac.uk and
administrative ones to rjs1008@cus.cam.ac.uk.

A hypertext version is available via the URL

	http://www.cl.cam.ac.uk/users/lcp/isabelle-course.html

I apologize for multiple copies.

                                                        Larry Paulson

UNIVERSITY OF CAMBRIDGE
Programme for Industry

Introduction to Theorem Proving, using "Isabelle"

12-14 July 1995
Course fee 650 pounds sterling
          (350 pounds sterling for full time students and faculty of
               higher education institutes)

Accommodation 180 pounds sterling

AIM OF THE COURSE

Theorem proving systems are growing in popularity and are demonstrating
their utility in many fields: hardware/software verification, protocol
verification, program synthesis, artificial intelligence, and mathematics
research.  The aim of this course is to introduce participants to the
Isabelle system, developed at Cambridge University, and used since 1986 in
research establishments.

Isabelle has built-in support for several logics, including first-order
logic (FOL), higher-order logic (HOL), Zermelo-Fraenkel set theory (ZF) and
extensional Constructive Type Theory (CTT).  New logics can also be
introduced by specifying their abstract syntax, notation, and inference
rules.  This feature makes Isabelle uniquely flexible, applicable to many
domains.

OUTLINE OF THE COURSE

The course is highly practical, with a large proportion of teaching taking
place as hands-on sessions conducted on X workstations.  The lectures and
terminal sessions will enable participants to perform their own Isabelle
proofs in higher-order logic.  Main topics:

  Single-step proof checking.  Forward and backward proof.
  Declaring types and constants.  Quantifier reasoning.  
  Higher-Order Logic in Isabelle.  Advanced proof tools.

The course will be taught by Dr Lawrence Paulson, the originator of Isabelle.

WHO SHOULD ATTEND

The course is intended for researchers, academic and industrial, in the
fields of computer science and logic.  Participants must have experience
with X workstation environments and should also be familiar with elementary
logic.  Experience with a functional programming language such as ML would
be helpful, but not essential.

LECTURER

Dr Lawrence Paulson is a University Lecturer at the Computer Laboratory,
University of Cambridge.  He has a PhD in Computer Science from Stanford
University and a BS in Mathematics from the California Institute of
Technology.

His research concerns interactive theorem proving and its applications.
His modified version of Edinburgh LCF was adopted as the basis of both
the HOL system and Nuprl.  His Isabelle system is one of the most popular
generic theorem provers.  He has applied Isabelle to investigate uses for
formal set theory in specification and verification.

COURSE FEES AND ACCOMMODATION

The course fee is 650 pounds sterling (350 pounds for full time students and
faculty of higher education institutes) payable in advance and includes a full
set of course notes, a certificate of attendance, lunch, and day-time
refreshments for the duration of the course.  Accommodation can be arranged
for delegates in single college rooms with shared facilities at 180 pounds
sterling for 3 nights in Peterhouse college from Tuesday July 11, to include
bed and breakfast, dinner and a Course Dinner with wine.  If you would prefer
to make your own arrangements, please indicate on the registration form and
details of local hotels will be sent to you.

LOCATION

The course will be held at the Department of Engineering, University of
Cambridge.  Access to Cambridge by air is possible direct from Amsterdam, and
via Stansted Airport from many other European cities.  Frequent bus services
are available from Heathrow, Gatwick and Stansted Airports.  Rail and road
communications to Cambridge are excellent; however, car parking in Cambridge
is limited.  Full directions will be sent with course joining instructions.

REGISTRATIONS

The number of places available on the course are limited to 20.  You can
make a provisional reservation on the course by telephone, fax or e-mail.
All provisional places must be confirmed by returning a registration form to
the address below.  Bookings will be confirmed after payment has been received
in full.  Delegates will only be accepted onto a course if payment has been
received in full or an official company purchase order has been received.

METHODS OF PAYMENT

Payments should be made by
 Crossed international money order
 A cheque drawn on a UK bank
 VISA or Mastercard/Eurocard
 Sterling travellers' cheques

Any bank changes arising from international transactions must be met by the
delegate.  All payments to the University of Cambridge must be for the full
amount of fees incurred.  Personal cheques drawn on banks outside the UK will
not be accepted.  Please do not send cash.  Cheques or orders should be made
payable to University of Cambridge-EYA.

CANCELLATIONS

Half the registration fee will be returned for bookings cancelled up to one
calendar month in advance of the course.  After this time no fees are
returnable.  However, substitutions may be made at any time.  The Cambridge
Programme for Industry reserves the right to pass on any charges levied by a
College for cancellation of accommodation and meal bookings.


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

I wish to register for the course: Introduction to Theorem Proving, using
"Isabelle"

Title (Dr, Mr, Ms etc):
Name:
First Names:
Job Title:
Company:
Division:
Address:
Post Code:
Tel. No:
Fax. No:
E-mail address:

[ ] Please reserve one place.  I enclose a cheque/purchase order for _______
[650 or 350 pounds], made payable to the University of Cambridge/EYA.

[ ] Please reserve one place and accommodation for 3 nights.  I enclose a
cheque/purchase order for _______ [830 or 530 pounds], made payable to the
University of Cambridge/EYA.

[ ] Please send details of local hotels.

[ ] Please reserve one place at the Course Dinner (for delegates not resident
at Peterhouse College) @ 32 pounds sterling.

I have the following special requirements concerning diet or disabilities:

Total Amount Enclosed:  ____________

Return to :  The Registration Administrator 
University of Cambridge Programme for Industry,
1 Trumpington St, Cambridge CB2 1QA, England
Tel +44 (0)1223 302233
Fax +44 (0)1223 301122
e-mail: rjs1008@cus.cam.ac.uk