Return-Path: <info-hol-request@lal.cs.byu.edu>
Delivery-Date: 
Received: from bescot.cl.cam.ac.uk (user exim (mailer)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Wed, 20 Dec 1995 11:35:57 +0000
Received: from leopard.cs.byu.edu [128.187.2.182] by bescot.cl.cam.ac.uk 
          with esmtp (Exim 0.25 #7) id E0tSMns-00035p-00;
          Wed, 20 Dec 1995 11:35:24 +0000
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA163008202;
          Wed, 20 Dec 1995 01:30:02 -0700
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Received: from ra.abo.fi by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) 
          id AA162968182; Wed, 20 Dec 1995 01:29:42 -0700
Received: from xerxes.abo.fi (listen@xerxes.abo.fi [130.232.209.104]) 
          by ra.abo.fi (8.6.10/8.6.10) with ESMTP id KAA29194;
          Wed, 20 Dec 1995 10:28:32 +0200
From: Jockum von Wright IB <jwright@ra.abo.fi>
Received: (listen@localhost) by xerxes.abo.fi (8.6.10/8.6.10) id KAA26366;
          Wed, 20 Dec 1995 10:29:22 +0200
Date: Wed, 20 Dec 1995 10:29:22 +0200
Message-Id: <199512200829.KAA26366@xerxes.abo.fi>
To: info-hol@leopard.cs.byu.edu, theory@cl.cam.ac.uk, hvg@cl.cam.ac.uk, 
    ucam.cl.isabelle@cl.cam.ac.uk, fsdm-real@cs.uq.oz.au, qed@mcs.anl.gov, 
    pvs@csl.sri.com, ifip-10.5@ics.UCI.EDU
Subject: Call for Papers - Conference on Theorem Proving in Higher Order Logics




                              CALL FOR PAPERS:

                    THE 1996 INTERNATIONAL CONFERENCE ON

                   THEOREM PROVING IN HIGHER ORDER LOGICS

BACKGROUND

 The 1996 International Conference on Theorem Proving in Higher Order Logics
 will be the ninth conference in a series dating back to 1988.  The Conference
 will be held on 27-30 August 1996 (Tuesday to Friday) in Turku, in south-west
 Finland.  Previous conferences have been held in Cambridge (UK), Arhus, Davis,
 Leuven, Vancouver, Malta and Salt Lake City.
 
TOPICS

 The programme committee welcome submissions on all aspects of theorem proving,
 particularly those relating to higher order logics or to proof systems based
 on secure mechanizations of logic.  This includes, but is not limited to, the
 following areas:

  o advances in theorem proving technology
  o proof automation and decision procedures
  o applications of mechanized theorem proving
  o development and extension of higher order logics
  o comparisons between various approaches to theorem proving
  o exploitation of external tools within theorem provers
  o incorporation of theorem provers into larger systems
  o novel industrial applications of theorem provers

SUBMISSION

 Submissions are invited in the following categories:

  o Category A: Full research paper
  o Category B: Informal progress report

 Submissions under category A will be fully refereed, and accepted papers
 published in the conference proceedings.  Submissions accepted under
 category B will be distributed in an informal proceedings at the workshop.
 Unless otherwise requested, submissions rejected under category A will
 also be considered for inclusion under category B.  Submissions under 15
 pages are preferred.

 Email submissions may be sent to the organizing committee at orgcom@abo.fi.
 PostScript format is preferred. All submissions will be promptly acknowledged.
 Papers may also be physically sent to any member of the organizing committee
 at the following address: 

                     Department of Computer Science
                     Abo Akademi University
                     Lemminkaisenkatu 14A
                     FIN-20520  Turku
                     FINLAND

 In this case, please include five (5) copies of each paper.

IMPORTANT DATES

  o Deadline for category A submissions:                15 March 1996
  o Deadline for category B submissions:                14 April 1996
  o Notification of acceptance:                         30 April 1996
  o Camera-ready copy for category A due (provisional): 14 June  1996
  o Conference:                                         27-30 August 1996

PROGRAMME COMMITTEE

 The programme committee for the conference will include:

  o Flemming Andersen (Tele Danmark)
  o Albert Camilleri  (Hewlett-Packard)
  o Tony Cant         (DSTO)
  o Elsa Gunter       (AT&T)
  o Joshua Guttman    (MITRE)
  o John Herbert      (SRI Cambridge)
  o Paul Jackson      (Edinburgh)
  o Ramayya Kumar     (FZI Karlsruhe)
  o Tim Leonard       (DEC)
  o Paul Loewenstein  (Sun)
  o Tom Melham        (Glasgow)
  o Tobias Nipkow     (TU Munchen)
  o Christine Paulin  (ENS Lyon)
  o Larry Paulson     (Cambridge)
  o Tom Schubert      (Portland State)
  o David Shepherd    (SGS-THOMSON)
  o Phil Windley      (BYU)
  o Joakim von Wright (Abo Akademi)

CONFERENCE ORGANIZATION

 The conference is being organized by the Turku Centre for Computer Science
 (TUCS) and Abo Akademi University.  The organizing committee is as follows:

  o Jim Grundy
  o John Harrison
  o Gundel Westerholm
  o Joakim von Wright (Conference Chair)
