[Prev][Next][Index][Thread]
Isabelle course -- places still available
Dear Colleague,
Please forward the attached course announcement. The course is about the
theorem prover Isabelle. It will be held one week after LICS and two weeks
after CADE, to facilitate travel arrangements. Please send technical
questions to Larry.Paulson@cl.cam.ac.uk and administrative ones to
rt10005@phx.cam.ac.uk.
I apologize for multiple copies.
Larry Paulson
------------------------------------------------------------------------------
UNIVERSITY OF CAMBRIDGE
Programme for Industry
Introduction to Theorem Proving, using "Isabelle"
11-13 July 1994
Course fee 650 pounds sterling
(350 pounds sterling for academic participants)
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. The projected course outline
includes:
Single-step proof checking. How to perform rewriting.
Theory. Types and type classes. How to make simple definitions.
How to define new logics. 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.
COURSE FEES AND ACCOMMODATION
A 10% DISCOUNT CAN BE APPLIED TO THE COURSE FEE OF ANY
REGISTRATION PRIOR TO 1 MARCH 1994.
The course fee is 650 pounds sterling (350 pounds sterling for academics)
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 176 pounds sterling for 3 nights in
Peterhouse college from Sunday July 10, to include bed and breakfast,
dinner with wine and a Course Dinner. 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 and Gatwick 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 completing and returning the
tear-off slip below together with a company purchase order or full payment.
METHODS OF PAYMENT
Payments should be made by:
A cheque drawn on a UK bank
VISA or Mastercard/Eurocard
Sterling travellers' cheques
The University reserves the right to retrieve any bank charges or exchange
costs which arise from payments made in other ways (including Eurocheques).
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.
------------------------------------------------------------------------------
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 and accommodation for 3 nights.
I enclose a cheque/purchase order for _______, made payable to the
University of Cambridge/EYA.
_____ Please reserve one place and send details of local hotels.
I enclose a cheque/purchase order for _______, made payable to the
University of Cambridge/EYA.
_____ Please reserve one place at the Course Dinner (for delegates not
resident at Peterhouse College) @ 30 pounds sterling.
I have the following special requirements concerning diet or disabilities:
Total Amount Enclosed: ____________
Return to : The Course Administrator, Cambridge Programme for Industry,
University of Cambridge,
1 Trumpington St, Cambridge CB2 1QA
Tel no +44 (0)223 332722
Fax +44 (0)223 301122
e-mail: rt10005@phx.cam.ac.uk