[comp.specification] 5-day Course on Cambridge HOL System

joyce@cs.ubc.ca (Jeffrey Joyce) (03/23/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 Idaho:

        anonymous FTP to ted.cs.uidaho.edu
        login as "anonymous" (any password)
        type "cd /pub/hol"
        type "binary"
        type "get hol.tar.Z"

A detailed description of the HOL system can also be obtained
by anonymous FTP (in PS format):

        type "get HOLSYS.ps.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
------------------------------

Regular Registration:  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.

msaltzman@vms.macc.wisc.edu (04/07/91)

In article <1991Mar22.164859.23479@cs.ubc.ca>, joyce@cs.ubc.ca (Jeffrey Joyce) writes...

> 
>              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 Idaho:
> 
>        anonymous FTP to ted.cs.uidaho.edu
>        login as "anonymous" (any password)
>        type "cd /pub/hol"
>        type "binary"
>        type "get hol.tar.Z"
> 
>A detailed description of the HOL system can also be obtained
>by anonymous FTP (in PS format):
> 
>        type "get HOLSYS.ps.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
>------------------------------
> 
>Regular Registration:  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.