The programme committee welcomes submissions on all aspects of interactive theorem proving and its applications. The topics include, but are not limited to, the following: · Specification and verification of hardware: microprocessors, memory systems, pipelines, etc; formal semantics of hardware design languages; synthesis; formal design flows. · Specification and verification of software: program verification, refine- ment, and synthesis for functional, declarative and imperative languages; formal semantics of programming languages; proof carrying code. · Industrial application of theorem provers. · Formalization of mathematical theories. · Advances in theorem prover technology: proof automation and deci- sion procedures, induction, combination of deductive and algorithmic approaches, incorporation of theorem provers into larger systems, com- bination of theorem provers with other provers and tools. · Other topics, including formal verification of security policies and con- figurations (formal analysis, verification of security algorithms, etc); specification and requirements analysis of systems; user interfaces for theorem provers; development and extension of higher order logics. · Proof Pearls: concise and elegant presentations of interesting examples.