3 Feb 1994 10:55
Isabelle course -- places still available
Lawrence C Paulson <Larry.Paulson@...>
1994-02-03 09:55:23 GMT
1994-02-03 09:55:23 GMT
Dear Colleague, Please forward the attached course announcement. The course is about the theorem prover Isabelle. It will be held one week after LICS and two weeks after CADE, to facilitate travel arrangements. Please send technical questions to Larry.Paulson@... and administrative ones to rt10005@... I apologize for multiple copies. Larry Paulson ------------------------------------------------------------------------------ UNIVERSITY OF CAMBRIDGE Programme for Industry Introduction to Theorem Proving, using "Isabelle" 11-13 July 1994 Course fee 650 pounds sterling (350 pounds sterling for academic participants) AIM OF THE COURSE Theorem proving systems are growing in popularity and are demonstrating their utility in many fields: hardware/software verification, protocol verification, program synthesis, artificial intelligence, and mathematics research. The aim of this course is to introduce participants to the Isabelle system, developed at Cambridge University, and used since 1986 in research establishments. Isabelle has built-in support for several logics, including first-order logic (FOL), higher-order logic (HOL), Zermelo-Fraenkel set theory (ZF) and extensional Constructive Type Theory (CTT). New logics can also be introduced by specifying their abstract syntax, notation, and inference rules. This feature makes Isabelle uniquely flexible, applicable to many domains. OUTLINE OF THE COURSE The course is highly practical, with a large proportion of teaching taking place as hands-on sessions conducted on X workstations. The lectures and terminal sessions will enable participants to perform their own Isabelle proofs in higher-order logic. The projected course outline includes: Single-step proof checking. How to perform rewriting. Theory. Types and type classes. How to make simple definitions. How to define new logics. Advanced proof tools. The course will be taught by Dr Lawrence Paulson, the originator of Isabelle. WHO SHOULD ATTEND The course is intended for researchers, academic and industrial, in the fields of computer science and logic. Participants must have experience with X workstation environments and should also be familiar with elementary logic. Experience with a functional programming language such as ML would be helpful, but not essential. COURSE FEES AND ACCOMMODATION A 10% DISCOUNT CAN BE APPLIED TO THE COURSE FEE OF ANY REGISTRATION PRIOR TO 1 MARCH 1994. The course fee is 650 pounds sterling (350 pounds sterling for academics) payable in advance and includes a full set of course notes, a certificate of attendance, lunch, and day-time refreshments for the duration of the course. Accommodation can be arranged for delegates in single college rooms with shared facilities at 176 pounds sterling for 3 nights in Peterhouse college from Sunday July 10, to include bed and breakfast, dinner with wine and a Course Dinner. If you would prefer to make your own arrangements, please indicate on the registration form and details of local hotels will be sent to you. LOCATION The course will be held at the Department of Engineering, University of Cambridge. Access to Cambridge by air is possible direct from Amsterdam, and via Stansted Airport from many other European cities. Frequent bus services are available from Heathrow and Gatwick Airports. Rail and road communications to Cambridge are excellent; however, car parking in Cambridge is limited. Full directions will be sent with course joining instructions. REGISTRATIONS The number of places available on the course are limited to 20. You can make a provisional reservation on the course by telephone, fax or e-mail. All provisional places must be confirmed by completing and returning the tear-off slip below together with a company purchase order or full payment. METHODS OF PAYMENT Payments should be made by: A cheque drawn on a UK bank VISA or Mastercard/Eurocard Sterling travellers' cheques The University reserves the right to retrieve any bank charges or exchange costs which arise from payments made in other ways (including Eurocheques). Personal cheques drawn on banks outside the UK will not be accepted. Please do not send cash. Cheques or orders should be made payable to University of Cambridge/EYA. CANCELLATIONS Half the registration fee will be returned for bookings cancelled up to one calendar month in advance of the course. After this time no fees are returnable. However, substitutions may be made at any time. ------------------------------------------------------------------------------ I wish to register for the course: Introduction to Theorem Proving, using "Isabelle" Title (Dr, Mr, Ms etc): Name: First Names: Job Title: Company: Division: Address: Post Code: Tel. No: Fax. No: E-mail address: _____ Please reserve one place and accommodation for 3 nights. I enclose a cheque/purchase order for _______, made payable to the University of Cambridge/EYA. _____ Please reserve one place and send details of local hotels. I enclose a cheque/purchase order for _______, made payable to the University of Cambridge/EYA. _____ Please reserve one place at the Course Dinner (for delegates not resident at Peterhouse College) <at> 30 pounds sterling. I have the following special requirements concerning diet or disabilities: Total Amount Enclosed: ____________ Return to : The Course Administrator, Cambridge Programme for Industry, University of Cambridge, 1 Trumpington St, Cambridge CB2 1QA Tel no +44 (0)223 332722 Fax +44 (0)223 301122 e-mail: rt10005@...