Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!yale!umich!ox.com!emv From: joyce@cs.ubc.ca (Jeffrey Joyce) Newsgroups: comp.archives Subject: [comp.software-eng] Cambridge HOL System - 5-day intensive course Keywords: formal specification/verification, machine-assisted proof Message-ID: <1991Jan3.223638.6351@ox.com> Date: 3 Jan 91 22:36:38 GMT References: <1991Jan3.174140.5525@cs.ubc.ca> Sender: emv@ox.com (Edward Vielmetti) Reply-To: joyce@cs.ubc.ca (Jeffrey Joyce) Followup-To: comp.software-eng Organization: University of British Columbia, Vancouver, B.C., Canada Lines: 141 Approved: emv@ox.com (Edward Vielmetti) X-Original-Newsgroups: comp.software-eng Archive-name: theory/logic/hol/1991-01-03 Archive: clover.ucdavis.edu:/pub/hol/hol111.tar.Z [128.120.57.1] Original-posting-by: joyce@cs.ubc.ca (Jeffrey Joyce) Original-subject: Cambridge HOL System - 5-day intensive course Reposted-by: emv@ox.com (Edward Vielmetti) 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.