# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1407683206 -3600
# Node ID 5868d8f8649f18e483f4a1930582c5f093f03760
# Parent  a4b7afa82af676656fbf18006b7f53fa6370f8a1
added

diff -r a4b7afa82af6 -r 5868d8f8649f index.html
--- a/index.html	Fri Jul 25 14:38:12 2014 +0100
+++ b/index.html	Sun Aug 10 16:06:46 2014 +0100
@@ -111,7 +111,10 @@
 <TD align="right" valign="top"><img src="pics/nanjing-map.jpg" width="42%" height="40%" alt="TUM" align="top"></TD>
 </TR>
 </TABLE>
-<BR>
+<p>
+
+</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.
 <A HREF="http://en.wikipedia.org/wiki/Nanjing">Nanjing</A> is situated
@@ -121,20 +124,23 @@
 HREF="http://www.cityofnanjing.com">cultural heritage</A>.  
 We expect to have more information about travelling and a detailed programme
 nearer the time.
+</p>
 
 <H4>Timing and Tentative Programme</H4>
 
 The conference will be held in the last week of August (24th - 27th
-August 2015). We intend to organise an Isabelle tutorial before the
-conference and host any workshops on the 28th August, provided
-there is interest.
-<p>
+August 2015).  As is the tradition, the conference consists of 4 days
+of research presentations and invited talks. Like in previous
+conferences, we would allow ample time between the formal sessions for
+attendees to mingle and converse. Half a day will be dedicated to an
+excursion.
 
-As is the tradition, the conference consists of 4 days of research presentations
-and invited talks. Like in previous conferences, we would allow ample time
-between the formal sessions for attendees to mingle and converse. Half a day
-will be dedicated to an excursion.
-
+<p>
+<IMG SRC="pics/new.gif" ALT="" style="" align="left">There will be an Isabelle tutorial before the
+conference (21 - 23 August), and<BR><BR>
+<IMG SRC="pics/new.gif" ALT="" style="" align="left">there will be a Coq tutorial after the conference
+(27 - 29 August).<BR><BR>
+</p>
 
 <H4>Travel to Nanjing</H4>
 
diff -r a4b7afa82af6 -r 5868d8f8649f pc
--- a/pc	Fri Jul 25 14:38:12 2014 +0100
+++ b/pc	Sun Aug 10 16:06:46 2014 +0100
@@ -2,7 +2,7 @@
 Ruben Gamboa      (University of Wyoming)
 Tobias Nipkow     (TU Munich)
 Michael Norrish   (NICTA)
-John Harrison     (asked)
+John Harrison     (INTEL)
 Matt Kaufman
 Thierry Coquand   (University of Gothenburg)
 Steffen Berghofer (Secunet Security Networks AG)
@@ -17,13 +17,14 @@
 Xinyu Feng        (Suzhou Institute for Advanced Study)
 Alwen Tui
 Humin Lin         (asked)
-Nick Benton       (asked)
 Yves Bertot       (INRIA)
 John Matthews (no asked yet Galois)
 Konrad Slind      (Rockwell Collins)
 Hugo Herbelin     (INRIA)
 Bob Constable
-(27)
+Jesper Bengtson   (ITU)
+Lars Birkedal     (asked)
+(14)
 
 Previous ITP was 33
 
@@ -43,6 +44,7 @@
 
 =======================
 Gilles Barthe     (out)
+Nick Benton       (out)
 
 =========
 Potential Invited speakers:
diff -r a4b7afa82af6 -r 5868d8f8649f pics/new.gif
Binary file pics/new.gif has changed