1 \documentclass{article}

     2 \usepackage{times}

     3 %\usepackage[latin1]{inputenc}

     4 %\usepackage{fullpage}

     5 

     6 \addtolength{\textheight}{60mm}

     7 \addtolength{\topmargin}{-30mm}

     8 \addtolength{\textwidth}{70mm}

     9 \addtolength{\oddsidemargin}{-35mm}

    10 

    11 \pagestyle{empty}

    12 \parindent0em

    13 

    14 \begin{document}

    15 

    16 \begin{center}

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

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

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

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

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

    22 \end{center}

    23 

    24 \vspace{0mm}

    25 

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

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

    28 

    29 \textbf{Programme Committee:} \\

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

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

    32 Steffen Berghofer, \emph{Secunet Security Networks AG}\\

    33 Yves Bertot, \emph{INRIA}\\

    34 Lars Birkedal, \emph{Aarhus University}\\

    35 Sandrine Blazy, \emph{IRISA}\\

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

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

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

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

    40 Mike Gordon, \emph{Cambridge University}\\

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

    42 John Harrison, \emph{Intel Corporation}\\

    43 Hugo Herbelin, \emph{INRIA}\\

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

    45 Gerwin Klein, \emph{NICTA}\\

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

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

    48 Michael Norrish, \emph{NICTA}\\

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

    50 Randy Pollack, \emph{Edinburgh University}\\

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

    52 Konrad Slind, \emph{Rockwell Collins}\\

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

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

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

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

    57 \\[1em]

    58 %

    59 \textbf{Important Dates:} \\

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

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

    62 Full paper submission:        & 13 March 2015\\

    63 Author notification:     & 15 May 2015\\

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

    65 Conference:              & 24 -- 27 August 2015\\

    66 \end{tabular}

    67 \\[1em]

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

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

    70 Xingyuan Zhang\\

    71 Chunhan Wu\\

    72 Christian Urban\\

    73 \end{tabular}

    74 

    75 \end{minipage}

    76 \hspace{3mm}

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

    78 \renewcommand{\baselinestretch}{0.95}

    79 %\parskip0ex\parindent1.5em

    80 \parskip1ex\parindent0em

    81 %%%\small

    82 

    83 ITP is the premier international conference for researchers

    84 from all areas of interactive theorem proving and its

    85 applications. The sixth conference will be held on 24 through

    86 27 August 2015 in Nanijing.

    87 

    88 {\bf Topics}\medskip

    89 

    90 The programme committee welcomes submissions on all aspects of

    91 interactive theorem proving and its applications. The topics

    92 include, but are not limited to, the following:

    93 

    94 

    95 \begin{itemize} 

    96 \item Specification and verification of hardware:

    97       microprocessors, memory systems, pipelines, etc; formal

    98       semantics of hardware design languages; synthesis;

    99       formal design flows. 

   100 \item Specification and verification of software: program

   101       verification, refinement, and synthesis for functional,

   102       declarative and imperative languages; formal semantics

   103       of programming languages; proof carrying code.

   104 \item Industrial application of theorem provers. 

   105 \item Formalization of mathematical theories. 

   106 \item Advances in theorem prover technology: proof automation

   107       and decision procedures, induction, combination of

   108       deductive and algorithmic approaches, incorporation of

   109       theorem provers into larger systems, combination of

   110       theorem provers with other provers and tools. 

   111 \item Other topics, including: security algorithms,

   112       properties, and policies; specification and requirements

   113       analysis of systems; user interfaces for theorem

   114       provers; development and extension of higher order

   115       logics. 

   116 \item Proof Pearls: concise and elegant presentations of

   117       interesting examples. 

   118 \end{itemize}

   119  

   120 Submission is electronic. Papers should be no more than 16

   121 pages in length and are to be submitted in PDF format. They

   122 must conform to the LNCS style preferably using LaTeX2e. The

   123 proceedings are to be published as a volume in the Lecture

   124 Notes in Computer Science series. 

   125  

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

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

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

   129 They will be refereed: they will be expected to present

   130 innovative and promising ideas, possibly in an early form and

   131 without supporting evidence. Accepted diamonds will be

   132 published in the main proceedings, and will be presented as

   133 short talks. 

   134 

   135 Authors of all accepted papers are expected to present their

   136 paper at the conference.

   137 

   138 

   139 \end{minipage}

   140 \end{document}