Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) 
          id <21568-0@swan.cl.cam.ac.uk>; Thu, 11 Jun 1992 07:23:29 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA05890;
          Wed, 10 Jun 92 23:13:32 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from n-kulcs.cs.kuleuven.ac.be by ted.cs.uidaho.edu (16.6/1.34) 
          id AA05885; Wed, 10 Jun 92 23:13:13 -0700
Received: from gpx3u.esat.kuleuven.ac.be 
          by n-kulcs.cs.kuleuven.ac.be (5.65b/n_kulcs1.1) id AA00581;
          Thu, 11 Jun 92 08:12:02 +0200
Date: Thu, 11 Jun 92 08:13:41 +0100
Message-Id: <9206110713.AA09195@esat.kuleuven.ac.be>
Original-Received: by esat.kuleuven.ac.be Thu, 
                   11 Jun 92 08:13:42 +0100
PP-warning: Illegal Received field on preceding line
From: claesen@be.imec
To: infohol@m.
Subject: Reminder: Paper contributions for |- HOL-92 !

==============================================================================
                        Call for Papers & Participation

                             21-24 September 1992
                        1992 International Workshop 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.

              in cooperation with: ESPRIT CHEOPS BRA, IFIP 10.2
                          IMEC - Leuven - Belgium

==============================================================================

This scientific meeting is the fifth in a series of annual workshops focusing  
arround the topic of higher order logic theorem proving, its usage in the HOL 
system and its applications. Previous workshops have taken place in Cambridge 
UK, Aarhus Denmark and Davis California.

The HOL system is a higher order logic theorem proving system implemented at
Cambridge University.  It has found many applications, from the verification 
of hardware designs at all levels to the verification of programs and 
communication protocols. Besides HOL, also contributions and experiences with 
other implementations of higher order logic are welcomed.

TOPICS. 
=======

Papers are invited related to all topics concerning higher order logic theorem 
proving and its applications in HOL and/or other higher order logic based 
theorem provers. This includes, but is not limitted to the following subjects:

* Formal Hardware Design and Verification. 
* Formal Software Design and Verification. 
* System Level Verification.
* Transformational Design.
* Hardware / Software co-Design.
* Basic Proof Techniques and Developments.
* Industrial applications of higher order logic proving.
* Trade off Theorem Proving / OBDD's.
* Efficient implementations of higher order logic.
* Embedding other formalisms in higher order logic.
* Interfacing with hardware description languages.
* User interface aspects of interactive proof.
* Practical experiences.

Authors should send seven copies of either an extended abstract or a full 
paper describing the proposed presentation to the workshop chair. 
Electronic mail submissions in PostScript format will also be accepted.
Accepted papers will be published in Proceedings by North-Holland.

For proposals of tutorials, demonstrations and panel sessions please send an 
abstract description to the workshop chair.

IMPORTANT DATES
===============

* 15 June 1992: deadline for paper submissions.
* 10 August 1992: notification of acceptance.  
* 4 September 1992: camera ready copy.
* 21-24 September 1992: workshop.

PROGRAM COMMITTEE:
==================

* Myla Archer  (University of California, Davis, USA) 
* Graham Birtwistle  (University of Calgary, CA) 
* Holger Bush (Siemens AG, D)   
* Albert Camilleri (Hewlett-Packard, UK) 
* Shui-Kai Chin  (Syracuse University, USA) 
* Luc Claesen  (IMEC / Kath. Univ. Leuven, B) 
* Simon Finn (Abstract Hardware Ltd., UK) 
* Michael Gordon  (University of Cambridge, UK) 
* Elsa L. Gunter  (AT\&T Bell Labs, USA) 
* John Herbert  (SRI International, UK) 
* Roger B. Jones  (ICL Defence Systems, UK) 
* Jeff Joyce  (University of British Columbia, CA) 
* Ton Kalker (Philips, NL) 
* Matt Kaufmann (Computational Logic Inc., USA) 
* Kurt Keutzer (Synopsys, USA) 
* Ramayya Kumar (Univ. of Karlsruhe, D) 
* Miriam Leeser (Cornell University, USA) 
* Tim Leonard (Digital Equipement Corp., USA) 
* Paul Loewenstein  (Sun Microsystems, USA)  
* Tom Melham  (University of Cambridge, UK) 
* Carl Seger (University of British Columbia, CA) 
* David Shepherd (Inmos Ltd., UK) 
* Gerd Venzl (Siemens AG, D) 
* Phillip J. Windley  (University of Idaho, USA) 

ORGANIZATION
============

Workshop Chair	 			Workshop co-Chair
Luc Claesen   				Michael Gordon
IMEC / K.U.Leuven 			University of Cambridge
Kapeldreef 75 				Computer Laboratory
B-3001 Leuven 				Pembroke Street
Belgium 				Cambridge CB2 3QG
phone: +32-16-281203 			U.K.
fax:   +32-16-281515 			email: mjcg@cl.cam.ac.uk
email: claesen@imec.be

LOCAL ARRANGEMENTS
==================
Annemie Stas 
IMEC - Kapeldreef 75 
B-3001 Leuven Belgium 
phone: +32-16-281201 
fax: +32-16-281515 
email: annemie@imec.be

Please include in all your correspondence, your postal address, phone, fax
and email.

==============================================================================
