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


                     CALL FOR PAPERS: TPHOLs 2004

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

                           Park City, Utah

              Tuesday 14 September - Friday 17 September 2004

              ***********************************************
              *     http://www.cs.utah.edu/tphols2004/      *
              ***********************************************

TOPICS

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

  o  Specification and verification of:
     * Hardware: microprocessors, memory systems, buses, pipelines, etc;
                 formal semantics of hardware design languages; synthesis;
                 formal design flows
     * Software: program verification, refinement, and synthesis for
                 declarative and imperative languages; formal
                 semantics of programming languages; proof carrying code
  o  Industrial application of theorem provers
  o  Advances in theorem prover technology:
     * Proof automation and decision procedures
     * Induction
     * Combination of deductive and algorithmic approaches
     * Incorporation of theorem provers into larger systems
     * Combination of theorem provers with other provers and tools
  o  Security algorithms, properties, and policies
  o  Specification and requirements analysis of systems
  o  User interfaces for theorem provers
  o  Development and extension of higher order logics
  o  Formalization of mathematical theories
  o  Proof Pearls: concise and elegant presentations of interesting examples.

SUBMISSIONS

Submissions are invited in the following categories: "Mature Work" and
"Emerging Trends"  

                             Mature Work           Emerging Trends
  o Submission deadline:      20 Feb 2004           21 May 2004
  o Acceptance notification:   2 Apr 2004           18 June 2004
  o Camera-ready copy due:     7 May 2004           16 July 2004

Submissions under "Mature Work" will be fully refereed, and accepted
papers will be published in a volume of Springer's Lecture Notes in
Computer Science, which will be available at the conference.  Authors
of accepted papers are expected to present their work at the
conference.

Submissions under "Emerging Trends" will not be formally refereed, but
their content and relevance will be reviewed.  Accepted submissions
will be published in a University of Utah 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 "Mature Work" will
also be considered for inclusion under "Emerging Trends".

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
"tphols2004@cs.utah.edu".  This email address can also 
be used for any inquiries concerning the conference.

PROGRAM COMMITTEE

Mark Aagaard (Waterloo)                 Clark Barrett (NYU)
David Basin (Zurich)                    Yves Bertot (INRIA)
Ching-Tsun Chou (Intel)                 Thierry Coquand (Chalmers)
Peter Dybjer (Chalmers)                 Amy Felty (Ottawa)
Jean-Christophe Filliatre (Paris Sud)   Jacques Fleuriot (Edinburgh)
Mike Gordon (Cambridge)                 Jim Grundy (Intel)
Elsa Gunter (NJIT)                      John Harrison (Intel)
Jason Hickey (Caltech)                  Peter Homeier (DoD, USA)
Doug Howe (Carleton)                    Paul Jackson (Edinburgh)
Bart Jacobs (Nijmegen)                  Sara Kalvala (Warwick)
Matt Kaufmann (AMD)                     Thomas Kropf (Bosch)
Tom Melham (Oxford)                     Cesar Munoz (NASA)
Tobias Nipkow (Muenchen)                Sam Owre (SRI)
Christine Paulin-Mohring (Paris Sud)    Lawrence Paulson (Cambridge)
Frank Pfenning (CMU)                    Konrad Slind (Utah) (PC Chair)
Sofiene Tahar (Concordia)               Burkhardt Wolff (Freiburg)


CONFERENCE ORGANIZATION

The conference organizers are Konrad Slind and Ganesh Gopalakrishnan of 
the School of Computing at the University of Utah. Please use the
address tphols2004@cs.utah.edu to send email to the organizers.


RELATED EVENTS

There will be a gap of one day between the end of TPHOLs2004 and the
start of ICFP, the International Conference on Functional Programming.
ICFP will be held at Snowbird, Utah during Sept. 19-22. See 
http://www.cs.indiana.edu/icfp04/cfp/cfp.html for details.