TPHOLs 2000 --- call for papers

10 Dec 1999

      [We apologize if you receive multiple copies of this message]

                     CALL FOR PAPERS: TPHOLs 2000

                 The 13th International Conference on
                Theorem Proving in Higher Order Logics

                        Portland, Oregon, USA
               Monday 14 August - Friday 18 August 2000

               ***************************************
               *  http://www.cse.ogi.edu/tphols2000  *
               ***************************************

The 2000 International Conference on Theorem Proving in Higher Order
Logics will be the thirteenth in a series that dates back to 1988.
The conference will be held Monday 14 August through Friday 18 August,
2000, at the DoubleTree Hotel, Portland, Oregon, USA.  The first day
of the conference will be devoted to tutorials, with the remaining 4
days covering the main conference program.

TOPICS

The program committee welcomes submissions on all aspects of theorem
proving in higher order logics, and on related topics in theorem
proving and verification.  This includes, but is not limited to, the
following topics:

  o  Hardware and software verification, refinement and synthesis
  o  Verification of security and communications protocols
  o  Formal specification and requirements analysis of systems
  o  Industrial applications of theorem provers
  o  Advances in theorem prover technology
  o  Comparisons of various approaches to theorem proving
  o  Proof automation and decision procedures
  o  Incorporation of theorem provers into larger systems
  o  Combination of theorem provers with other provers and tools
  o  User interfaces for theorem provers
  o  Development and extension of higher order logics

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
will be published as a volume of Springer-Verlag's Lecture Notes in
Computer Science series ("http://www.springer.de/comp/lncs/index.html"),
which will be available at the conference.  Authors of accepted papers
are expected to present their work at the conference.

Submissions under category B will not be formally refereed, but their
content and relevance will be reviewed.  Those submissions accepted
will be published in a technical report, which will be available at the
conference.  Authors of accepted papers are expected to present a
brief outline of their work at the conference and to prepare a poster
for display at the conference venue.  Unless otherwise requested,
submissions rejected under category A will also be considered for
inclusion under category B.

DEADLINES AND SUBMISSION PROCEDURE

  o Deadline for category A submissions:                   25 Feb 2000
  o Deadline for category B submissions:                   17 Mar 2000
  o Notification of acceptance:                             3 Apr 2000
  o Camera-ready copy for category A due (provisional):     5 May 2000
  o Conference:                                         14-18 Aug 2000

Papers should be no more than 16 pages in length and should be written
using LaTeX2e and the LNCS style file, which is available from
"http://www.springer.de/comp/lncs/authors.html".  Submissions should
be sent electronically following the instructions on the TPHOLs web
page, or emailed directly to the organizers using the email address
"tphols2000@cse.ogi.edu".  This email address can also be used for any
inquiries concerning the conference.

PROGRAM COMMITTEE

 Mark Aagaard (Intel)               Bart Jacobs (Nijmegen)
 Flemming Andersen (IBM)            Paul Jackson (Edinburgh)
 David Basin (Freiburg)             Steve Johnson (Indiana)
 Richard Boulton (Edinburgh)        Sara Kalvala (Warwick)
 Albert Camilleri (HP)              Tom Melham (Glasgow)
 Gilles Dowek (INRIA)               Paul Miner (NASA)
 Harald Ganzinger (Saarbrucken)     Tobias Nipkow (Muenchen)
 Ganesh Gopalakrishnan (Utah)       Sam Owre (SRI)
 Mike Gordon (Cambridge)            Christine Paulin-Mohring (INRIA)
 Jim Grundy (ANU)                   Lawrence Paulson (Cambridge)
 Elsa Gunter (Bell Labs)            Klaus Schneider (Karlsruhe)
 John Harrison (Intel)              Sofiene Tahar (Concordia)
 Doug Howe (Bell Labs)              Ranga Vemuri (Cincinnati)
 Warren Hunt (IBM)

CONFERENCE ORGANIZATION

The conference is being organized by Intel Corp. and the Oregon
Graduate Institute (OGI).  The organizing committee is as follows:

    Mark Aagaard (General Chair)  John Harrison (Program Chair)
    Kelly Atkinson                Naren Narasimhan
    Robert Beers                  Tom Schubert
    Nancy Day