6th International Conference on Interactive Theorem Proving (ITP 2015)

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.