[Hol-info] TPHOLs 2008 (LAST CALL FOR PAPERS)

[Otmane A. M. <ai...@en...>]

               Last Call for Papers
               --------------------

   21st International Conference on Theorem Proving in
               Higher Order Logics
                 (TPHOLs 2008)

       http://www.ece.concordia.ca/TPHOLs2008
            tph...@ec...

     August 18-21, 2008, Montreal, Quebec, Canada


The 2008 International Conference on Theorem Proving in Higher Order
Logics will be the 21st in a series that dates back to 1988. The
conference will be held in Montreal, Quebec, Canada, on 18-21 August 2008.

Topics
------

The program 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, modeling, 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, specification and
  requirement analysis of systems, user interfaces for theorem provers,
  development and extension of higher order logics, and application of
  theorem proving technology to new domains of science, e.g., biology.

Submissions
-----------

Submissions are invited in the following categories:

     * Category A: Full research paper
     * Category B: Emerging trends

Submissions under category A will be fully refereed. Accepted papers
will be published as a volume of Springer's Lecture Notes in Computer
Science series, which will be available at the conference.  Authors of
accepted Category A 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. Submissions accepted in this category will be published in a
technical report of Concordia University, which will be available at
the conference. Authors of accepted Category B 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.

Submissions must describe original unpublished work not submitted for
publication elsewhere. They may be no more than 16 pages in length,
including references, and must be prepared using the LNCS style.  The
PC chair should be informed of closely related work concurrently
submitted to a conference or journal. All contributions should be
submitted electronically through the conference submission web page.

Important dates
---------------
                                  Category A       Category B
    Abstract submission          15 Feb 2008           -
    Submission deadline          22 Feb 2008       2 May 2008
    Notification of acceptance   15 April 2008     25 Jun 2008
    Camera-ready copy due        15 May 2007       25 Jul 2008

Conference Chair
---------------

  Sofiene Tahar, Concordia University

Program Chairs
--------------

   Otmane Ait Mohamed, Concordia University
   Cesar Munoz, National Institute of Aerospace

Program Committee
-----------------

Mark Aagaard (University of Waterloo)
Otmane Ait Mohamed (Concordia University)
Hasan Amjad (Middlesex University)
Yves Bertot (INRIA)
Jens Brandt (University of Kaiserslautern)
Jean-Christophe Filliatre (CNRS)
Thierry Coquand (Göteborg University)
Ganesh Gopalakrishnan (University of Utah)
Mike Gordon (University of Cambridge)
Hanne Gottliebsen (Queen Mary, University of London)
Jim Grundy (Intel)
Elsa Gunter (University of Illinois at Urbana-Champaign)
John Harrison (Intel)
Jason Hickey (California Institute of Technology)
Peter Homeier (Department of Defense)
Joe Hurd (Galois)
Paul Jackson (University of Edinburgh)
Thomas Kropf (Bosch)
John Matthews (Galois)
Cesar Munoz (National Institute of Aerospace)
Tobias Nipkow (Technische Universität München)
Sam Owre (SRI International)
Christine Paulin-Mohring (Université Paris-Sud)
Lawrence Paulson (University of Cambridge)
Klaus Schneider (University of Kaiserslautern)
Konrad Slind (University of Utah)
Sofiene Tahar (Concordia University)
Matthew Wilding (Rockwell Collins)
Burkhart Wolff (ETH-Zurich)

Steering Committee
------------------

Mike Gordon (University of Cambridge)
John Harrison (Intel)
Matt Kaufmann (University of Texas, Austin)
John Matthews (Galois)
Tobias Nipkow (Technische Universität München)
Michael Norrish (National ICT Australia)
Lawrence Paulson (University of Cambridge)
Klaus Schneider(University of Kaiserslautern)
Sofiene Tahar (Concordia University)
Laurent Théry (INRIA Sophia Antipolis)