itp-2015: index.html@ad23aa434cd1 (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">
184 8d2a12050a75 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 180 diff changeset	33	body { font-family: "trebuchet ms", helvetica, sans-serif; }
15 9052a9b07b59 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 14 diff changeset	34	</style>
0 98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	35	</head>
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	36
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	37	<BODY TEXT="#000000"
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	38	BGCOLOR="#4169E1"
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	39	LINK="#0000EF"
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	40	VLINK="#51188E"
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	41	ALINK="#FF0000"
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	42	onload="initialize()" onunload="GUnload()">
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	43
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	44	<TABLE WIDTH="100%"
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	45	BGCOLOR="#4169E1"
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	46	BORDER="0"
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	47	FRAME="border"
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	48	CELLPADDING="10"
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	49	CELLSPACING="2"
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	50	RULES="all">
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	51
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	52	<!-- left column -->
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	53	<TR>
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	54	<TD BGCOLOR="#FFFFFF"
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	55	WIDTH="20%"
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	56	VALIGN="TOP"
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	57	ROWSPAN="2">
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	58
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	<p align=center>
18 c4dc7907c66b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 17 diff changeset	61	<a href="pics/ITP-Linggusu.jpg">
26 abaa87d69a1d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 25 diff changeset	62	<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	63	<br>
26 abaa87d69a1d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 25 diff changeset	64	Linggusi pagoda<br>
0 98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	65	</p>
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	66
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	67	<p align=center>
18 c4dc7907c66b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 17 diff changeset	68	<a href="pics/ITP-Mochou.jpg">
22 889666f40918 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 21 diff changeset	69	<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	70	<br>
26 abaa87d69a1d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 25 diff changeset	71	Mochou Lake Park<br>
0 98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	72	</p>
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	73
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	74	<p align=center>
18 c4dc7907c66b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 17 diff changeset	75	<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	76	<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	77	<br>
26 abaa87d69a1d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 25 diff changeset	78	Nanjing city wall<br>
20 a78382005a14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 19 diff changeset	79	</p>
a78382005a14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 19 diff changeset	80
a78382005a14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 19 diff changeset	81	<p align=center>
a78382005a14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 19 diff changeset	82	<a href="pics/Nanjing2.jpg">
a78382005a14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 19 diff changeset	83	<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	84	<br>
109 d1b952e3431d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	85	`"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	86	</p>
4dab946931d8 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 23 diff changeset	87
4dab946931d8 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 23 diff changeset	88	<p align=center>
4dab946931d8 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 23 diff changeset	89	<a href="pics/Nanjing3.jpg">
4dab946931d8 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 23 diff changeset	90	<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	91	<br>
26 abaa87d69a1d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 25 diff changeset	92	Nanjing's skyline<br>
25 af623d2a1b3e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 24 diff changeset	93	</p>
af623d2a1b3e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 24 diff changeset	94
af623d2a1b3e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 24 diff changeset	95	<p align=center>
af623d2a1b3e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 24 diff changeset	96	<a href="pics/Nanjing4.jpg">
af623d2a1b3e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 24 diff changeset	97	<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	98	<br>
26 abaa87d69a1d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 25 diff changeset	99	Science and Technology<br> Museum<br>
25 af623d2a1b3e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 24 diff changeset	100	</p>
0 98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	101
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	102	</TD>
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	103
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	<!-- right column -->
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	106	<TD BGCOLOR="#FFFFFF" WIDTH="75%" VALIGN="TOP">
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	107	<TABLE>
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	108	<TR>
82 7b71e2c2b422 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 80 diff changeset	109	<TD><H1>ITP 2015 will be in Nanjing, China</H1></TD>
184 8d2a12050a75 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 180 diff changeset	110	<TD align="right" valign="top"><img src="pics/nanjing-map.jpg" width="42%" height="40%" alt="ITP" align="top"></TD>
0 98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	111	</TR>
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	112	</TABLE>
89 6861b6c7446a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 88 diff changeset	113
75 5868d8f8649f added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 70 diff changeset	114	<p>
82 7b71e2c2b422 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 80 diff changeset	115	<HR>
89 6861b6c7446a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 88 diff changeset	116	[<A HREF="index.html#dates">Important Dates</A>]
139 4b5c18028ec6 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 138 diff changeset	117	[<A HREF="index.html#programme">Programme</A>]
171 fd47136d623a Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 170 diff changeset	118	[<A HREF="index.html#travel">Travel + Registration</A>]
307 9d9e004c540f updated link Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 286 diff changeset	119	[<A HREF="booklet2.pdf">ITP Booklet</A>]
171 fd47136d623a Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 170 diff changeset	120	<BR>
139 4b5c18028ec6 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 138 diff changeset	121	[<A HREF="accepted.html">Accepted Papers</A>]
82 7b71e2c2b422 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 80 diff changeset	122	[<A HREF="cfp.pdf">CFP</A>]
89 6861b6c7446a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 88 diff changeset	123	[<A HREF="index.html#committees">Committees</A>]
80 571250c1b210 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 76 diff changeset	124	[<A HREF="history.html">Conference History</A>]
116 4718e6804c94 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 114 diff changeset	125	[<A HREF="bids-2016.html">ITP 2016 Bids</A>]
89 6861b6c7446a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 88 diff changeset	126	<HR>
90 566dc939e9cf updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 89 diff changeset	127
75 5868d8f8649f added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 70 diff changeset	128
5868d8f8649f added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 70 diff changeset	129	<p>
65 aba8911d873e some small changes after the bid Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 64 diff changeset	130	The 6th conference on Interactive Theorem Proving will be held in
93 9eb085881cd5 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 92 diff changeset	131	Nanjing, China.
59 bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	132	<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	133	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	134	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	135	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	136	HREF="http://www.cityofnanjing.com">cultural heritage</A>.
309 d89e541bbde9 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 307 diff changeset	137	The proceedings will be published as usual in the
d89e541bbde9 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 307 diff changeset	138	<A HREF="http://link.springer.com/book/10.1007/978-3-319-22102-1">LNCS</A>
262 26b193439245 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	139	Series. There will be an
26b193439245 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	140	<A HREF="http://www21.in.tum.de/~nipkow/isa-tut-itp15.html">Isabelle tutorial</A> before the
263 4979283341dc updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 262 diff changeset	141	conference (21 - 23 August), and
262 26b193439245 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	142	a <A HREF="http://www.strub.nu/coq-itp-15">Coq tutorial</A> after the conference
26b193439245 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 261 diff changeset	143	(27 - 29 August).
147 9b9e6590882e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 146 diff changeset	144
9b9e6590882e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 146 diff changeset	145	<p>
286 f700d78f7924 updated page Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 283 diff changeset	146	<IMG SRC="pics/new.gif" ALT="" style="" align="left"><A HREF="http://talisker.inf.kcl.ac.uk/%7Eurbanc/cgi-bin/repos.cgi/itp-2015/raw-file/tip/prog.pdf">Preliminary programme</A><BR><BR>
307 9d9e004c540f updated link Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 286 diff changeset	147	<IMG SRC="pics/new.gif" ALT="" style="" align="left"><A HREF="booklet2.pdf">ITP Booklet</A>,
188 71eb49da978f updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 187 diff changeset	148	contains practical information about registration, travelling, etc.<BR><BR>
86 99f336f35f87 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 84 diff changeset	149	</p>
99f336f35f87 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 84 diff changeset	150
99f336f35f87 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 84 diff changeset	151	<H4><A NAME="dates"></A>Important Dates</H4>
99f336f35f87 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 84 diff changeset	152
84 2e2e4680a9d2 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 82 diff changeset	153	Submission of title and abstracts: 9 March 2015<BR>
113 a48645d86b36 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 111 diff changeset	154	Submission of full papers: <strike>13 March 2015</strike> 20 March 2015
a48645d86b36 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 111 diff changeset	155	<font color="red">closed</font><BR>
82 7b71e2c2b422 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 80 diff changeset	156	Author notification: 15 May 2015<BR>
7b71e2c2b422 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 80 diff changeset	157	Camera-ready papers: 5 June 2015<BR>
87 c8156c1b463c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 86 diff changeset	158	Conference: 24-27 August 2015<BR>
107 6de6964d9680 added submission page Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	159	<A HREF="https://easychair.org/conferences/?conf=itp2015">Submission page</A><BR>
82 7b71e2c2b422 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 80 diff changeset	160
139 4b5c18028ec6 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 138 diff changeset	161	<H4><A NAME="programme">Tentative Programme</H4>
69 43da71639190 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 65 diff changeset	162
264 7eeaa39d25e8 updated prog Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 263 diff changeset	163	As is the tradition, the conference consists of 4 days
75 5868d8f8649f added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 70 diff changeset	164	of research presentations and invited talks. Like in previous
264 7eeaa39d25e8 updated prog Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 263 diff changeset	165	conferences, we will have ample time between the formal sessions for
75 5868d8f8649f added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 70 diff changeset	166	attendees to mingle and converse. Half a day will be dedicated to an
133 7d35f05836fd updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 132 diff changeset	167	excursion to <A HREF="http://en.wikipedia.org/wiki/Yangzhou">Yangzhou</A>
7d35f05836fd updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 132 diff changeset	168	and the <A HREF="http://en.wikipedia.org/wiki/Yangzhou#Slender_West_Lake">Slender West Lake</A>.
264 7eeaa39d25e8 updated prog Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 263 diff changeset	169	The preliminary programme of talks can be found
7eeaa39d25e8 updated prog Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 263 diff changeset	170	<A HREF="http://talisker.inf.kcl.ac.uk/%7Eurbanc/cgi-bin/repos.cgi/itp-2015/raw-file/tip/prog.pdf">here</A>.
7eeaa39d25e8 updated prog Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 263 diff changeset	171
69 43da71639190 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 65 diff changeset	172
141 8fea16405d08 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 140 diff changeset	173	<H4><A NAME="travel">Travel to Nanjing</H4>
0 98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	174
59 bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	175	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	176	connections directly to <A
bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	177	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	178	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	179	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	180	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	181	1h from Shanghai and about 4h from Beijing. Travel within Nanjing can
282 ebb313189536 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 264 diff changeset	182	be done cheaply via taxi and public transport. Hopefully helpful tips
ebb313189536 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 264 diff changeset	183	for travelling in Nanjing and China can be found in the
307 9d9e004c540f updated link Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 286 diff changeset	184	<A HREF="booklet2.pdf">booklet</A>.
2 9bcf6b8176bd added travel Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 1 diff changeset	185
17 a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	186	<p>
163 76e279bf3563 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 162 diff changeset	187	Remember that travelling to China requires a
76e279bf3563 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 162 diff changeset	188	<A HREF="http://www.travelchinaguide.com/embassy/visa.htm">visa</A>;
174 79d4ade4adb4 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 173 diff changeset	189	but it should be relatively easy to obtain one for participants. You will need
173 f1bc1d0881a1 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 172 diff changeset	190	a letter of invitation which Chunhan will send you (chunhanwu at 126 dot com).
180 dda7cb026a2e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 177 diff changeset	191	You need to provide him with your name, title, DOB, work address, e-mail and paper title
307 9d9e004c540f updated link Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 286 diff changeset	192	(if you present a paper). See the <A HREF="booklet2.pdf">booklet</A> for
173 f1bc1d0881a1 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 172 diff changeset	193	details about the visa application.
135 7294b3fd68dc updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	194
7294b3fd68dc updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	195	<p>
17 a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	196	<center>
a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	197	<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	198	</center>
a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	199
152 ff43f5f28656 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	200	<H4>Registration</H4>
ff43f5f28656 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	201
171 fd47136d623a Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 170 diff changeset	202	The early rate of the registration fee will be 3300元 (ca. £350/$533/€488).
170 35d8162d935b Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 169 diff changeset	203	The late rate starting from 1 August will be 3800元.
172 5d2e61a18fd7 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 171 diff changeset	204	The registration fee includes lunches during the
185 9ce7445ca4e2 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 184 diff changeset	205	conference. It also covers the excursion, the conference banquet and a welcome reception.
9ce7445ca4e2 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 184 diff changeset	206	The tutorials are separate. Their registration fee is 250元 for the Isabelle-tutorial
9ce7445ca4e2 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 184 diff changeset	207	and 200元 for the Coq-tutorial.
9ce7445ca4e2 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 184 diff changeset	208
9ce7445ca4e2 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 184 diff changeset	209	<p>
187 8cfc96642da5 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 186 diff changeset	210	The registration fee needs to be transferred via a bank
160 2bb006aee53b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 159 diff changeset	211	transfer; we <span style="text-decoration: underline;"><B>cannot</B></span>
161 99cd8611c244 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 160 diff changeset	212	accept credit cards etc for the conference fee. The hotel and many other things can be paid
307 9d9e004c540f updated link Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 286 diff changeset	213	by credit card, but not the conference fee. See the <A HREF="booklet2.pdf">booklet</A> for
172 5d2e61a18fd7 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 171 diff changeset	214	details about the bank transfer.
145 da73d9e9c606 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 144 diff changeset	215
17 a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	216	<H4>Venue and Accommodation</H4>
6 5c0d0f923ac2 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 5 diff changeset	217
111 ce6e1152d777 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 109 diff changeset	218	The conference will take place at the
126 f242e25a4b48 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 125 diff changeset	219	<A HREF="http://english.ctrip.com/hotels/nanjing-hotel-detail-66456/nanjing-hanyuan-mansion-center-of-academic-exchange/">Hanyuan
114 0f589d1fb51a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 113 diff changeset	220	Hotel</A>, which is relatively inexpensive
170 35d8162d935b Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 169 diff changeset	221	(ca. 390元/£34/$52/€47 per night including breakfast)
61 ee1abe77bda1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 59 diff changeset	222	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>
163 76e279bf3563 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 162 diff changeset	223	at Google Maps). The conference hotel has the usual amenities (Wifi, conference rooms, etc)
177 f7241974b3ae Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 176 diff changeset	224	and includes a restaurant.
172 5d2e61a18fd7 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 171 diff changeset	225	We have reserved some rooms in the hotel for participants. See the
307 9d9e004c540f updated link Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 286 diff changeset	226	<A HREF="booklet2.pdf">booklet</A> for information about the hotel booking.
172 5d2e61a18fd7 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 171 diff changeset	227
163 76e279bf3563 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 162 diff changeset	228
162 63383d98c87a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 161 diff changeset	229	<p>
7 8eeb61050189 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 6 diff changeset	230	<center>
40 b8c65cd84c74 update Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 39 diff changeset	231	<table style="width: 75%">
17 a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	232	<tr>
a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	233	<td>
33 390df693274d fixed errors Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 32 diff changeset	234	<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	235	</td>
a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	236	<td>
33 390df693274d fixed errors Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 32 diff changeset	237	<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	238	</td>
37 5d45217fe2e6 update Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 36 diff changeset	239	<td>
40 b8c65cd84c74 update Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 39 diff changeset	240	<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	241	</td>
17 a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	242	</tr>
a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	243	<tr>
37 5d45217fe2e6 update Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 36 diff changeset	244	<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	245	</tr>
a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	246	</table>
7 8eeb61050189 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 6 diff changeset	247	</center>
6 5c0d0f923ac2 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 5 diff changeset	248
164 942dbc16733c Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 163 diff changeset	249	<p>
942dbc16733c Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 163 diff changeset	250	There are also many additional
942dbc16733c Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 163 diff changeset	251	<A HREF="http://wikitravel.org/en/Nanjing#Sleep">hotels</A> in all price categories nearby.
942dbc16733c Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 163 diff changeset	252	Also there are innumerable <A
942dbc16733c Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 163 diff changeset	253	HREF="http://www.chinatour.com/nanjing/nanjing-food.htm">restaurants</A> in the area.
942dbc16733c Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 163 diff changeset	254
17 a512aa90613b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 16 diff changeset	255
86 99f336f35f87 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 84 diff changeset	256	<H4>Local Information</H4>
6 5c0d0f923ac2 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 5 diff changeset	257
146 5db9bd259266 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 145 diff changeset	258
6 5c0d0f923ac2 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 5 diff changeset	259
21 93e72c39cbbe updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	260	<p>
93e72c39cbbe updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	261	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	262	affordable food. It has several excellent
21 93e72c39cbbe updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	263	<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	264	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	265	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	266	<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	267	<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	268	<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	269	<A HREF="http://en.wikipedia.org/wiki/Suzhou">Suzhou</A>.
135 7294b3fd68dc updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	270	If you want to explore Nanjing yourself, the best tour is to go to the
7294b3fd68dc updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	271	<A HREF="http://en.wikipedia.org/wiki/Purple_Mountain">Purple Mountains</A> passing by
7294b3fd68dc updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	272	the <A HREF="http://en.wikipedia.org/wiki/Linggu_Temple">Linggusi</A> pagoda,
7294b3fd68dc updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	273	the <A HREF="http://en.wikipedia.org/wiki/City_Wall_of_Nanjing">city wall</A> and the
7294b3fd68dc updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	274	<A HREF="http://en.wikipedia.org/wiki/Ming_Xiaoling_Mausoleum">Ming tombs</A> (see pictures on
7294b3fd68dc updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	275	the left). There is a wide selection of excellent restaurants around
7294b3fd68dc updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	276	Nanjing's Confucius Temple.
7294b3fd68dc updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	277
7294b3fd68dc updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 134 diff changeset	278
12 865c16294358 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 11 diff changeset	279	<H4>Excursion</H4>
0 98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	280
134 6a5c643fbed7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	281	The excursion will be to
56 e92ef125bd82 update Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 diff changeset	282	<A HREF="http://en.wikipedia.org/wiki/Yangzhou">Yangzhou</A> (1h away
134 6a5c643fbed7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	283	from Nanjing by bus). The tour will include a walk
59 bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	284	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	285	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	286	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	287	and the old Stone Pagoda of Yangzhou. The day
134 6a5c643fbed7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	288	will finish with a dinner in the well-known
6a5c643fbed7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	289	<A HREF="http://en.wikipedia.org/wiki/Fuchun_Teahouse">Fuchun</A> restaurant.
6a5c643fbed7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	290
138 8c3343a78af5 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	291	<center>
8c3343a78af5 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	292	<table style="width: 75%">
8c3343a78af5 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	293	<tr>
8c3343a78af5 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	294	<td>
8c3343a78af5 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	295	<img src="pics/Yangzhou2.jpg" alt="Yangzhou" width="98%" height="21%" border=0>
8c3343a78af5 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	296	</td>
8c3343a78af5 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	297	<td>
8c3343a78af5 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	298	<img src="pics/Yangzhou1.jpg" alt="Yangzhou" width="98%" height="21%" border=0>
8c3343a78af5 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	299	</td>
8c3343a78af5 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	300	<td>
8c3343a78af5 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	301	<img src="pics/Yangzhou3.jpg" alt="Yangzhou" width="98%" height="21%" border=0>
8c3343a78af5 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	302	</td>
8c3343a78af5 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	303	</tr>
8c3343a78af5 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	304	<tr>
8c3343a78af5 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	305	<td colspan="3"><center><small>Yangzhou, Slender West Lake</small></center></td>
8c3343a78af5 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	306	</tr>
8c3343a78af5 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	307	</table>
8c3343a78af5 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	308	</center>
8c3343a78af5 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	309
137 2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	310
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	311	<H4><A NAME="committees"></A>Programme Committee</H4>
134 6a5c643fbed7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 133 diff changeset	312
137 2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	313	<TABLE>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	314	<TR><TD><A HREF="http://www.cs.unibo.it/~asperti/">Andrea Asperti</A></TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	315	<TD>University of Bologna, Italy</TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	316	</TR>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	317	<TR><TD><A HREF="http://www.itu.dk/people/jebe/">Jesper Bengtson</A></TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	318	<TD>IT University of Copenhagen, Denmark</TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	319	</TR>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	320	<TR><TD><A HREF="http://wwwbroy.in.tum.de/~berghofe/">Stefan Berghofer</A></TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	321	<TD>Secunet Security Networks AG, Germany</TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	322	</TR>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	323	<TR><TD><A HREF="http://www-sop.inria.fr/members/Yves.Bertot/">Yves Bertot</A></TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	324	<TD>INRIA, France</TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	325	</TR>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	326	<TR><TD><A HREF="http://cs.au.dk/~birke/">Lars Birkedal</A></TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	327	<TD>Aarhus University, Denmark</TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	328	</TR>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	329	<TR><TD><A HREF="https://www.irisa.fr/celtique/blazy/index.html">Sandrine Blazy</A></TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	330	<TD>University of Rennes, France</TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	331	</TR>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	332	<TR><TD><A HREF="http://www.cs.cornell.edu/home/rc/">Bob Constable</A></TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	333	<TD>Cornell University, USA</TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	334	</TR>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	335	<TR><TD><A HREF="http://www.cse.chalmers.se/~coquand/">Thierry Coquand</A></TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	336	<TD>University of Gothenburg, Sweden</TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	337	</TR>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	338	<TR><TD><A HREF="http://staff.ustc.edu.cn/~xyfeng/">Xinyu Feng</A></TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	339	<TD>University of Science and Technology, China</TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	340	</TR>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	341	<TR><TD><A HREF="http://www.cs.uwyo.edu/~ruben/">Ruben Gamboa</A></TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	342	<TD>University of Wyoming, USA</TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	343	</TR>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	344	<TR><TD><A HREF="http://www.cs.ru.nl/~herman/">Herman Geuvers</A></TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	345	<TD>Radboud University Nijmegen, The Netherlands</TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	346	</TR>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	347	<TR><TD><A HREF="http://www.cl.cam.ac.uk/~mjcg/">Mike Gordon</A></TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	348	<TD>Cambridge University, United Kingdom</TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	349	</TR>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	350	<TR><TD><A HREF="http://web.engr.illinois.edu/~egunter/">Elsa Gunter</A></TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	351	<TD>University of Illinois, Urbana-Champaign, USA</TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	352	</TR>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	353	<TR><TD><A HREF="http://www.cl.cam.ac.uk/~jrh13/">John Harrison</A></TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	354	<TD>Intel Corporation, USA</TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	355	</TR>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	356	<TR><TD><A HREF="http://pauillac.inria.fr/~herbelin/index-eng.html">Hugo Herbelin</A></TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	357	<TD>INRIA, France</TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	358	</TR>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	359	<TR><TD><A HREF="http://www.cs.utexas.edu/~kaufmann/">Matt Kaufmann</A></TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	360	<TD>University of Texas at Austin, USA</TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	361	</TR>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	362	<TR><TD><A HREF="http://www.cse.unsw.edu.au/~kleing/">Gerwin Klein</A></TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	363	<TD>NICTA, Australia</TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	364	</TR>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	365	<TR><TD><A HREF="http://shemesh.larc.nasa.gov/people/cam/">César Muñoz</A></TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	366	<TD>NASA Langley Research Center, USA</TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	367	</TR>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	368	<TR><TD><A HREF="http://www21.in.tum.de/~nipkow/">Tobias Nipkow</A></TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	369	<TD>TU München, Germany</TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	370	</TR>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	371	<TR><TD><A HREF="http://nicta.com.au/people/norrishm">Michael Norrish</A></TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	372	<TD>NICTA, Australia</TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	373	</TR>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	374	<TR><TD><A HREF="http://www.cs.kent.ac.uk/people/staff/sao/">Scott Owens</A></TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	375	<TD>University of Kent, United Kingdom</TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	376	</TR>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	377	<TR><TD><A HREF="http://homepages.inf.ed.ac.uk/rpollack/">Randy Pollack</A></TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	378	<TD>Harvard University, USA</TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	379	</TR>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	380	<TR><TD><A HREF="http://www.itu.dk/people/carsten/">Carsten Schürmann</A></TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	381	<TD>IT University of Copenhagen, Denmark</TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	382	</TR>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	383	<TR><TD><A HREF="http://loonwerks.com/people/konrad-slind.html">Konrad Slind</A></TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	384	<TD>Rockwell Collins, USA</TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	385	</TR>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	386	<TR><TD><A HREF="http://www.ntu.edu.sg/home/atiu/">Alwen Tiu</A></TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	387	<TD>Nanyang Technological University, Singapore</TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	388	</TR>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	389	<TR><TD><A HREF="http://www.inf.kcl.ac.uk/staff/urbanc/">Christian Urban</A> (co-chair) </TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	390	<TD>King's College London, United Kingdom</TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	391	</TR>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	392	<TR><TD><A HREF="http://research.microsoft.com/en-us/people/dimitris/">Dimitrios Vytiniotis</A></TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	393	<TD>Microsoft Research Cambridge, United Kingdom</TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	394	</TR>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	395	<TR><TD>Xingyuan Zhang (co-chair)</TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	396	<TD>PLA University of Science and Technology, China</TD>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	397	</TR>
2aa7e50835ff updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 136 diff changeset	398	</TABLE>
59 bdf7a09e950b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 58 diff changeset	399
0 98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	400
18 c4dc7907c66b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 17 diff changeset	401	<H4>Finance</H4>
0 98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	402
155 aeb4ce6b7ef3 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	403	We are grateful for the generous support received from the PLA University of
138 8c3343a78af5 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 137 diff changeset	404	Science and Technology in Nanjing.
0 98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	405
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	406	</TD>
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	407	</TR>
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	408	</TABLE>
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	409
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	410	<hr>
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	411	<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	412	</body>
98b6328773c2 initial commit Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	413	</html>

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Thu, 20 Aug 2015 11:32:02 +0800
changeset 311	ad23aa434cd1
parent 309	d89e541bbde9
child 312	f40c44330340
permissions	-rw-r--r--