Short Course at UBC: Cambridge HOL System

Date:  2 Apr 90 17:17 -0700

                     The Cambridge HOL System:

           An Introduction to Interactive Machine-Assisted
                Theorem-Proving in Higher-Order Logic

                    Monday-Friday, June 4-8, 1990
                      FIVE-DAY INTENSIVE COURSE

              Seminars and Lab Workshops to be held on
              The University of British Columbia Campus
                      (Vancouver Canada)

       Sponsored by:  The UBC Centre for Continuing Education and
       The UBC Centre for Integrated Computer Systems Research

Course Description:

This five-day course is an introduction to higher-order logic and use of
the Cambridge HOL System.  The HOL system is an interactive environment
for machine-assisted theorem-proving in higher-order logic.  This system
is currently in use at sites in North America, Europe, China and Japan.
It is used for hardware verification, software verification and basic
research into machine-assisted formal proof.  Users include both companies
doing contract proofs and researchers.

This course will be of particular interest to contractors developing
hardware/software systems to meet increasingly tough standards such as
the UK MoD Interim Defence Standard 00-55 for the development of safety-
critical software and the US DoD Trusted Computer Systems A1 security
classification (both requiring the use of formal verification techniques).

Morning lectures will describe the HOL formulation of higher-order logic
along with some examples of using higher-order logic to specify digital

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.

For more details on using the HOL system to verify digital hardware, see
"The Notion of Proof in Hardware Verification" (by Avra Cohn, Journal of
Automated Reasoning, Vol. 5, May 1989, pp. 127-139) which gives an account
of using the HOL system to partially verify the commercially-available
VIPER microprocessor.

Course Instructors:

Rachel Cardell-Oliver, Ph.D. Candidate, Cambridge University/Australian
Defence Science and Technology Organization, (Protocol Specification
and Verification).

John Herbert, Research Associate, Cambridge University/SRI Cambridge,
(Specification and Verification of digital hardware).

Jeff Joyce, Assistant Professor, University of British Columbia,
(Specification and Verification of microprocessor-based systems).

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 background in formal logic is NOT required, however, some
familiarity with the notation of predicate calculus would be helpful.
Experience with the use of an interactive functional programming language
(such as Lisp) would be very helpful.

Other Information:

The Cambridge HOL system is available as a public domain system. Copies
of the 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).

For further course information contact:

Jeff Joyce
Computer Science Department            Telephone: (604) 228-4327
The University of British Columbia     Fax: (604) 228-5485
6356 Agricultural Road                 Email: joyce@cs.ubc.ca
Vancouver, B.C. V6T 1W5

For information regarding registration contact:

Vicki Ayerbe
Computer Science Programs              Telephone: (604) 222-5251
Centre for Continuing Education        Fax: (604) 222-5283
5997 Iona Drive
Vancouver, B.C. V6T 2A4

Registration Information:

Course Location:   University of British Columbia Campus,
                   Vancouver, B.C., Canada

Pre-registration deadline:   May 7, 1990
                             Enrollment limited.

                                    Before May 7     After May 7
                                    ------------     -----------
Registration Fees:    Regular       $295.00          $345.00
                      Student       $150.00          $175.00

Also available by order: Software (magnetic tape):   $25.00*
                         Three Volume Manual:       $110.00*

                         * - public domain (copying costs only)

Ways to Register !

Mail your cheque (payable to UBC) along with yhour registration form
(attached below).

In Canada only: Use your VISA or MASTERCARD and register by telephone,
(604) 222-5251, or by FAX at (604) 222-5283, 10am - 4pm, Monday-Friday.

Cancellation Policy:  Notice of participant cancellation must be in
writing and must be received by the Centre for Continuing Education
two weeks prior to the course starting date to qualify for a refund
(a full refund less $50.00 cancellation fee).  No refund will be
made for cancellation received after that time.  The course may
be cancelled by May 14 due to insufficient registrations.

-------------------- CUT HERE --------------------------------------

Accommodation Information and Registration Form

                    Walter Gage Residence

Single bedrooms are arranged apartment style (each apartment contains
six private bedrooms with a single bed) with one large shared washroom,
a lounge area with refrigerator and a balcony.

Accommodation payment is requested upon check-in by cash, traveller's

NAME:            ____________________________________________________

ADDRESS:         ____________________________________________________


TELEPHONE:       ____________________________________________________

ARRIVAL DATE:    __________________ DEPARTURE DATE: _________________

Check-in time: 1400 hours (2 pm)   Check-out time: 1100 hours (11 am)


Single Bedroom (sharing washroom and lounge)             $28.00/night
A deposit is not required.
A provincial hotel tax, currently 8%, is added to the above rate.

Send this reservation request form to:

                      UBC Conference Centre
                     5961 Student Union Mall
                Vancouver, B.C., V6T 2C9 Canada

                   Telephone:  (604) 228-2963
                   Fax:  (604) 228-5297

-------------------- CUT HERE --------------------------------------

Course Registration Form

The Cambridge HOL System                                 CS 5012-290

LAST NAME                                  FIRST NAME

ADDRESS                                     CITY/TOWN

Registration Fee:     $______________

Software (optional):  $______________

Manual (optional):    $______________

TOTAL:                $______________

Method of Payment

          Cheque/Money Order (Payable to UBC)
          Cash (For Registration in person)

          VISA Card __________________________

          MASTERCARD _________________________

Valid Date: ______________ Expiry Date: ______________


I authorize UBC to charge the above amount to my credit card

Signature _____________________________________________________

Name of person paying for program (s) (if different than registrant)

Mail completed registration form to: