\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}\\
Randy Pollack, \emph{Edinburgh University}\\
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}