[TYPES/announce] TPHOLs'09 Last Call for Papers

[Stefan Berghofer]

   LAST CALL FOR PAPERS: TPHOLs 2009

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

17 - 20 August 2009 in Munich, Germany

 ******************************
 *  http://tphols.in.tum.de/  *
 ******************************

TPHOLs is a series of international conferences that started in 1988.
It brings together researchers working in all areas of interactive
theorem proving.  The conference will be held on 17 - 20 August
2009 in Munich. As in previous years, the formal proceedings of
TPHOLs will appear as a volume of LNCS.

Important Dates
---------------
Submission:              8 March 2009
Author notification:     4 May 2009
Camera-ready papers due: 5 June 2009

Website for submissions
http://www.easychair.org/conferences/?conf=tphols2009

Submission for the emerging
trends section:          11 May 2009

Conference:              17 - 20 August 2009


Topics
------

The program committee welcomes submissions on all aspects of theorem
proving in higher order logics, on related topics in theorem proving
and verification, and on relevant applications. The topics include, but
are not limited to, the following:

 Specification and verification of hardware: microprocessors, memory
 systems, buses, pipelines, etc; formal semantics of hardware design
 languages; synthesis; formal design flows.

 Specification and verification of software: program verification,
 refinement, and synthesis for functional, declarative and imperative
 languages; formal semantics of programming languages; compiler and
 operating system verification; proof carrying code.

 Industrial application of theorem provers.

 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.

 Other topics, including: user interfaces for theorem provers; development
 and extension of higher order logics.

 Proof Pearls: concise and elegant presentations of interesting examples.

Relevant research involving interactive first-order systems, such as ACL2
and Mizar, is also welcome. All authors are reminded that their work
should  be presented in a way that users of other systems can understand.

Papers should be no more than 16 pages in length and are to be submitted
in PDF format. Submissions must describe original unpublished work not
submitted for publication elsewhere. They must conform to the LNCS style
preferably using LaTeX2e. The proceedings are to be published as a volume
in the Lecture Notes in Computer Science series and will be available to
participants at the conference.

Authors of accepted papers are expected to present their paper at the
conference.

As has been custom in previous years there will be an emerging trends
section. Submissions under this section 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 TU München, which will also
be available at the conference. Authors of accepted papers in this section
are expected to present a brief outline of their work at the conference
and to prepare a poster for display at the conference venue.


Invited Speakers
----------------
David Basin      ETH Zurich
John Harrison    Intel
Wolfram Schulte  Microsoft Research

Programme Committee
-------------------
Thorsten Altenkirch        Nottingham University
David Aspinall             Edinburgh University
Jeremy Avigad              Carnegie Mellon University
Gilles Barthe              IMDEA
Christoph Benzmüller       Saarland University
Peter Dybjer               Chalmers University
Jean-Christophe Filliâtre  CNRS
Georges Gonthier           Microsoft Research
Mike Gordon                Cambridge University
Jim Grundy                 Intel
Reiner Hähnle              Chalmers University
Joe Hurd                   Galois
Gerwin Klein               NICTA
Xavier Leroy               INRIA
Pete Manolios              Northeastern University
César Muñoz                National Institute of Aerospace
Tobias Nipkow (co-chair)   TU München
Michael Norrish            NICTA
Sam Owre                   SRI International
Larry Paulson              Cambridge University
Frank Pfenning             Carnegie Mellon University
Randy Pollack              Edinburgh University
Sofiène Tahar              Concordia University
Laurent Théry              INRIA
Christian Urban (co-chair) TU München
Freek Wiedijk              Radboud University Nijmegen

Affiliated Events
-----------------

- Workshop on Programming Languages for Mechanized Mathematics
  Systems (PLMMS)

- Coq Users Meeting

- Isabelle Developers Workshop


Organizers
----------

Stefan Berghofer
Tobias Nipkow
Christian Urban
Makarius Wenzel