Received: from antares.mcs.anl.gov (mcs.anl.gov [140.221.9.6]) by ra.abo.fi (8.6.10/8.6.10) with ESMTP id TAA23077; Tue, 30 Jan 1996 19:19:56 +0200
Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
	id JAA27427 for qed-out; Tue, 30 Jan 1996 09:21:40 -0600
Received: from ra.abo.fi (ra.abo.fi [130.232.18.2]) by antares.mcs.anl.gov (8.6.10/8.6.10)  with ESMTP
	id JAA27214 for <qed@mcs.anl.gov>; Tue, 30 Jan 1996 09:13:00 -0600
Received: from bruce.abo.fi (root@bruce.abo.fi [130.232.209.103]) by ra.abo.fi (8.6.10/8.6.10) with ESMTP id RAA17666; Tue, 30 Jan 1996 17:10:59 +0200
Received: from bruce.abo.fi (jgrundy@localhost [127.0.0.1]) by bruce.abo.fi (8.6.10/8.6.10) with ESMTP id RAA19214; Tue, 30 Jan 1996 17:12:01 +0200
Message-Id: <199601301512.RAA19214@bruce.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@cs.uq.oz.au, qed@mcs.anl.gov,
        pvs@csl.sri.com, ifip-10.5@ics.uci.edu
Subject: 2nd CFP: TPHOLs96 - Theorem Proving in Higher Order Logics (ASCII)
From: Jim Grundy <jim.grundy@abo.fi>
Date: Tue, 30 Jan 1996 17:11:55 +0200
Sender: owner-qed@mcs.anl.gov
Precedence: bulk


			  CALL FOR PAPERS: TPHOLs'96

                    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.  Further information about the
 conference can be found at the conference web site:
			http://~jharriso/TPHOLs96.html.
 
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 Springer-Verlag LNCS series.  Submissions accepted under
 category B will be published as a technical report and destributed 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
                     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 is as follows:

  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)

