CALL FOR PAPERS: TPHOLs 2001

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

                          Edinburgh, Scotland
              Monday 3rd  - Thursday 6th September 2001

              *****************************************
              *  http://www.dcs.gla.ac.uk/TPHOLs2001  *
              *****************************************

The 2001 International Conference on Theorem Proving in Higher Order
Logics will be the fourteenth in a series that dates back to 1988.
The conference will be held Monday 3rd September through Thursday 
6th September in central Edinburgh, Scotland. 

TOPICS

The programme 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

Online paper submission is now open: www.dcs.gla.ac.uk/TPHOLs2001

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.

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. The TPHOLs web page
should be consulted for further details on preparation and electronic
submission.  

Important dates are:
                              Category A    Category B 

Submission deadline:          23 Feb 2001   18 May 2001 
Notification of acceptance:   30 Apr 2001   25 Jun 2001
Camera-ready copy due:         1 Jun 2001   27 Jul 2001 

ACCOMMODATION

Information on accommodation is now available on the TPHOLs2001 web
site: www.dcs.gla.ac.uk/TPHOLs2001

RELATED EVENTS

TPHOLs 2001 will be co-located with the 11th Advanced Research Working
Conference on Correct Hardware Design and Verification Methods (CHARME
2001), which will run from Tuesday 4th to Friday 7th September 2001 and
will be located at the Institute for System Level Integration in the
nearby town of Livingston.  A joint half-day session is planned for
Wednesday 5th September.  Further information on CHARME 2001 is
available at http://www.dcs.gla.ac.uk/CHARME2001.

PROGRAMME COMMITTEE

Mark Aagaard (U. Waterloo)          Paul Jackson (U. Edinburgh)
David Basin (U. Freiburg)           Sara Kalvala (U. Warwick)
Richard Boulton (U. Glasgow)        Michael Kohlhase (CMU & Saarland U.)
Albert Camilleri (HP)               J Moore (U. Texas, Austin)
Victor Carreno (NASA Langley)       Sam Owre (SRI)
Gilles Dowek (INRIA Roquencourt)    Christine Paulin (INRIA Roquencourt)
Harald Ganzinger (MPI Saarbruecken) Lawrence Paulson (U. Cambridge)
Ganesh Gopalakrishnan (U. Utah)     Frank Pfenning (CMU)
Jim Grundy (Intel)                  Klaus Schneider (U. Karlsruhe)
Elsa Gunter (NJIT)                  Henny Sipma (Stanford U.)
John Harrison (Intel)               Konrad Slind (U. Cambridge)
Doug Howe (Carleton U.)             Don Syme (Microsoft)
Bart Jacobs (U. Nijmegen)           Sofiene Tahar (Concordia U.)

CONFERENCE ORGANIZATION

The conference is being organized jointly by the University of
Edinburgh Division of Informatics and the University of Glasgow
Department of Computing Science.

The organizing committee is as follows:

  Conference Chair:         Richard Boulton  (U. Glasgow)
  Programme Chair:          Paul Jackson     (U. Edinburgh)
  Local Arrangements Chair: Louise Dennis    (U. Edinburgh) 
  Local Arrangements:       Jacques Fleuriot (U. Edinburgh)
  Publicity Chair:          Simon Gay        (U. Glasgow)
  TPHOLs/CHARME Coordinating General Chair: 
                            Tom Melham       (U. Glasgow)

SPONSORS

TPHOLs 2001 is sponsored by the following organizations:

 o Intel
 o Microsoft Research

CONTACT

Enquiries concerning the conference should be emailed to
tphols2001@inf.ed.ac.uk.