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 10-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.

	Category A	Category B
Submission deadline	23 Mar 2007	18 May 2007
Notification of acceptance	25 May 2007	25 Jun 2007
Camera-ready copy due	08 Jun 2007	27 Jul 2007

Programme Committee

• Mark Aagaard, Waterloo
• Yves Bertot, INRIA
• Ching Tsun Chou, Intel
• Thierry Coquand, Chalmers
• Amy Felty, Ottawa
• Jean-Christophe Filliatre, Paris Sud
• Jacques Fleuriot, Edinburgh
• Ganesh Gopalakrishnan, Utah
• Mike Gordon, Cambridge
• Jim Grundy, Intel
• Elsa Gunter, UIUC
• John Harrison, Intel
• Jason Hickey, Caltech
• Peter Homeier, US DoD
• Joe Hurd, Oxford
• Paul Jackson, Edinburgh
• Thomas Kropf, Bosch
• John Matthews, Galois
• Tom Melham, Oxford
• Cesar Munoz, Aerospace
• Tobias Nipkow, Munich
• Sam Owre, SRI
• Christine Paulin-Mohring, Paris Sud
• Lawrence Paulson, Cambridge
• Klaus Schneider, Kaiserslautern
• Konrad Slind, Utah
• Sofiene Tahar, Concordia
• Burkhart Wolff, Zurich