Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) outside ac.uk; Sun, 4 Apr 1993 20:47:59 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA21756; Sun, 4 Apr 93 12:29:34 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from grolsch.cs.ubc.ca by ted.cs.uidaho.edu (16.6/1.34) id AA21751; Sun, 4 Apr 93 12:29:20 -0700 Received: by grolsch.cs.ubc.ca id AA16636 (5.65c/IDA-1.3.5 for info-hol@ted.cs.uidaho.edu); Sun, 4 Apr 1993 12:29:10 -0700 Date: 4 Apr 93 12:29 -0700 From: hug93 To: info-hol , cdn-soft-eng , lics-email Message-Id: <32*hug93@cs.ubc.ca> Subject: HUG'93 Announcement and call-for-participation First Call for Participation 1993 International Meeting on H I G H E R O R D E R L O G I C T H E O R E M P R O V I N G A N D I T S A P P L I C A T I O N S August 10-13 1993 The University of British Columbia Vancouver - Canada ============================================================================== This scientific meeting is the sixth in a series of annual workshops devoted to topics of higher order logic theorem proving, its usage in the HOL system and its applications. Previous workshops took place in Cambridge UK, Aarhus Denmark, Davis USA and Leuven Belgium. The HOL system is a higher order logic theorem proving system originally implemented at Cambridge University. It has found many applications, from verification of hardware designs at various levels to verification of software and communication protocols. Program ======= The program consists of sessions for technical presentations and sessions for invited speakers and demonstrations. The program committee invites submissions in the following areas: * Extensions/enhancements of the HOL system; * Other formalisms in comparison with the HOL formulation of higher-order logic; * Other theorem-provers in comparison with the HOL system; * Applications of the HOL system; * Implementation issues (e.g. efficiency, integrity, usability, interoperability) for the HOL system and other related systems. The deadline for paper submission is May 1, 1993. The Call-for-Papers announcement is available by anonymous ftp at cs.ubc.ca:/ftp/local/hug93, see CFPapers1.{txt|ps} or CFPapers2.{txt|ps}. Tutorials ========= Two parallel 1-day tutorials will be offered on Tuesday, August 10: (a) Introduction to the HOL System and Its Applications. ---------------------------------------------------- This tutorial will provide an introduction to the notation of higher-order logic and its principles of definition and formal reasoning. Part of the tutorial will describe how the notation of higher-order logic can be used as a specification language for a variety of application domains. The tutorial will also explain how other formalisms and specification languages can be embedded semantically inside higher-order logic allowing the HOL System to be used as a software tool for developing rigorous interfaces between a variety of formalisms and/or specification languages. The tutorial will include some hands-on laboratory exercises. This 1-day tutorial is intended mainly for HUG'93 participants who might not necessarily be familiar with the HOL System and would benefit from an overview of the system in preparation for participation in the workshop. (b) Introduction to the NaDSet and its Applications. ------------------------------------------------ NaDSet is a natural deduction-based set theory and logic that formalizes logical connectives, quantifiers and set abstraction through rules of deduction rather than axioms. NaDSet is particularly useful for the definition of inductively defined sets. Induction rules can be derived from these inductive definitions rather than being introduced as primitive rules of reasoning. In particular NaDSet provides a logical foundation for structured operational semantics, for category theory and for non-well-founded sets. In addition to a discussion of NaDSet, the tutorial will describe experience in building and using a theorem-prover implemented in a commercial-based Meta-CASE tool, the REFINE System from Reasoning Systems, Inc. This 1-day tutorial is offered to HUG'93 participants as an alternative to the above "Introduction to the HOL System and Its Application" tutorial. Formal Hardware Verification Course -- August 4-6 =================================================== An intensive 3-day course on formal hardware verification will be held August 4-6 at UBC. The course instructors, J. Joyce and C-J. Seger, will describe methods such as symbolic simulation, trajectory evaluation and model checking which complement the strengths of theorem-proving based approaches. This course will also describe how theorem-proving methods can be combined with these other formal approaches to obtain hybrid approaches to formal hardware verification. This course will include hands-on laboratory exercises. A description of this course and registration information is available by anonymous ftp at cs.ubc.ca:/ftp/local/hug93, see FHV.{txt|ps}. Although the course is organized separately from HUG'93, it has been scheduled in conjunction with HUG'93 for the convenience of those who may wish to participate in both events. Fees, Registration and Accommodation ==================================== The registration fee for the 1-day tutorials is CDN$35 for registration by June 21 and CDN$50 for registration after June 21. The registration fee for the 3-day HUG'93 workshop is CDN$275 for regular registration before June 21 and CDN$350 for late registration after June 21. Students may register in a tutorial for CDN$25 and in the workshop for CDN$150 at any time. Prospective participants should use a copy of the HUG'93 registration form to register in a tutorial and/or the workshop. This form is available by anonymous ftp at cs.ubc.ca:/ftp/local/hug93, see HUG93Reg.{txt|ps}. A limited number of rooms (private bedroom, shared bathroom) have been reserved for HUG'93 participants at $32 per night plus taxes. Twin accommodation may also be available at a reduced rate. This accommodation should be booked before July 20. Prospective participants should use a copy of the "request for accommodation" form to make accommodation arrangements. This form is available by anonymous ftp at cs.ubc.ca:/ftp/local/hug93, see Accommodation.{txt|ps}. Prospective participants seeking other accommodation (e.g., private bathroom, rooms for families, etc) should apply directly to the UBC Conferences Centre Administration Office at 5961 Student Union Blvd., University of British Columbia, Vancouver, B.C. Canada V6T 2C9, tel: (604) 822-1010, fax: (604) 822-1001. Student Travel Bursaries: ========================= A limited number of student travel bursaries are expected to be offered to full-time students. Students may apply to the HUG'93 organizing committee for a travel bursary. The application must consist of: * a statement that it is your intention to attend the workshop; * an estimate of your travel expenses (registration, accommodation, meals, airfare, ground transportation, etc); * a statement of what portion of these travel expenses you are prepared to cover with funds that you expect to receive from other sources; * a letter of recommendation from your supervisor confirming that you "will be a full-time student in August 1993". Applications for a student bursary must be received by May 30. They should be sent to Dr. J. Joyce by regular post to The Department of Computer Science, University of British Columbia, Vancouver, B.C., Canada, V6T 1Z2 or by fax to (604) 822-5485. Preference will be given to students who have submitted a paper to the workshop and to students who propose to cover a significant portion of their travel expenses with funds from other sources. The organizing committee expects to announce some bursaries by June 21. Additional bursaries may be announced at a later date. Airline Discounts ================= Air Canada is the official airline of HUG'93 and related events. In Canada and the United States, save up to 50% on economy fare, or 15% on excursion fare. It is our understanding that a "Saturday overnight stay" is not required on flights with a 15% discount. To take advantage of these savings, please call, in Canada and US, Air Canada 1-800-361-7585, or your travel agent. When purchasing tickets, please ask that CV930099 (the conference number of HUG'93 and its related events) be entered in the Tour Code box and UBC in the Endorsement box, regardless of the fare basis. Participants travelling from Europe should contact one of the following Air Canada offices: Frankfurt 25-01-31; Geneva 731-4980; London (081)-7592636; Paris (1) 43201200; Vienna (0222) 5861909 and Zurich 2110777. IMPORTANT DATES =============== * Deadline for paper submissions: May 1, 1993 * Deadline for student travel bursary application: May 30, 1993 * Deadline for panel proposals: June 1, 1993 * Deadline for advanced registration: June 21, 1993 * Hardware Verification Course: August 4-6, 1993 * HOL/NaDSet tutorials: August 10, 1993 * HOL Workshop: August 11-13, 1993 For more information about the workshop, please send your enquiry to: Email: hug93@cs.ubc.ca (Preferred) FAX: (604)-822-5485 Phone: (604)-822-6176 A copy of this announcement (ascii and Postscript versions) along with additional information (including future announcements) will be available by anonymous ftp at cs.ubc.ca:/ftp/local/hug93, see README. Registration Form (HUG'93 and Tutorials) August 10-13, 1993 The University of British Columbia Vancouver B.C. CANADA Before June 21st After June 21 Students ________________ _____________ ________ HOL/NaDSet Tutorials CDN$35 CDN$50 CDN$25 HUG'93 CDN$275 CDN$350 CDN$150 (Fees for students are the same before and after June 21.) Name _________________________________________________________________ FIRST MIDDLE LAST Organization _________________________________________________________ Department ___________________________________________________________ Address ______________________________________________________________ City____________________ State/Province_____________ Country__________ Phone______________________________ FAX_______________________________ Email_________________________________________________________________ I plan to attend [ ] HOL Tutorial (August 10, 1993) [ ] NaDSet Tutorial (August 10, 1993) [ ] HUG'93 (August 11-13, 1993) and pay by [ ]VISA [ ]MASTERCARD [ ]Travelers' Cheque [ ]Personal Cheque Amount: CDN$________________________________ Credit Card Number: __________________________________________________ Expiration Date: ______________ Signature: ___________________________ Payment must be in Canadian funds. Please make your cheque payable to: The University of British Columbia The registration fee covers the costs of HOL/NaDSet Tutorials (August 10) * Lecture materials. * Access to computing facilities. * Continental breakfast and lunch. HUG'93 (August 11-13) * One copy of the workshop proceedings. * Continental breakfast and lunch (Aug 11-13). * Coffee/tea during the workshop. * Workshop banquet at Cecil Green on Aug 12th. Please mail registration form to: Ms. Vicky Ayerbe University of British Columbia Continuing Studies Computer Science Programs 5997 Iona Drive Vancouver, BC V6T 1Z1 CANADA Cancellation: registration fee (minus $25) can be refunded any time before July 20, 1993. Please send your request to the above address. For more information about the workshop and the related events, please contact: Email: hug93@cs.ubc.ca (Preferred) FAX: (604)-822-5485 For registration information, please contact: Email: vayerbe@cce.ubc.ca FAX: (604)-222-5249 Phone: (604)-222-5256 A copy of this registration form (Ascii, and PS versions) along with additional information (including future announcements) will be available by anonymous ftp at cs.ubc.ca:/ftp/local/hug93, see HUG93Reg.{txt|ps}. University of British Columbia Request for Accommodation at Ritsumeikan A *limited* number of rooms have been reserved for participants in the Formal Hardware Verification Course and the 1993 HOL Users Group Meeting. This accommodation is located in the Ritsumeikan Residence (a new residence opened mid-1992) located within 5-10 minutes of course/tutorial/workshop locations. Reserved rooms are single bedrooms sharing a common kitchen, living area and washroom with three other single bedrooms. The rate is CAN$32 per night, plus applicable taxes. Some twin accommodation may also be available at a reduced rate. Groups of two, three or four participants who would like to share common facilities should indicate this on each application and, if possible, submit their individual applications together as a single package. When communicating with the UBC Conference Centre (other than a copy of this form), please use the following the identification codes: For accommodation between August 3-8: "HOL Users 1, T30803A". For accommodation between August 8-11: "HOL Users 2, T30808B". For accommodation between August 10-15: "HOL Users 3, T30810A". Payment can be made in Canadian or US funds at check-in by cash, travellers' cheques, VISA or Mastercard. We are unable to accept personal cheques. Please fill out this form and send it to: UBC Conference Centre Reservations Office 5961 Students Union Blvd. Vancouver B.C. V6T 2C9 CANADA (604)-822-1001 (FAX) (604)-822-1010 (phone, for enquiry only) Other accommodation may also be arranged. Please contact the UBC Conference Center directly at the above address. You are advised to make early arrangements for accommodation because on-campus accommodation is limited and very popular in August. Accommodation for this course will only be reserved until July 20, 1993. Last Name First Name ___________________________ __________________________ Address: __________________________________________________________________________ __________________________________________________________________________ City State/Province Zip _____________________ _______________ ______________ Country Phone ___________________________ __________________________________ Arrival: Departure: __________________________ ____________________________ Month/Date/Year Month/Date/Year (Check in time: 2pm, Check out time: 11am)