[DL] TPHOLs2007 Call for Papers

Klaus Schneider Klaus.Schneider at informatik.uni-kl.de
Thu Nov 2 14:38:10 CET 2006


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

Kaiserslautern, Germany
Tuesday 11th - Thursday 13th September 2007


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, during
September 11-13, 2007.


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


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 (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 of the University of Kaiserslautern,
which will also 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


    Category A

        Submission deadline:          23 Feb 2007
        Notification of acceptance:   30 Apr 2007
        Camera-ready copy due:        01 Jun 2007

    Category B

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


Enquiries concerning the conference should be emailed to
tphols2007 at informatik.uni-kl.de

More information about the dl mailing list