\documentclass{article}

\usepackage{times}

%\usepackage[latin1]{inputenc}

%\usepackage{fullpage}

\addtolength{\textheight}{60mm}

\addtolength{\topmargin}{-30mm}

\addtolength{\textwidth}{70mm}

\addtolength{\oddsidemargin}{-35mm}

\pagestyle{empty}

\parindent0em

\begin{document}

\begin{center}

\textbf{CALL FOR PAPERS}\\[1.2ex]

{\normalsize 6th International Conference on }\\[0.8ex]

{\large\bfseries Interactive Theorem Proving (ITP 2015)}\\[0.8ex]

{\normalsize\itshape 24 -- 27 August 2015, Nanjing, China}\\[1.2ex]

\texttt{http://www.inf.kcl.ac.uk/staff/urbanc/itp-2015/}

\end{center}

\vspace{0mm}

\begin{minipage}[t]{6.9cm}% first column

\renewcommand{\baselinestretch}{0.99}\parskip 4pt\small

\textbf{Programme Committee:} \\

Andrea Asperti, \emph{University of Bologna}\\

Jesper Bengtson, \emph{IT University of Copenhagen}\\

Stefan Berghofer, \emph{Secunet Security Networks AG}\\

Yves Bertot, \emph{INRIA}\\

Lars Birkedal, \emph{Aarhus University}\\

Sandrine Blazy, \emph{IRISA}\\

Thierry Coquand, \emph{University of Gothenburg}\\

Xinyu Feng, \emph{Univ.~of Science and Technology of China}\\

Ruben Gamboa, \emph{University of Wyoming}\\

Herman Geuvers, \emph{Radboud University Nijmegen}\\

Mike Gordon, \emph{Cambridge University}\\

Elsa Gunter, \emph{University of Illinois, Urbana-Champaign}\\

John Harrison, \emph{Intel Corporation}\\

Hugo Herbelin, \emph{INRIA}\\

Matt Kaufmann, \emph{University of Texas at Austin}\\

Gerwin Klein, \emph{NICTA}\\

Cesar Munoz, \emph{NASA Langley Research Center}\\

Tobias Nipkow, \emph{TU M\"unchen}\\

Michael Norrish, \emph{NICTA}\\

Scott Owens, \emph{University of Kent}\\

Carsten Sch\"urmann, \emph{IT University of Copenhagen}\\

Konrad Slind, \emph{Rockwell Collins}\\

Alwen Tiu, \emph{Nanyang Technological University}\\

Christian Urban (co-chair), \emph{King's College London}\\

Dimitrios Vytiniotis, \emph{Microsoft Research Cambridge}\\

Xingyuan Zhang (co-chair), \emph{PLA University of Science and Technology}    

\\[1em]

%

\textbf{Important Dates:} \\

\begin{tabular}{@{}l@{~~}r@{}}

Title \& abstract submission:        & 9 March 2015\\

Full paper submission:        & 13 March 2015\\

Author notification:     & 15 May 2015\\

Camera-ready papers due: & 5 June 2015\\

Conference:              & 24 -- 27 August 2015\\

\end{tabular}

\\[1em]

\textbf{Organizers:} \\[1ex]

\begin{tabular}{@{}l@{}}

Xingyuan Zhang\\

Chunhan Wu\\

Christian Urban\\

\end{tabular}

\end{minipage}

\hspace{3mm}

\begin{minipage}[t]{11cm}% second column

\renewcommand{\baselinestretch}{0.95}

%\parskip0ex\parindent1.5em

\parskip1ex\parindent0em

%%%\small

ITP is the premier international conference for researchers

from all areas of interactive theorem proving and its

applications. The sixth conference will be held on 24 through

27 August 2015 in Nanjing.\medskip

{\bf Topics}\medskip

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:

\begin{itemize} 

\item Specification and verification of hardware:

      microprocessors, memory systems, pipelines, etc; formal

      semantics of hardware design languages; synthesis;

      formal design flows. 

\item Specification and verification of software: program

      verification, refinement, and synthesis for functional,

      declarative and imperative languages; formal semantics

      of programming languages; proof carrying code.

\item Industrial application of theorem provers. 

\item Formalization of mathematical theories. 

\item 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. 

\item Other topics, including formal verification of security

      policies and configurations (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. 

\item Proof Pearls: concise and elegant presentations of

      interesting examples. 

\end{itemize}

Submission is electronic. Papers should be no more than 16

pages in length and are to be submitted in PDF format. 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. 

In addition to regular papers, described above, there will be

a ``rough diamond'' section. Rough diamond submissions are

limited to 6 pages and may consist of an extended abstract.

They will be refereed: they will be expected to present

innovative and promising ideas, possibly in an early form and

without supporting evidence. Accepted diamonds will be

published in the main proceedings, and will be presented as

short talks. 

Authors of all accepted papers are expected to present their

paper at the conference.

\end{minipage}

\end{document}