The Coq mailing list

[Klaus Schneider <Klaus.Schneider AT informatik.uni-kl.de>]

20th International Conference on Theorem Proving in Higher Order Logics
Kaiserslautern, Germany, 11-13 September 2007
http://rsg.informatik.uni-kl.de/TPHOLs-2007

Call for Papers

The 2007 International Conference on Theorem Proving in Higher Order
Logics will be the twentieth in a series that dates back to 1988. The
conference will be held in Kaiserslautern, Germany, on 11-13 September
2007.

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:

  * Formal semantics of specification, modelling, and programming
    languages: formal synthesis, validated compilation, formal design
    flows.
  * Specification and verification of hardware: microprocessors, memory
    systems, buses, pipelines etc.
  * Specification and verification of software: program verification,
    refinement, and synthesis for functional, declarative and imperative
    languages; proof carrying code.
  * Formalisation of mathematical theories.
  * 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.
  * Industrial application of theorem provers.
  * Proof Pearls: concise and elegant presentations of interesting
    examples.
  * Other topics, including: security algorithms, properties, and
    policies; specification and requirements analysis of systems; user
    interfaces for theorem provers; development and extension of higher
    order logics.

Submission

Submissions are invited in the following categories:

  * Category A: Full research paper
  * Category B: Emerging trends

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, which will be available at the conference.
Authors of accepted papers are expected to present their work at the
conference. Submissions should be no more than 16 pages in length and
should be written using LaTeX2e and the LNCS style file.

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 of the University of Kaiserslautern, 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. Papers should be no
more than 16 pages in length and should be written using LaTeX2e and the
LNCS style file. Unless otherwise requested, submissions rejected under
category A will also be considered for inclusion under category B.

Important Dates

Please note that the following deadlines are strict. Due to a tight
schedule, no further extension can be given.

Category A
  * Submission deadline: 23 Mar 2007
  * Notification of acceptance: 25 May 2007
  * Camera-ready copy due: 08 Jun 2007

Category B
  * Submission deadline: 18 May 2007
  * Notification of acceptance: 25 Jun 2007
  * Camera-ready copy due: 27 Jul 2007