itp-2015: index.html@56c28e4152f0 (annotated)

0 98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1	<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	2	<html>
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	3	<head>
64 d4ec47be8f14 bid accepted Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 63 diff changeset	4	<title>ITP 2015 in Nanjing</title>
31 18e8ae741f43 fixed errors Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 30 diff changeset	5	<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
34 77b0440b8694 fixed errors Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 33 diff changeset	6	<style type="text/css">
17 a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	7	#map_canvas {
a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	8	width: 500px;
a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	9	height: 400px;
a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	10	}
a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	11	</style>
29 9ce32a79d415 fixed errors Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 27 diff changeset	12	<script type="text/javascript" src="https://maps.googleapis.com/maps/api/js?sensor=false"></script>
32 5e946f890cfe fixed errors Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 31 diff changeset	13	<script type="text/javascript">
17 a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	14	function initialize() {
a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	15	var Latlng = new google.maps.LatLng(32.060255, 118.796877);
a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	16	var map_canvas = document.getElementById('map_canvas');
a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	17	var map_options = {
a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	18	center: Latlng,
a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	19	zoom: 0,
a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	20	mapTypeId: google.maps.MapTypeId.HYBRID
a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	21	}
a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	22	var map = new google.maps.Map(map_canvas, map_options)
0 98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	23
17 a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	24	var marker = new google.maps.Marker({
a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	25	position: Latlng,
a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	26	map: map,
a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	27	title: 'Nanjing'
a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	28	});
0 98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	29	}
17 a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	30	google.maps.event.addDomListener(window, 'load', initialize);
0 98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	31	</script>
34 77b0440b8694 fixed errors Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 33 diff changeset	32	<style type="text/css">
15 9052a9b07b59 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 14 diff changeset	33	body { font-size: 14px;
9052a9b07b59 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 14 diff changeset	34	font-family: "trebuchet ms", helvetica, sans-serif; }
9052a9b07b59 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 14 diff changeset	35	</style>
0 98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	36	</head>
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	37
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	38	<BODY TEXT="#000000"
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	39	BGCOLOR="#4169E1"
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	40	LINK="#0000EF"
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	41	VLINK="#51188E"
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	42	ALINK="#FF0000"
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	43	onload="initialize()" onunload="GUnload()">
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	44
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	45	<TABLE WIDTH="100%"
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	46	BGCOLOR="#4169E1"
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	47	BORDER="0"
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	48	FRAME="border"
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	49	CELLPADDING="10"
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	50	CELLSPACING="2"
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	51	RULES="all">
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	52
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	53	<!-- left column -->
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	54	<TR>
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	55	<TD BGCOLOR="#FFFFFF"
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	56	WIDTH="20%"
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	57	VALIGN="TOP"
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	58	ROWSPAN="2">
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	59
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	60
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	61	<p align=center>
18 c4dc7907c66b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 17 diff changeset	62	<a href="pics/ITP-Linggusu.jpg">
26 abaa87d69a1d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 25 diff changeset	63	<img src="pics/ITP-Linggusu.jpg" width="50%" height="12%" alt="Linggusi" border=0></a>
0 98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	64	<br>
26 abaa87d69a1d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 25 diff changeset	65	Linggusi pagoda<br>
0 98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	66	</p>
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	67
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	68	<p align=center>
18 c4dc7907c66b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 17 diff changeset	69	<a href="pics/ITP-Mochou.jpg">
22 889666f40918 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 21 diff changeset	70	<img src="pics/ITP-Mochou.jpg" alt="Mochou" width="88%" height="18%" border=0></a>
0 98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	71	<br>
26 abaa87d69a1d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 25 diff changeset	72	Mochou Lake Park<br>
0 98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	73	</p>
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	74
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	75	<p align=center>
18 c4dc7907c66b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 17 diff changeset	76	<a href="pics/ITP-najing-cit-walk.jpg">
20 a78382005a14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 19 diff changeset	77	<img src="pics/ITP-najing-cit-walk.jpg" alt="City Wall" width="50%" height="18%" border=0></a>
0 98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	78	<br>
26 abaa87d69a1d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 25 diff changeset	79	Nanjing city wall<br>
20 a78382005a14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 19 diff changeset	80	</p>
a78382005a14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 19 diff changeset	81
a78382005a14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 19 diff changeset	82	<p align=center>
a78382005a14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 19 diff changeset	83	<a href="pics/Nanjing2.jpg">
a78382005a14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 19 diff changeset	84	<img src="pics/Nanjing2.jpg" alt="City Wall" width="80%" height="13%" border=0></a>
a78382005a14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 19 diff changeset	85	<br>
26 abaa87d69a1d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 25 diff changeset	86	"Elephant Road" of the<br> Ming tomb<br>
24 4dab946931d8 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 23 diff changeset	87	</p>
4dab946931d8 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 23 diff changeset	88
4dab946931d8 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 23 diff changeset	89	<p align=center>
4dab946931d8 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 23 diff changeset	90	<a href="pics/Nanjing3.jpg">
4dab946931d8 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 23 diff changeset	91	<img src="pics/Nanjing3.jpg" alt="Nanjing's skyline" width="80%" height="13%" border=0></a>
4dab946931d8 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 23 diff changeset	92	<br>
26 abaa87d69a1d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 25 diff changeset	93	Nanjing's skyline<br>
25 af623d2a1b3e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 24 diff changeset	94	</p>
af623d2a1b3e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 24 diff changeset	95
af623d2a1b3e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 24 diff changeset	96	<p align=center>
af623d2a1b3e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 24 diff changeset	97	<a href="pics/Nanjing4.jpg">
af623d2a1b3e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 24 diff changeset	98	<img src="pics/Nanjing4.jpg" alt="Science and Technology Museum" width="80%" height="18%" border=0></a>
af623d2a1b3e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 24 diff changeset	99	<br>
26 abaa87d69a1d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 25 diff changeset	100	Science and Technology<br> Museum<br>
25 af623d2a1b3e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 24 diff changeset	101	</p>
0 98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	102
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	103	</TD>
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	104
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	105
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	106	<!-- right column -->
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	107	<TD BGCOLOR="#FFFFFF" WIDTH="75%" VALIGN="TOP">
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	108	<TABLE>
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	109	<TR>
69 43da71639190 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 65 diff changeset	110	<TD><H1>ITP 2015 will be in Nanjing</H1></TD>
16 8a34dbbd8788 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 15 diff changeset	111	<TD align="right" valign="top"><img src="pics/nanjing-map.jpg" width="42%" height="40%" alt="TUM" align="top"></TD>
0 98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	112	</TR>
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	113	</TABLE>
75 5868d8f8649f added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 70 diff changeset	114	<p>
5868d8f8649f added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 70 diff changeset	115
5868d8f8649f added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 70 diff changeset	116	</p>
5868d8f8649f added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 70 diff changeset	117	<p>
65 aba8911d873e some small changes after the bid Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 64 diff changeset	118	The 6th conference on Interactive Theorem Proving will be held in
aba8911d873e some small changes after the bid Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 64 diff changeset	119	Nanjing. The organising committee is chaired by Xingyuan Zhang and Christian Urban.
59 bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	120	<A HREF="http://en.wikipedia.org/wiki/Nanjing">Nanjing</A> is situated
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	121	in the heart of China — close to Shanghai and roughly
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	122	equidistant between Beijing and Hong Kong. It is a former capital
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	123	during the Ming Dynasty with a rich <A
65 aba8911d873e some small changes after the bid Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 64 diff changeset	124	HREF="http://www.cityofnanjing.com">cultural heritage</A>.
69 43da71639190 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 65 diff changeset	125	We expect to have more information about travelling and a detailed programme
76 56c28e4152f0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 75 diff changeset	126	nearer the time. The proceedings will be published as usual in the LNCS
56c28e4152f0 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 75 diff changeset	127	Series.
75 5868d8f8649f added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 70 diff changeset	128	</p>
69 43da71639190 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 65 diff changeset	129
43da71639190 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 65 diff changeset	130	<H4>Timing and Tentative Programme</H4>
43da71639190 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 65 diff changeset	131
43da71639190 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 65 diff changeset	132	The conference will be held in the last week of August (24th - 27th
75 5868d8f8649f added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 70 diff changeset	133	August 2015). As is the tradition, the conference consists of 4 days
5868d8f8649f added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 70 diff changeset	134	of research presentations and invited talks. Like in previous
5868d8f8649f added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 70 diff changeset	135	conferences, we would allow ample time between the formal sessions for
5868d8f8649f added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 70 diff changeset	136	attendees to mingle and converse. Half a day will be dedicated to an
5868d8f8649f added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 70 diff changeset	137	excursion.
69 43da71639190 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 65 diff changeset	138
75 5868d8f8649f added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 70 diff changeset	139	<p>
5868d8f8649f added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 70 diff changeset	140	<IMG SRC="pics/new.gif" ALT="" style="" align="left">There will be an Isabelle tutorial before the
5868d8f8649f added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 70 diff changeset	141	conference (21 - 23 August), and<BR><BR>
5868d8f8649f added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 70 diff changeset	142	<IMG SRC="pics/new.gif" ALT="" style="" align="left">there will be a Coq tutorial after the conference
5868d8f8649f added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 70 diff changeset	143	(27 - 29 August).<BR><BR>
5868d8f8649f added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 70 diff changeset	144	</p>
0 98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	145
3 13f56651ef26 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 2 diff changeset	146	<H4>Travel to Nanjing</H4>
0 98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	147
59 bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	148	Nanjing is a major city in China. There are international airline
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	149	connections directly to <A
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	150	HREF="http://en.wikipedia.org/wiki/Nanjing_Lukou_International_Airport">Nanjing
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	151	Lukou Airport</A> and via transfer at airports in Hong Kong, Beijing,
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	152	Shanghai and many others. There are also very convenient train
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	153	connections from Shanghai and Beijing, which take slightly more than
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	154	1h from Shanghai and about 4h from Beijing. Travel within Nanjing can
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	155	be done cheaply via taxi and public transport.
2 9bcf6b8176bd added travel Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 1 diff changeset	156
17 a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	157	<p>
a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	158	<center>
a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	159	<div id="map_canvas" style="width: 300px; height: 170px"></div>
a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	160	</center>
a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	161
a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	162	<H4>Venue and Accommodation</H4>
6 5c0d0f923ac2 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 5 diff changeset	163
7 8eeb61050189 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 6 diff changeset	164	The plan is to host the conference at the
59 bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	165	<A HREF="http://english.ctrip.com/hotels/nanjing-hotel-detail-66456/nanjing-hanyuan-mansion-center-of-academic-exchange/">Hanyuan
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	166	Hotel</A>, which is inexpensive
62 1af1e2c8924f updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 61 diff changeset	167	(ca. 350元/£35/$60/€40 per night including breakfast)
61 ee1abe77bda1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 59 diff changeset	168	and in easy reach from the city centre (see <A HREF="https://maps.google.com/maps?q=Hanyuan+Mansion,+20+Tongwei+Road,+Xuanwu,+Nanjing,+Jiangsu,+China,+210095&hl=en&ll=32.029617,118.838768&spn=0.204033,0.292854&sll=32.010405,118.824692&sspn=0.204076,0.292854&t=m&z=12">here</A>
59 bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	169	at Google Maps). It has the usual amenities for hosting conferences
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	170	(Wifi, conference rooms, etc) and has links to neighbouring
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	171	universities. There is also the possibility to use lecture rooms for
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	172	free in Xingyuan's university at the other side of the road. Hanyuan
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	173	Hotel includes a restaurant and there are innumerable <A
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	174	HREF="http://www.chinatour.com/nanjing/nanjing-food.htm">restaurants</A>
55 0835e51e4468 update Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 54 diff changeset	175	around the hotel and in downtown Nanjing, all usually very affordable.
6 5c0d0f923ac2 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 5 diff changeset	176
7 8eeb61050189 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 6 diff changeset	177	<center>
40 b8c65cd84c74 update Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 39 diff changeset	178	<table style="width: 75%">
17 a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	179	<tr>
a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	180	<td>
33 390df693274d fixed errors Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 32 diff changeset	181	<img src="pics/hotel1.jpg" alt="hotel" width="98%" height="21%" border=0>
17 a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	182	</td>
a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	183	<td>
33 390df693274d fixed errors Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 32 diff changeset	184	<img src="pics/hotel2.jpg" alt="hotel" width="98%" height="21%" border=0>
17 a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	185	</td>
37 5d45217fe2e6 update Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 36 diff changeset	186	<td>
40 b8c65cd84c74 update Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 39 diff changeset	187	<img src="pics/hotel4.jpg" alt="hotel" width="98%" height="21%" border=0>
37 5d45217fe2e6 update Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 36 diff changeset	188	</td>
17 a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	189	</tr>
a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	190	<tr>
37 5d45217fe2e6 update Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 36 diff changeset	191	<td colspan="3"><center><small>Hanyuan Hotel</small></center></td>
17 a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	192	</tr>
a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	193	</table>
7 8eeb61050189 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 6 diff changeset	194	</center>
6 5c0d0f923ac2 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 5 diff changeset	195
54 800508ef0e2b update Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 53 diff changeset	196	There are also many additional
58 58619a8f689a update Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 57 diff changeset	197	<A HREF="http://wikitravel.org/en/Nanjing#Sleep">hotels</A> in all price categories nearby.
23 75e46aa48c2f updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 22 diff changeset	198
17 a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	199
6 5c0d0f923ac2 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 5 diff changeset	200	<H4>Advantages of Hosting ITP in Nanjing</H4>
5c0d0f923ac2 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 5 diff changeset	201
23 75e46aa48c2f updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 22 diff changeset	202	There are several groups in the ITP area that are active in China. For example for the last
25 af623d2a1b3e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 24 diff changeset	203	five years there have been popular
52 68a42be6129e update Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 51 diff changeset	204	<A HREF="http://sts.thss.tsinghua.edu.cn/APSSFM_2013">summerschools</A> in China about Coq
22 889666f40918 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 21 diff changeset	205	with 50 or so student participants each. ITP (and TPHOLs) have
59 bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	206	<A HREF="http://www.cs.uwyo.edu/~ruben/itp-2014/Main/History">never</A> been hosted in
21 93e72c39cbbe updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	207	China, and this might be an opportunity for the ITP community to foster relations
93e72c39cbbe updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	208	with researchers from China and Asia, and for local researchers to become part of the
93e72c39cbbe updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	209	ITP community.
6 5c0d0f923ac2 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 5 diff changeset	210
21 93e72c39cbbe updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	211	<p>
93e72c39cbbe updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	212	Being in China, Nanjing offers the usual conveniences of good and
49 64a3b4a50135 update Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 48 diff changeset	213	affordable food. It has several excellent
21 93e72c39cbbe updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	214	<A HREF="http://en.wikipedia.org/wiki/Nanjing#Museums">museums</A>
93e72c39cbbe updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	215	and tourist <A HREF="http://en.wikipedia.org/wiki/Nanjing#Tourism">attractions</A>.
26 abaa87d69a1d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 25 diff changeset	216	In the nearby vicinity are touristic hotspots like
36 ffbfc9fe31fe update Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 35 diff changeset	217	<A HREF="http://en.wikipedia.org/wiki/Yangzhou">Yangzhou</A>,
26 abaa87d69a1d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 25 diff changeset	218	<A HREF="http://en.wikipedia.org/wiki/Hangzhou">Hangzhou</A>,
abaa87d69a1d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 25 diff changeset	219	<A HREF="http://en.wikipedia.org/wiki/Wuxi">Wuxi</A> and
abaa87d69a1d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 25 diff changeset	220	<A HREF="http://en.wikipedia.org/wiki/Suzhou">Suzhou</A>.
21 93e72c39cbbe updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	221	Travelling
93e72c39cbbe updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	222	<A HREF="http://www.travelchinaguide.com/embassy/visa.htm">visas</A>
50 7fed88d4616d update Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	223	to China should be easy to obtain for participants.
21 93e72c39cbbe updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	224
8 adaf6b83330a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 7 diff changeset	225
12 865c16294358 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 11 diff changeset	226	<H4>Excursion</H4>
0 98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	227
23 75e46aa48c2f updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 22 diff changeset	228	We have two possible destinations for an excursion in mind: one is to
56 e92ef125bd82 update Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	229	<A HREF="http://en.wikipedia.org/wiki/Yangzhou">Yangzhou</A> (1h away
59 bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	230	from Nanjing by bus), and the other is a (more leisurely) tour of
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	231	Nanjing and its attractions. The tour to Yangzhou would involve a walk
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	232	around the Slender West Lake with its pavilions, the white Lotus
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	233	Flower Pagoda and the Suzhou-style gardens. One the way we would
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	234	visit the <A HREF="http://arts.cultural-china.com/en/85Arts6286.html">Daming Temple</A>
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	235	and the old Stone Pagoda of Yangzhou. The day
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	236	would finish with a dinner in the well-known
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	237	<A HREF="http://en.wikipedia.org/wiki/Fuchun_Teahouse">Fuchun</A> restaurant. The
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	238	best tour around Nanjing is to go to the
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	239	<A HREF="http://en.wikipedia.org/wiki/Purple_Mountain">Purple Mountains</A> passing by
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	240	the <A HREF="http://en.wikipedia.org/wiki/Linggu_Temple">Linggusi</A> pagoda,
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	241	the <A HREF="http://en.wikipedia.org/wiki/City_Wall_of_Nanjing">city wall</A> and the
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	242	<A HREF="http://en.wikipedia.org/wiki/Ming_Xiaoling_Mausoleum">Ming tombs</A> (see pictures on
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	243	the left). There is a wide selection of excellent restaurants around
65 aba8911d873e some small changes after the bid Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 64 diff changeset	244	Nanjing's Confucius Temple for a conference dinner. We will canvas for opinions about
aba8911d873e some small changes after the bid Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 64 diff changeset	245	what participants would be most interested in.
59 bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	246
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	247	<center>
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	248	<table style="width: 75%">
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	249	<tr>
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	250	<td>
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	251	<img src="pics/Yangzhou2.jpg" alt="Yangzhou" width="98%" height="21%" border=0>
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	252	</td>
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	253	<td>
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	254	<img src="pics/Yangzhou1.jpg" alt="Yangzhou" width="98%" height="21%" border=0>
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	255	</td>
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	256	<td>
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	257	<img src="pics/Yangzhou3.jpg" alt="Yangzhou" width="98%" height="21%" border=0>
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	258	</td>
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	259	</tr>
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	260	<tr>
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	261	<td colspan="3"><center><small>Yangzhou, Slender West Lake</small></center></td>
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	262	</tr>
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	263	</table>
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	264	</center>
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	265
0 98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	266
18 c4dc7907c66b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 17 diff changeset	267	<H4>Finance</H4>
0 98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	268
21 93e72c39cbbe updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	269	We will seek to keep costs low by negotiating discounts with
23 75e46aa48c2f updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 22 diff changeset	270	the hotel and by trying to find sponsoring where sensible.
0 98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	271
52 68a42be6129e update Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 51 diff changeset	272	<H4>Experience of the Programme Chairs and Local Organisation</H4>
0 98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	273
52 68a42be6129e update Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 51 diff changeset	274	Xingyuan and Christian are regular participants at ITP. Christian was a
68a42be6129e update Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 51 diff changeset	275	co-organiser of the TPHOLs conference
21 93e72c39cbbe updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	276	in 2009 in <A HREF="http://isabelle.in.tum.de/nominal/activities/tphols09/">Munich</A>.
52 68a42be6129e update Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 51 diff changeset	277	We will make use of the infrastructure available at Xingyuan's university for local
53 08280615de4a update Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 52 diff changeset	278	organisation. There will also be a student team that helps with running the conference.
0 98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	279	</TD>
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	280	</TR>
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	281	</TABLE>
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	282
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	283	<hr>
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	284	<a href="http://validator.w3.org/check/referer">[Validate this page.]</a>
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	285	</body>
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	286	</html>

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Tue, 12 Aug 2014 14:45:03 +0100
changeset 76	56c28e4152f0
parent 75	5868d8f8649f
child 80	571250c1b210
permissions	-rw-r--r--