joyce@cs.ubc.ca (Jeffrey Joyce) (01/04/91)
A FIVE-DAY INTENSIVE COURSE ON
*****************************
| The Cambridge HOL System |
*****************************
An Introduction to
Interactive Machine-Assisted
Theorem-Proving in Higher-Order Logic
April 29 - May 3, 1991
The University of British Columbia
Vancouver, Canada
Course Description
------------------
This is a five-day introductory course on using the Cambridge
HOL System - an interactive environment for machine-assisted
theorem-proving in higher-order logic. This system, developed
by researchers at Cambridge University, is currently in use at
sites in North America, Europe, Australia, China and Japan.
It is used for hardware verification, software verification,
protocol specification, and basic research into machine-
assisted formal proof. Specialized applications include both
safety-critical hardware and computer system security. Users
include academic and industrial researchers, and companies
doing contract proofs.
Who Will Benefit
----------------
This course will benefit researchers in both industrial and
academic settings with an interest in the development of
reliable hardware/software systems. A previous offering of
this course in June 1990 attracted participants from a variety
of organizations including Boeing, IBM France, British Telecom,
Mitre Corporation, Mitsubishi and Unisys.
A strong background in formal logic is NOT required, however,
some familiarity with the notation of predicate calculus would
be helpful. Experience with an interactive functional
programming language (such as Lisp) would also be helpful.
Course Instructors
------------------
RACHEL CARDELL-OLIVER, Research Student, Cambridge University,
and Australian Defence Science and Technology Organization,
(Protocol Specification and Verification).
JOHN HERBERT, SRI International, and Research Associate
Cambridge University (Specification and Verification of Digital
Hardware).
JEFFREY JOYCE, Assistant Professor, University of British
Columbia, (Specification and Verification of Microprocessor-
based Systems).
Course Format
-------------
Morning lectures will describe the HOL formulation of higher-
order logic and essential concepts for interactive, machine-
assisted proof (e.g., forward and backward proof styles).
Afternoon laboratory sessions will provide instruction on using
the HOL system to create formal specifications and generate
formal proofs. Course participants will have workstation
access to the HOL system for course exercises. A course
syllabus is available on request.
Obtaining the Cambridge HOL System
----------------------------------
The Cambridge HOL system is available as a PUBLIC DOMAIN system.
It can be obtained by remote file transfer from the University
of California at Davis:
anonymous FTP to clover.ucdavis.edu
login as "anonymous" (any password)
type "cd /pub/hol"
type "binary"
type "get hol111.tar.Z"
You will need either a public domain or commercial version of
Lisp (Franz Lisp or Common Lisp) to run the HOL system. A
public domain version of Franz Lisp is available by anonymous
FTP from UC Davis. Copies of the HOL system will be available
at the course (at cost for magnetic tape). Pre-ordered copies
of the three-volume HOL System Manual will also be available
(at cost for copying). Enquiries about the HOL System should
be directed to:
Sara Kalvala
Computer Laboratory
New Museums Site
Pembroke Street
Cambridge CB2 3QG England
e-mail: sk@cl.cam.ac.uk
Registration and Accommodation
------------------------------
Before March 18 After March 18
-------------------------------------
Regular Registration: Cdn $750 Cdn $825
Full-Time Students: Rates available on request
A limited number of on-campus suites have been block-booked
for the nights of April 27 to May 2. Each suite accommodates
1-3 people and consists of a bedroom (2 beds), a lounge area
(1 sofa-bed), full kitchen and bathroom. The price is $55.00
per suite per night plus provincial hotel tax.
Further information on registration and/or accommodation can
be requested from:
Ms. Vicki Ayerbe
Computer Science Programs
UBC CENTRE FOR CONTINUING EDUCATION
5997 Iona Drive
The University of British Columbia
Vancouver, B.C., V6T 2A4 CANADA
tel: (604) 222-5251
fax: (604) 222-5283
or by e-mail from:
joyce@cs.ubc.ca
Please specify postal address in your e-mail request.