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.