Binary file cfp.pdf has changed

--- /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}

--- a/index.html	Sat Nov 15 08:44:19 2014 +0000
+++ b/index.html	Sat Nov 29 00:08:23 2014 +0000
@@ -107,18 +107,20 @@
 <TD BGCOLOR="#FFFFFF" WIDTH="75%" VALIGN="TOP">
 <TABLE>
 <TR>
-<TD><H1>ITP 2015 will be in Nanjing</H1></TD>
+<TD><H1>ITP 2015 will be in Nanjing, China</H1></TD>
 <TD align="right" valign="top"><img src="pics/nanjing-map.jpg" width="42%" height="40%" alt="TUM" align="top"></TD>
 </TR>
 </TABLE>
 <p>
-[CFP]
+<HR>
+[<a href="index.html#dates">Important Dates</a>]
+[<A HREF="cfp.pdf">CFP</A>]
 [<A HREF="history.html">Conference History</A>]
-</p>
+<HR></p>
 
 <p>
 The 6th conference on Interactive Theorem Proving will be held in
-Nanjing. The organising committee is chaired by Xingyuan Zhang and Christian Urban.
+Nanjing, China. The organising committee is chaired by Xingyuan Zhang and Christian Urban.
 <A HREF="http://en.wikipedia.org/wiki/Nanjing">Nanjing</A> is situated
 in the heart of China &#8212; close to Shanghai and roughly
 equidistant between Beijing and Hong Kong. It is a former capital
@@ -129,6 +131,13 @@
 Series.
 </p>
 
+<H3><A NAME="dates"></A>Important Dates</H3>
+Submission of title and abstract: 9 March 2015<BR>
+Submission of full paper: 13 March 2015<BR>
+Author notification: 15 May 2015<BR>
+Camera-ready papers: 5 June 2015<BR>
+Conference: 14-27 August 2015<BR>
+
 <H4>Timing and Tentative Programme</H4>
 
 The conference will be held in the last week of August (24th - 27th

--- a/pc	Sat Nov 15 08:44:19 2014 +0000
+++ b/pc	Sat Nov 29 00:08:23 2014 +0000
@@ -1,28 +1,54 @@
-Gerwin Klein      (NICTA)
-Ruben Gamboa      (University of Wyoming)
-Tobias Nipkow     (TU Munich)
-Michael Norrish   (NICTA)
-John Harrison     (INTEL)
-Thierry Coquand   (University of Gothenburg)
+Andrea Asperti    (Uni Bologna)
+   http://www.cs.unibo.it/~asperti/
+Jesper Bengtson   (IT University of Copenhagen)
+   http://www.itu.dk/people/jebe/
 Steffen Berghofer (Secunet Security Networks AG)
-Randy Pollack     (Harvard University)
-Mike Gordon       (Cambridge University)
-Sandrine Blazy    (INRIA)      
-Herman Geuvers    (Nijmegen)
-Xinyu Feng        (Suzhou Institute for Advanced Study)
+   http://wwwbroy.in.tum.de/~berghofe/
 Yves Bertot       (INRIA)
-Konrad Slind      (Rockwell Collins)
+   http://www-sop.inria.fr/members/Yves.Bertot/
+Lars Birkedal     (Aarhus University)
+   http://cs.au.dk/~birke/
+Sandrine Blazy    (IRISA)
+   https://www.irisa.fr/celtique/blazy/index.html#contact
+Thierry Coquand   (University of Gothenburg)
+   http://www.cse.chalmers.se/~coquand/
+Xinyu Feng        (University of Science and Technology of China)
+   http://staff.ustc.edu.cn/~xyfeng/
+Ruben Gamboa      (University of Wyoming)
+   http://www.cs.uwyo.edu/~ruben/
+Herman Geuvers    (Nijmegen)
+   http://www.cs.ru.nl/~herman/
+Mike Gordon       (Cambridge University)
+   https://www.cl.cam.ac.uk/~mjcg/
+Elsa Gunter       (University of Illinois, Urbana - Champaign)
+   http://web.engr.illinois.edu/~egunter/
+John Harrison     (Intel Corporation)
+   http://www.cl.cam.ac.uk/~jrh13/
 Hugo Herbelin     (INRIA)
-Lars Birkedal     (Aarhus)
-Jesper Bengtson   (ITU)
-Carsten Schuermann (ITU)
-Dimitrios Vytiniotis (Microsoft)
-Elsa Gunter       (Urbana Champain)
-Cesar Munos       (nasa)
-Andrea Asperti     (Uni Bologna)
-Scott Owens       (Kent)
-Matt Kaufman      (texas)
-Alwen Tiu          (Nanyang)
+   http://pauillac.inria.fr/~herbelin/index-eng.html
+Matt Kaufman      (University of Texas at Austin)
+   http://www.cs.utexas.edu/~kaufmann/
+Gerwin Klein      (NICTA)
+   http://www.cse.unsw.edu.au/~kleing/
+Cesar Munoz       (NASA Langley Research Center)
+   http://shemesh.larc.nasa.gov/people/cam/
+Tobias Nipkow     (TU Munich)
+   http://www21.in.tum.de/~nipkow/
+Michael Norrish   (NICTA)
+   http://nicta.com.au/people/norrishm
+Scott Owens       (University of Kent)
+   http://www.cs.kent.ac.uk/people/staff/sao/
+Randy Pollack     (Harvard University)
+   http://homepages.inf.ed.ac.uk/rpollack/
+Carsten Schümann (IT University of Copenhagen)
+   http://www.itu.dk/people/carsten/ 
+Konrad Slind      (Rockwell Collins)
+Alwen Tiu         (Nanyang Technological University)
+   http://www.ntu.edu.sg/home/atiu/
+Christian Urban   (King's College London)
+Dimitrios Vytiniotis (Microsoft Research Cambridge)
+   http://research.microsoft.com/en-us/people/dimitris/
+Xingyuan Zhang    (PLA University of Science and Technology Nanjing)
 (25)