--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/cfp.tex	Sat Nov 29 00:08:23 2014 +0000
@@ -0,0 +1,140 @@
+\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}\\
+Steffen 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 Nanjing}    
+\\[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 Nanijing.
+
+{\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: security algorithms,
+      properties, and policies; 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}