[isabelle] TPHOLs 2007 (2nd Call for Papers)
20th International Conference on Theorem Proving in Higher Order Logics
Kaiserslautern, Germany, 11-13 September 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
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
* 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.
* 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
* Other topics, including: security algorithms, properties, and
policies; specification and requirements analysis of systems; user
interfaces for theorem provers; development and extension of higher
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.
Please note that the following deadlines are strict. Due to a tight
schedule, no further extension can be given.
* Submission deadline: 23 Mar 2007
* Notification of acceptance: 25 May 2007
* Camera-ready copy due: 08 Jun 2007
* Submission deadline: 18 May 2007
* Notification of acceptance: 25 Jun 2007
* Camera-ready copy due: 27 Jul 2007
This archive was generated by a fusion of
Pipermail (Mailman edition) and