schubert@gourami.eecs.ucdavis.edu (Tom Schubert) (04/24/91)
CALL FOR PARTICIPATION The 1991 International Tutorial and Workshop on the HOL Theorem Proving System and Its Applications Davis, California, USA August 27 and August 28-30, 1991 The HOL system is a higher-order-logic theorem proving system implemented at Cambridge University using methods developed at Edinburgh University. It has found many applications, from the verification of hardware designs at all levels to the verification of programs and communication protocols. This workshop is intended to bring together developers, users, potential users, and others interested in the HOL theorem proving system to share information on new development, extensions, and applications of HOL, and to discuss future directions for improvements to HOL and its interfaces. The 3-day workshop will be preceded by a full-day tutorial on August 27th, consisting of presentations by a panel of invited HOL experts on a range of topics including: an overview of the system; a survey of applications; comparison of HOL with other interactive verification systems; what helps and what hinders new users; the integration of HOL with existing methodologies, tools and environments. This tutorial is designed for an audience not necessarily familiar with the HOL system or its applications; it is intended primarily to give prospective users an informed basis for evaluating the HOL system and its potential. Papers are invited concerning new developments and extensions to HOL, applications of HOL, including proof techniques, user interfaces for HOL and interfaces between HOL and other systems, comparison of HOL with other verification systems, and progress in other higher-order-logic proving systems. Panel proposals on these topics also will be entertained. Authors should send seven copies of a 1000 word abstract or panel proposal to the HOL91 program coordinator, Phil Windley. Electronic mail submissions in PostScript format will also be accepted, for the convenience of European and other overseas participants. Abstracts or proposals must be received by May 29, 1991. Notification of acceptance will be made by July 1, 1991. Papers accepted for the workshop will be published in a Proceedings. Non-authors are also encouraged to participate in the tutorial and/or workshop; those wishing to attend should communicate with Myla Archer. Travel scholarships for amounts up to $1,000 may be available for full-time students, awarded on a competitive basis. For details, write to Jeff Joyce. Co-sponsors: Keynote Speakers: IEEE Computer Society Matt Kaufmann (Computational Logic Inc.) ACM SIGDA Kurt Keutzer (Synopsis Inc.) University of California, Davis John Rushby (SRI International) University of Idaho University of British Columbia Program Committee: Myla Archer (University of California, Davis) Graham Birtwistle (University of Calgary) Shui-Kai Chin (Syracuse University) Luc Claesen (IMEC / Kath. Univ. Leuven) Avra Cohn (University of Cambridge) Michael Gordon (University of Cambridge) Elsa Gunter (AT&T Bell Labs) John Herbert (University of Cambridge) Roger Jones (ICL Defence Systems) Jeff Joyce (University of British Columbia) Karl Levitt (University of California, Davis) Paul Loewenstein (Mitsubishi / Stanford University) Tom Melham (University of Cambridge) Phil Windley (University of Idaho) Glynn Winskel (Aarhus University) Organizing Committee: Myla Archer (General Chair) Karl Levitt (Financial Chair) Division of Computer Science Division of Computer Science University of California, Davis University of California, Davis Davis, CA 95616, USA Davis, CA 95616, USA archer@eecs.ucdavis.edu levitt@eecs.ucdavis.edu (916) 752-7583 (916) 752-0832 fax: (916) 752-4767 fax: (916) 752-4767 Jeff Joyce (Tutorials Chair) Phil Windley (Program Chair) Department of Computer Science Department of Computer Science University of British Columbia University of Idaho Vancouver, BC V6T 1W5, CANADA Moscow, ID 83843, USA joyce@cs.ubc.ca windley@cs.uidaho.edu (604) 228-4327 (208) 885-6501 fax: (604) 228-5485 fax: (208) 885-6645 Local Arrangements Committee: Meshell Robinson (Chair) robinson@cs.ucdavis.edu (916) 752-1974 George Fink gfink@cs.ucdavis.edu (916) 752-8285 Tom Schubert schubert@cs.ucdavis.edu (916) 752-6452 Location and Accomodations: Davis is a small university town. Its warm summer weather is conducive to recreational activities such as tennis, cycling and swimming. Workshop participants will have access the extensive recreational facilities of the University. Bicycles can be rented for rides to the country surrounding the Campus. San Francisco is a 90 minute drive to the West and the northern Sierra Nevada Peaks are within 2 hours to the East. Within 1 hour is the Napa Valley wine country. A block of rooms at Davis motels within easy walking distance of the Campus have been reserved. Details will be sent to registrants.