Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!uakari.primate.wisc.edu!zazen!news
From: msaltzman@vms.macc.wisc.edu
Newsgroups: comp.specification
Subject: Re: 5-day Course on Cambridge HOL System
Message-ID: <1991Apr7.021914.21933@macc.wisc.edu>
Date: 7 Apr 91 02:19:25 GMT
Sender: news@macc.wisc.edu (USENET News System)
Organization: University of Wisconsin Academic Computing Center
Lines: 140

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.