Call for Papers
The 2008 International Conference on Theorem Proving in Higher Order
Logics will be the twenty first in a series that dates back to 1988.
The conference will be held in Montéal, Québec, Canada, on 18th to 21st August, 2008.
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.
- 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
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/Mature research work
- Category B: Emerging trends
Submissions under category A will be fully refereed, and 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.
Submissions should 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.
|
|
Category A
|
Category B
|
| Abstract submission |
15 Feb 2008 |
|
| Submission deadline |
22 Feb 2008 |
2 May 2008 |
| Notification of acceptance |
15 Apr 2008 |
2 Jun 2008 |
| Camera-ready copy due |
15 May 2008 |
4 Jul 2008 |
Conference Chair
- Sofiene Tahar, Concordia University
Program Chairs
- Otmane Ait Mohamed, Concordia university
- César Muñoz, 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 (Goteborg 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)
- César Muñoz (National Institute of Aerospace)
- Tobias Nipkow (Technische Universitat Munchen)
- Sam Owre (SRI International)
- Christine Paulin-Mohring (University 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 Universitat Munchen)
- Michael Norrish (National ICT Australia)
- Lawrence Paulson (University of Cambridge)
- Klaus Schneider(University of Kaiserslautern)
- Sofiene Tahar (Concordia University)
- Laurent Thery (INRIA Sophia Antipolis)
