\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{University of Rennes}\\Bob Constable, \emph{Cornell University}\\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{Harvard 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\\Jinshang Wang\\Christian Urban\\\end{tabular}\end{minipage}\hspace{3mm}\begin{minipage}[t]{11cm}% second column\renewcommand{\baselinestretch}{0.95}%\parskip0ex\parindent1.5em\parskip1ex\parindent0em%%%\smallITP is the premier international conference for researchersfrom all areas of interactive theorem proving and itsapplications. The sixth conference will be held on 24 through27 August 2015 in Nanjing.\medskip{\bf Topics}\medskipThe programme committee welcomes submissions on all aspects ofinteractive theorem proving and its applications. The topicsinclude, 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 applications 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 16pages in length and are to be submitted in PDF format. Theymust conform to the LNCS style preferably using LaTeX2e. Theproceedings are to be published as a volume in the LectureNotes in Computer Science series. In addition to regular papers, described above, there will bea ``rough diamond'' section. Rough diamond submissions arelimited to 6 pages and may consist of an extended abstract.They will be refereed: they will be expected to presentinnovative and promising ideas, possibly in an early form andwithout supporting evidence. Accepted diamonds will bepublished in the main proceedings, and will be presented asshort talks. Authors of all accepted papers are expected to present theirpaper at the conference.\end{minipage}\end{document}