CALL FOR PAPERS
The 20th International Conference
on Theorem Proving in Higher Order Logics
Kaiserslautern, Germany
Tuesday 11th - Thursday 13th September 2007
http://rsg.informatik.uni-kl.de/TPHOLs-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.
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.
- 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
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 (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
submission.
IMPORTANT DATES
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
CONTACT
Enquiries concerning the conference should be emailed to
tphols2007 at informatik.uni-kl.de