165
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1
\documentclass[11pt]{report}
252
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 2
\usepackage{dina4}
165
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 3
\usepackage{eurosym}
166
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 4
\usepackage{fontspec}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 5
\usepackage[sc]{mathpazo}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 6
\setmainfont[Ligatures=TeX]{Palatino Linotype}
252
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 7
\usepackage{fancyvrb}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 8
\usepackage[table]{xcolor}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 9
\usepackage{floatpag}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 10
\floatpagestyle{empty}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 11
\definecolor{linkcolor}{rgb}{0,0,0.5}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 12
\usepackage[colorlinks=true,linkcolor=linkcolor,citecolor=linkcolor,filecolor=linkcolor,pagecolor=linkcolor,urlcolor=linkcolor]{hyperref}
168
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 13
257
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 14
%\usepackage{xeCJK}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 15
%\setCJKmainfont[BoldFont=STZhongsong, ItalicFont=STKaiti]{STSong}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 16
%\setCJKsansfont[BoldFont=STHeiti]{STXihei}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 17
%\setCJKmonofont{STFangsong}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 19
168
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 20
\def\xyzemail{xingyuanzhang at 126 dot com}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 21
\def\cwemail{chunhanwu at 126 dot com}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 22
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 23
165
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 24
\begin{document}
169
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 25
\title{\LARGE\bf ITP 2015 Conference Booklet}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 26
\author{Xingyuan Zhang, Chunhan Wu and Christian Urban}
165
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 27
\date{\today}
170
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 28
%%\tableofcontents
165
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 29
\maketitle
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 30
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 31
\chapter{Pre-Arrival}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 32
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 33
\section{Registration and Conference Fee}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 34
166
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 35
In short
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 36
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 37
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 38
\item[(1)] you need to make a bank transfer for the conference
198
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 39
fee in your local currency, and
166
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 40
\item[(2)] you need to email Xingyuan with your details\\
168
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 41
(\xyzemail)
166
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 42
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 43
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 44
\noindent Xingyuan will then confirm that the payment has been
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 45
received. Note that if you are Chinese and need a \emph{fa
169
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 46
piao} to reclaim the conference fee, you need to contact
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 47
Xingyuan directly before making any money transfer.
166
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 48
\medskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 49
170
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 50
\noindent The early conference fee is RMB 3300, which is
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 51
approximately \pounds{}350, \$533, or \euro{}488. It must be
198
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 52
transferred via bank transfer and must be made in your local
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 53
currency; we cannot accept any other form of payment. The
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 54
tutorials can be registered independently from the conference.
170
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 55
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 56
The conference fee includes lunches during the conference. It
172
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 57
also covers the excursion, the conference banquet and a
170
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 58
welcome reception.
165
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 59
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 60
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 61
\begin{tabular}{l@{\hspace{4mm}}l}
170
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 62
Early conference fee until 31.~July: & RMB 3300\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 63
Late conference fee from 1.~August: & RMB 3800\bigskip\\
165
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 64
170
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 65
Additional banquet dinner and excursion: & RMB 530\\
169
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 66
(one is included in the conference fee)\bigskip\\
165
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 67
170
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 68
Isabelle tutorial (21 -- 23 August): & RMB 250\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 69
Coq tutorial (27 -- 29 August): & RMB 200\\
165
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 70
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 71
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 72
191
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 73
\noindent The amount payable needs to be
190
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 74
transferred to the account:
166
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 75
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 76
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 77
\begin{tabular}{ll}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 78
Account holder's name:& Zhang Xingyuan\medskip\\
Beneficiary bank:& BANK OF CHINA\medskip\\
Swift Code:& BKCHCNBJ940\medskip\\
Account number:& 504066588897\medskip\\
Beneficiary bank address:& Nanjing Mei Hua Shan Zhuang\\
170
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 79
& Sub-branch, Nanjing, China\medskip\\
Account holder's address:& \\
169
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 80
& Suite 2106, Building 20,\\
& 20 Biao Ying,\\
& Qinhuai District,\\
& Nanjing, Jiangsu Province,\\
& People's Republic of China.\\
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 81
\end{center}
\noindent {\bf Please make doubly-sure that your bank
170
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 82
transferral contains your full name as reference (additional
198
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 83
information field), and is in your local currency
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 84
(e.g.~\euro, \$, \pounds)!} Otherwise we will have no idea
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 85
where the money came from, and will not be able to receive
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 86
the money on our end. Please also make sure that your transferral
170
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 87
covers all bank fees.\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 88
\section{Hotel Booking}
In short, you need to send your arrival and departure
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 89
details to Chunhan
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 90
(\cwemail).\bigskip
166
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 91
170
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 92
\noindent While it is possible to book the hotel via official
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 93
online travel web-pages, the price there is higher. The
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 94
easiest is to send Chunhan your name, arrival and departure
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 95
dates and he will send you back a booking ticket from Hanyuan
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 96
hotel, which you might need for your visa application.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 97
You can pay the hotel when you arrive using Visa or
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 98
MasterCard.
166
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 99
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 100
\section{Visa}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 101
168
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 102
Please be aware that for travelling to China you will need a
178
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 103
visa, for which you have to apply {\bf beforehand}. It often takes
168
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 104
one or two weeks before a visa is granted. Though if you
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 105
are prepared to pay a higher application fee, then you can
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 106
shorten the delay to a few days. For the visa you
170
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 107
will need an invitation letter, which Chunhan will send you
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 108
(\cwemail). You need to provide him with your name, title,
180
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 109
DOB, work address, e-mail and paper title (if you present a paper).
170
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 110
He will e-mail you the invitation letter. You might also need
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 111
your hotel booking (see above) and flight details for the visa
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 112
application.
252
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 113
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 114
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 115
\chapter{Arrival}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 116
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 117
Welcome in China. You made it to the destination airport.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 118
Unless your are one of the very few foreigners who can speak
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 119
and read Chinese, potentially the most challenging part of
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 120
your journey is about to begin. Below we explain how to get to
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 121
Hanyuan Hotel in Nanjing from Nanjing Lukou Airport and from
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 122
Shanghai Pudong Airport. If you arrive from somewhere else and
269
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 123
need help, please let us know. If you need help while
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 124
travelling, the local organisers can be reached on their
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 125
mobile:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 126
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 127
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 128
\begin{tabular}{ll}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 129
Xingyuan: & (+86)\hspace{2mm}13814081536\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 130
Chunhan: & (+86)\hspace{2mm}15312993807\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 131
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 132
\end{center}
252
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 133
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 134
China is generally a safe country for travelling, if the usual
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 135
precautions are taken. We assume you have never been in China
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 136
before, therefore let us still start with some general points.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 137
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 138
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 139
\item \textbf{Weather}\hspace{3mm}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 140
Unfortunately end of August is the time when it will be especially
257
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 141
hot in Nanjing (usually above 30$^{\circ}$C). Be prepared with lots of
252
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 142
light clothes, but do not forget a jumper, or sweater, since many
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 143
places are air-conditioned. It can also rain.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 144
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 145
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 146
\item \textbf{Bottled Water}\hspace{3mm}
252
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 147
Whereas in many places it is safe to drink water from taps,
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 148
do not take chances and drink only bottled water! During the
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 149
conference we will provide bottled water. In other places you
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 150
have to buy bottles yourself. Remember, Chinese are famous for
269
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 151
nibbling on a bottle of hot tea the whole day, even in sweltering
252
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 152
temperatures. There is a reason for this.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 153
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 154
\item \textbf{Traffic}\hspace{3mm}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 155
Do not even think of renting a car in China. Hence, while in
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 156
China, you probably will be mostly going around on foot. Be
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 157
careful though: You might come from a region where traffic rules are
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 158
organised so that pedestrians are mostly
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 159
treated with respect by all other road users, or even have an
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 160
``elevated status'' because they are considered the ``weakest''.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 161
Traffic in China is, in contrast, organised more, shall we say,
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 162
according to a Darwinian model: Under no circumstance assume a
257
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 163
car (or even a bicycle or one of the noiseless electric motor bikes) will stop for you. As pedestrian, you
252
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 164
have to take care of everybody else. Therefore, whenever
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 165
possible cross roads at traffic lights and even if the light
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 166
shows green for you, look out for cars that pay no attention to this
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 167
fact. Also, zebra crossings do \emph{not}, I repeat, \emph{do not}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 168
have any special meaning in
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 169
China for the road users higher up the traffic ladder
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 170
(i.e.~bicycles and above).
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 171
Even if it sounds too funny, take
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 172
our word and head this advice\ldots{}it might increase your
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 173
life-expectancy.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 174
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 175
\item \textbf{Free Public Wifi / Mobile Phones}\hspace{3mm}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 176
While free public wifi is nowadays pretty ubiquitous in big
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 177
cities in China (Starbucks, Costas, McDonalds are obvious
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 178
places where to find wifi), you need a working mobile phone in
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 179
order to use it. You will have to register your number when
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 180
you log in, and the wifi operator will then send you a
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 181
password token via SMS. The problem is that chances are great
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 182
your mobile phone will \emph{not} work in China. Therefore do
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 183
not assume you can check information on the Internet while
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 184
travelling.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 185
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 186
At the hotel there will be wifi (with the super-secure
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 187
password: 123456789). But again, do not assume you can
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 188
download that last episode of the Daily Show: while bandwidth
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 189
will generally be enough for reading email, be prepared for an
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 190
uninterrupted stay in China, free from any disturbance coming
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 191
from online demands.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 192
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 193
\item \textbf{Google etc}\hspace{3mm}There are two Great Walls in
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 194
China: one prevents you from accessing Google, for example. Use
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 195
\url{www.aol.com} or \url{www.bing.com} instead as your preferred
257
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 196
search engine. Also, if you care about such things, set your
252
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 197
status on Facebook to ``unavailable'' for the period of time
267
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 198
you will be in China. Ditto Twitter.
257
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 199
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 200
\item \textbf{Map of Hotel / Taxis}\hspace{3mm} While more and
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 201
more young Chinese are exposed to English, you cannot
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 202
rely on anyone of the general public speaking more than a few
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 203
words. Rather, you have to always calculate with the very,
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 204
very likely scenario that nobody speaks any English at all
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 205
and all
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 206
signs round you are written in characters that do not give you the
257
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 207
slightest idea what they are about. This means you always
265
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 208
have to prepare your travelling beforehand and ask us for help
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 209
if you are unsure!
252
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 210
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 211
One part of \emph{every} trip preparation, including your
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 212
arrival, should be to carry with you a printed copy of the map
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 213
where the Hanyuan Hotel is located (see Fig.~\ref{hanyuan}).
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 214
When you want to go to the hotel by taxi, you need to show the map to
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 215
the driver, since telling Hanyuan Hotel will most probably not
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 216
be understood and also the driver most likely does not know
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 217
where it is located. Showing the map will also guard against
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 218
the possible situation where a taxi driver cannot actually
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 219
read the address.\footnote{You might sneer at this. But
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 220
remember: the prime age of Chinese taxi drivers appears to be
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 221
50 plus. If you can also remember, between 1966 and 1976
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 222
somebody had the ``great'' idea to be nasty to teachers
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 223
(amonst others). So the education these people were able to
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 224
receive when their were in their teens was rather rudimentary.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 225
Given that the ability of reading Chinese characters takes
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 226
years of arduous studying, it is glaringly obvious that it is
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 227
not their fault.} Take the map always with you: it might be
265
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 228
your life-line for avoiding unpleasant situations. For
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 229
travelling inside Nanjing, taxis can be hailed at the
268
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 230
street curb. You need to pay them in cash. They are always
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 231
metered.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 232
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 233
\item \textbf{Tips in Restaurants, Taxi}\hspace{3mm}One easy
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 234
part of travelling in China are matters to do with tipping:
269
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 235
no tips are expected when paying at a restaurant, for a taxi
268
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 236
journey etc. The good thing about this is you are treated as a
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 237
nice customer, if you are a nice customer (meaning you treat
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 238
staff with respect).
257
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 239
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 240
\item \textbf{Cash / Credit Cards}\hspace{3mm}While foreign
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 241
credit cards are accepted in a number of places, including
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 242
the hotel,\footnote{Visa and Mastercard} these places are
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 243
considered ``upmarked'' in China. So if you insist on being able
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 244
to use your credit card, you will often be paying some form of
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 245
premium. Cash still rules many aspects of Chinese life
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 246
(metro ticket, taxi journey,\ldots{}) where foreign credit cards
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 247
are of no use (China has its own credit card system which is
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 248
accepted more widely, but also not everywhere). Pretty much the
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 249
only places where cash can be obtained with a foreign credit
269
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 250
card are ATMs in Chinese banks. There are several in the
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 251
nearer vicinity of the hotel.
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 252
\end{itemize}
257
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 253
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 254
\begin{figure}[p]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 255
\begin{tabular}{l}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 256
Address of Hanyuan Hotel:\medskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 257
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 258
%å¸æœºå¸ˆå‚…,请将我é€å¾€``{\bf ç«¥å«è·¯20å·ç¿°è‹‘宾馆}'',其ä½ç½®å¦‚地图ä¸çº¢è‰²A点所示。\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 259
%酒店电è¯ï¼š02584393962。谢谢ï¼
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 260
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 261
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 262
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 263
\makebox[0mm]{\includegraphics[scale=0.5]{travel_guide/badu.png}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 264
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 265
\caption{The location of the Hanyuan Hotel. Please print out!
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 266
\label{hanyuan}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 267
\end{figure}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 268
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 269
252
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 270
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 271
\section{Travel from Nanjing Lukou Airport to the Hanyuan Hotel}
252
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 272
257
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 273
There are essentially three options depending on how frugal
267
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 274
or adventurous you want to be to travel from the Nanjing Airport
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 275
to the hotel:
257
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 276
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 277
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 278
\item The first option is to take a taxi for the whole journey
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 279
from the airport to the hotel. Follow the taxi signs at
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 280
the airport and take a yellow taxi. The journey will
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 281
cost you around 130 RMB (\euro{}19, \$21) and takes
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 282
about 45 minutes. Show the driver the map in
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 283
Fig.~\ref{hanyuan}. The taxi needs to be paid in cash.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 284
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 285
\item A bit less expensive is going first by Metro Line S1
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 286
from the airport to Nanjing Nan Railway Station (Nanjing
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 287
South Railway Station). The metro will operate between
265
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 288
6:40 and 22:00. As you can see in the map shown in
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 289
Fig.~\ref{metronanjing}, Nanjing Nan will be the last
268
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 290
stop on Line~S1. At Nanjing Nan Railway Station you need to go
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 291
to the taxi stand, which means leaving the metro via exit
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 292
2B and follow the signs for ``Taxi (Underground)''.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 293
The way is marked yellow in the map below.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 294
This option takes approximately
265
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 295
55 minutes and costs 7 RMB for the metro ticket and
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 296
around 36 RMB for the taxi.
257
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 297
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 298
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 299
\includegraphics[scale=0.4]{travel_guide/ggg.jpg}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 300
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 301
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 302
\item If you already paid the fixed price for the metro, why
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 303
not going the whole way by metro? This is the third
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 304
option. The disadvantage is that you need to change
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 305
at Nanjing Nan Railway Station to Line 3 and at
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 306
Daxinggong to Line 2 for Xiamafang or Muxuyuan, which
265
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 307
are the closest stations to the Hanyuan Hotel
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 308
(see Fig.~\ref{metronanjing}). Both
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 309
stations then need a 15 minutes walk to the hotel.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 310
This is another disadvantage of this option if you have
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 311
a heavy suitcase.
257
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 312
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 313
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 314
\begin{figure}[p]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 315
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 316
\makebox[0mm]{\includegraphics[scale=1.1]{travel_guide/metromapnanjing.png}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 317
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 318
\caption{Metro map of Nanjing. Stations
269
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 319
Xiamafang and Muxuyuan on Line 2 (red line) are
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 320
closest to the hotel.\label{metronanjing}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 321
\end{figure}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 322
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 323
\subsubsection*{Getting a Ticket for the Metro in Nanjing}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 324
268
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 325
Like in all Chinese metro stations, entering the metro station at the
265
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 326
airport means you have to go through a brief security check
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 327
where your luggage will be X-rayed. After the check you will
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 328
see ticket machines
257
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 329
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 330
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 331
\includegraphics[scale=0.27]{travel_guide/20150331_110412.jpg}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 332
\hspace{4mm}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 333
\includegraphics[scale=0.27]{travel_guide/20150331_110548.jpg}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 334
\end{center}
257
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 335
265
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 336
\noindent which can change the language to English (in this
267
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 337
way you can avoid having to talk to a sales person in the ticket
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 338
counter, who might not speak any English). You need to select
268
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 339
the destination station on the touch screen (shown on
267
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 340
the right). Next you need to pay for the ticket with 10 RMB or 5
265
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 341
RMB bank notes, or 1 RMB coins. If you do not have them yet,
269
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 342
you will need to get your ticket from the counter.
267
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 343
After paying, the machine will issue a blue plastic coin which
265
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 344
is your ticket. This coin needs to be swiped when going
267
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 345
through the gates of the metro (shown on the right below).
257
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 346
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 347
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 348
\includegraphics[scale=0.27]{travel_guide/20150331_110738.jpg}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 349
\hspace{4mm}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 350
\includegraphics[scale=0.27]{travel_guide/IMG_7177.jpg}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 351
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 352
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 353
\noindent At the end of your journey you will
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 354
have to return the blue coin at the exit gate. (??)
252
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 355
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 356
\section{Travel from Shanghai Pudong Airport}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 357
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 358
Many of the participants will arrive at Shanghai Pudong
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 359
Airport. From there, in short, you have to get to (1) the Hong
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 360
Qiao railway station and then from there to (2) Nanjing Nan
265
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 361
railway station. From Nanjing Nan it is best to take a taxi,
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 362
but you can also take the metro as explained in the previous
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 363
section. Overall this will take approximately 3h of travelling
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 364
to the hotel.
252
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 365
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 366
\subsection*{From Shanghai Pudong Airport to Hong Qiao Train Station}
166
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 367
252
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 368
For the first leg to Hong Qiao train station there are
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 369
essentially two travel options: one recommended by locals
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 370
and being the more sensible option is to take the airport bus;
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 371
the other is by the World's only commercial Maglev train
265
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 372
including a change to the metro.
252
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 373
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 374
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 375
\item \textbf{Option 1 by Airport bus}:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 376
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 377
At the Pudong Airport follow the signs for Airport Bus, or Airport
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 378
Ring Bus. You have to take Line 1, which operates between 7:00
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 379
and 23:00. The bus stop where you have to wait is
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 380
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 381
\begin{center}
265
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 382
\includegraphics{travel_guide/image005.jpg}
252
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 383
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 384
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 385
The waiting time is around 15 minutes during peak hours, or 30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 386
minutes at other times. The ticket costs 30 RMB (\euro{}4.25,
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 387
\$5) and can be bought on the bus. This however requires cash.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 388
While you wait, be prepared to be harassed by taxi drivers,
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 389
who insist on driving you to Hong Qiao train station. You can
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 390
ignore them: it will cost you more, around 100 RMB; the bus is
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 391
comfortable and air-conditioned, unlike the taxi; and, like
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 392
the taxi driver, the bus driver already aims for maximum
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 393
possible speed given good road conditions.
252
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 394
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 395
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 396
The airport bus takes around 1h and makes only two stops at
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 397
the very end of the journey. Both stops are in near
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 398
proximity. You have to take the \emph{second} stop at Hong Qiao
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 399
Railway Station. You will be able to see the big signs of
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 400
Hong Qiao Railway Station when you approach the station. Do
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 401
not take the exit for Hong Qiao International Airport.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 402
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 403
\item \textbf{Option 2 Maglev train / Metro}:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 404
Of course travelling on the Maglev is pretty cool\ldots{}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 405
reaching speeds of 415 km/h at certain(!) times of the day,
257
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 406
namely 9:02--10:47 and 15:02--16:47. At other times it will
267
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 407
travel at mere speeds of 300 km/h, which you get in China
265
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 408
also with conventional high-speed trains. Anyway, a
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 409
ticket for the Maglev will set you back around 50 RMB (\euro{}7, \$8). The
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 410
ticket can be paid in cash or with credit card.
257
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 411
The service of the Maglev
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 412
starts at 7:02 and finished the day at 21:42.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 413
To take this option
265
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 414
at the airport, you will need to follow the Maglev signs. The
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 415
main problem with
269
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 416
this option, however, is that you can only travel until Longyang
257
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 417
Road Station and then have to
265
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 418
change into the overcrowded and much, much slower metro Line 2.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 419
The change to the
252
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 420
metro is a short walk from the Maglev. You have to first buy a
268
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 421
ticket inside the metro station. The good thing
252
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 422
about this option is that metro travelling in Shanghai is
265
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 423
pretty easy for foreigners as all stations are signed out in
269
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 424
letters. For buying a ticket for the metro, check the section
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 425
about buying a metro ticket in Nanjing (the procedure is
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 426
pretty universal in China).
266
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 427
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 428
Overall the journey time of this option is around 2h. So
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 429
unless you really want to sample the feeling of travelling for
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 430
7 minutes at 415 km/h, we recommend Option 1 by bus.
252
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 431
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 432
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 433
\subsection*{From Hong Qiao Train Station to Nanjing Nan via
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 434
High-Speed Train}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 435
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 436
The airport bus will stop directly in front of the southern
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 437
part of the Hong Qiao train station. As background, train
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 438
stations above the village level in China are organised more
265
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 439
like an airport, than the more sleepy train station you might be
252
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 440
familiar with. Therefore you first have to go through a
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 441
security gate where luggage is checked and you padded by a
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 442
security guard. The security guard might be of either sex and
268
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 443
this is seen as normal by Chinese.
252
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 444
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 445
Next you need to buy a train ticket. There are ticket
268
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 446
counters, see left below, signed out in the main hall. (Unlike
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 447
the metro, ticket machines for trains are of no use for you,
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 448
because you would need a Chinese ID-card in order to buy
269
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 449
anything with them.)
252
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 450
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 451
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 452
\includegraphics[scale=0.8]{travel_guide/image038.jpg}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 453
\includegraphics[scale=0.8]{travel_guide/image040.jpg}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 454
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 455
268
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 456
\noindent You have to queue on the usually longer queue and
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 457
buy a ticket for Nanjing Nan (Nan stands for South station).
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 458
You will need to show your passport in order to buy a ticket.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 459
The ticket will cost around 135 RMB and looks like this:
252
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 460
266
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 461
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 462
\includegraphics[scale=0.3]{travel_guide/ticket.jpg}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 463
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 464
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 465
\noindent The G-Number (G42 above) stands for the train
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 466
number, which identifies the train also on the large displays
268
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 467
at the hall. Below that number is the date and departure time,
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 468
in this case 2015-08-12 and departure time 10:28. To the right
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 469
is the coach number (14) and seat number (09C). Just below
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 470
from that is the sign that the ticket is for second class (-\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 471
-). For the short duration of the trip there is no real need
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 472
to buy a ticket for first class. On the top right-hand corner
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 473
is the platform signed out (10A). If not, you have to look
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 474
at the large display in the hall to get this information.
252
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 475
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 476
Next you have to wait for your train on the main concourse of
268
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 477
the station. Assuming you have some time, rest for a moment
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 478
and take in the atmosphere of a typical Chinese train
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 479
station\ldots{} definitely busy. Once you know the
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 480
platform, go to the gate. Be careful, the gates are nestled
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 481
between shops and can be easily overlooked. For each platform
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 482
there are two gates labelled `A' and `B', respectively. They
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 483
are on opposite sides of the main hall. `A' stands for the
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 484
front of the train and `B' for the rear -- you know which one
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 485
to go to from the coach number on your ticket. When the gates
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 486
are opened for your train you need to show again your passport
266
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 487
verifying that it is you who is travelling on the ticket. The
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 488
journey to Nanjing Nan takes around 1h.
252
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 489
266
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 490
\subsection*{Nanjing Nan Railway Station to the Hanyuan Hotel}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 491
269
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 492
Like in the section for travelling from Nanjing Lukou Airport,
268
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 493
there are two option you can take from Nanjing Nan. The only
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 494
difference is that the train station has a different taxi
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 495
stand, which is signed out at the station. At the taxi stand
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 496
you need to take a yellow taxi that goes to ``Nanjing
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 497
Downtown''. The taxi will cost around 36 RMB and needs to be
269
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 498
paid in cash. Show the driver the map in Fig~\ref{hanyuan}.
166
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 499
179
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 500
%weather, electrical connectors
166
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 501
269
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 502
\chapter{At the Conference}
265
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 503
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 504
266
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 505
\section{Schedule of the Excursion}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 506
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 507
On Wednesday afternoon there will be the traditional ITP
269
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 508
excursion, this time to a Chinese garden in Yangzhou and to the
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 509
Slender West Lake. You might like to note a few points:
\begin{itemize}
\item The conference session will end at 11:30, and you
266
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 510
should finish lunch no later than 12:20 in order to get
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 511
to the hotel lobby.
\item Boarding the shuttle bus is at 12:30 sharp!
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 512
\item The first leg of the bus journey takes roughly 40 minutes
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 513
to Ge Yuan Garden (meaning Bamboo Garden). This is a
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 514
small garden in traditional Chinese style. We will be there
269
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 515
for approximately 1h. You can find a short description at
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 516
\url{https://en.wikipedia.org/wiki/Ge_Yuan_Garden}.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 517
266
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 518
\item After Ge Yuan, we are going to board the shuttle bus again
269
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 519
for the Slender West Lake. We are going to enter the Slender West
266
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 520
Lake area from its North Gate. The walking tour at Slender
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 521
West Lake will be lead by two guides speaking English.
269
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 522
Wiki has some rudimentary information at
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 523
\url{https://en.wikipedia.org/wiki/Slender_West_Lake}.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 524
%\item After the walk, we will board boats which will bring
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 525
% us to the South Gate of the lake.
\item The banquet restaurant (named Lion
266
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 526
Pavilion) is located on the campus
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 527
of Yangzhou University. It will take us 5 minute walk
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 528
from the South Gate to get there.
\item We expect that the shuttle bus brings us back starting
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 529
around 21:30 and we should be back in the hotel by 23:00.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 530
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 531
269
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 532
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 533
\section{While being in Nanjing, Local Attractions}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 534
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 535
%% what is the downtown metro station?
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 536
252
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 537
\newlength{\cw}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 538
\setlength{\cw}{100mm}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 539
\newcolumntype{L}[1]{>{\raggedright\let\newline\\\arraybackslash\hspace{0pt}}m{#1}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 540
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 541
\begin{figure}[p]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 542
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 543
\rotatebox{90}{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 544
\small
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 545
\begin{tabular}[t]{@{}*{2}{c @{\hspace{4mm}}} @{}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 546
\mbox{}\\[-20mm]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 547
\begin{tabular}[t]{@{}|@{\hspace{0.5mm}}L{\cw}@{\hspace{0.5mm}}|}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 548
\multicolumn{1}{c}{\textbf{Monday}}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 549
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 550
9:00 -- 10:00\smallskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 551
Short Intro Session\smallskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 552
M.~Moscato, C.~Munoz, A.~Smith\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 553
Affine Arithmetic and Applications to Real-Number Proving\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 554
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 555
\multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 556
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 557
10:20 -- 11:10\smallskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 558
J.~Hölzl, A.~Lochbihler, D.~Traytel\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 559
A Formalized Hierarchy of Probabilistic System Types (Proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 560
Pearl)\smallskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 561
F.~Immler\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 562
A Verified Enclosure for the Lorenz Attractor (Rough
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 563
Diamond)\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 564
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 565
\multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 566
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 567
11:30 -- 12:30\smallskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 568
A.~Anand, R.~Knepper\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 569
ROSCoq: Robots Powered by Constructive Reals\smallskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 570
H.~Chan, M.~Norrish\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 571
Mechanisation of AKS Algorithm: Part 1 – the Main Theorem\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 572
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 573
\multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}2hs lunch break}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 574
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 575
14:30 -- 15:30\smallskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 576
S.~Schneider, G.~Smolka, S.~Hack\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 577
A First-Order Functional Intermediate Language for Verified
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 578
Compilers\smallskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 579
A.~Fox\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 580
Improved Tool Support for Machine-Code Decompilation in
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 581
HOL4\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 582
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 583
\multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}30 mins coffee break}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 584
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 585
16:00 -- 17:00\smallskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 586
F.~Besson, S.~Blazy, P.~Wilke\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 587
A Concrete Memory Model for CompCert\smallskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 588
T.~Tuerk, M.~Myreen, R.~Kumar\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 589
Pattern Matches in HOL: A New Representation and Improved Code
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 590
Generation\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 591
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 592
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 593
& \begin{tabular}[t]{|@{\hspace{0.5mm}}p{\cw}@{\hspace{0.5mm}}|}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 594
\multicolumn{1}{c}{\textbf{Tuesday}}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 595
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 596
9:00 -- 10:00 (chair: M.~Norrish)\smallskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 597
A.~Charguéraud, F.~Pottier\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 598
Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 599
Implementation\smallskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 600
T.~Nipkow\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 601
Amortized Complexity Verified\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 602
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 603
\multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 604
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 605
10:20 -- 11:10\smallskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 606
S.~Blazy, D.~Demange, D.~Pichardie\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 607
Validating Dominator Trees for a Fast, Verified Dominance
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 608
Test\smallskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 609
A.~Lochbihler, A.~Maximova\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 610
Stream Fusion for Isabelle’s Code Generator (Rough
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 611
Diamond)\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 612
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 613
\multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 614
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 615
11:30 -- 12:30 (chair: X.~Zhang)\smallskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 616
L.~Birkedal\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 617
\textbf{Invited Talk}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 618
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 619
\multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}2hs lunch break}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 620
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 621
14:30 -- 15:30\smallskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 622
M.~Abdulaziz, M.~Norrish, C.~Gretton\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 623
Verified Over-Approximation of the Diameters of Propositionally Factored Transition
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 624
Systems\smallskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 625
T.~Prathamesh\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 626
Formalizing Knot Theory in Isabelle/HOL\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 627
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 628
\multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}30 mins coffee break}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 629
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 630
16:00 -- 17:00\smallskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 631
S.~Schäfer, T.~Tebbi, G.~Smolka\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 632
Autosubst: Reasoning with de Bruijn Terms and Parallel
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 633
Substitutions\smallskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 634
P.~Maksimovic, A.~Schmitt\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 635
HOCore in Coq\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 636
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 637
\multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}short coffee break}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 638
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 639
17:15 -- 18:00\smallskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 640
\textbf{ITP Business Meeting}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 641
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 642
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 643
\end{tabular}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 644
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 645
\end{figure}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 646
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 647
\begin{figure}[p]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 648
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 649
\rotatebox{90}{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 650
\small
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 651
\begin{tabular}[t]{@{} *{2}{c @{\hspace{4mm}}} @{}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 652
\mbox{}\\[-30mm]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 653
\begin{tabular}[t]{|@{\hspace{0.5mm}}L{90mm}@{\hspace{0.5mm}}|}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 654
\multicolumn{1}{c}{\textbf{Wednesday}}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 655
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 656
9:00 -- 10:00\smallskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 657
R.~Spadotti\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 658
A Mechanized Theory of Regular Trees in Dependent Type
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 659
Theory\smallskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 660
G.~Smolka, S.~Schäfer, C.~Doczkal\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 661
Transfinite Constructions in Classical Type Theory\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 662
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 663
\multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}30 mins coffee break}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 664
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 665
10:30 -- 11:30\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 666
M.~Norrish\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 667
\textbf{Invited Talk}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 668
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 669
\multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}1h Lunch break}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 670
\hline
269
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 671
12:30 -- 22:30\smallskip\\
252
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 672
Excursion to Ge Yuan Garden and Slender West Lake\smallskip\\
269
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 673
The bus departs at 12:30 sharp from the hotel.\smallskip\\
252
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 674
Dinner will be at the Lion Pavilion restaurant which is close
269
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 675
to the Slender West Lake.\smallskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 676
We expect to be back at the hotel around 22:30.\\
252
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 677
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 678
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 679
& \begin{tabular}[t]{|@{\hspace{0.5mm}}L{130mm}@{\hspace{0.5mm}}|@{}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 680
\multicolumn{1}{c}{\textbf{Thursday}}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 681
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 682
9:00 -- 10:00\smallskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 683
B.~Fallenstein, R.~Kumar\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 684
Proof-Producing Reflection for HOL, with an Application
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 685
to Model Polymorphism\smallskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 686
O.~KunÄar, A.~Popescu\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 687
A Consistent Foundation for Isabelle/HOL\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 688
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 689
\multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 690
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 691
10:20 -- 11:10\smallskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 692
Z.~Paraskevopoulou \textit{et al}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 693
Foundational Property-Based Testing\smallskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 694
C.~Kaliszyk, J.~Urban, J.~Vyskocil\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 695
Learning To Parse on Aligned Corpora (Rough Diamond)\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 696
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 697
\multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 698
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 699
11:30 -- 12:30\smallskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 700
F.~Sieczkowski, A.~Bizjak, L.~Birkedal\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 701
ModuRes: A Coq Library for Modular Reasoning about Concurrent Higher-Order Imperative Programming
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 702
Languages\smallskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 703
S.~Boulmé, A.~Maréchal\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 704
Refinement to Certify Abstract Interpretations, Illustrated
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 705
on Linearization for Polyhedra\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 706
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 707
\multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}2hs lunch break}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 708
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 709
14:30 -- 15:30\smallskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 710
C.~Sternagel, R.~Thiemann\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 711
Deriving Comparators and Show-Functions in Isabelle/HOL\smallskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 712
R.~Affeldt, J.~Garrigue\\
269
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 713
Formalization of Error-Correcting Codes: from Hamming to Modern Coding
252
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 714
Theory\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 715
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 716
\multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}30 mins coffee break}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 717
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 718
16:00 -- 17:00\smallskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 719
P.~Lammich\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 720
Refinement to Imperative/HOL\smallskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 721
B.~Barras, C.~Tankink, E.~Tassi\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 722
Asynchronous Processing of Coq Documents:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 723
from the Kernel up to the User Interface\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 724
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 725
\multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}short coffee break}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 726
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 727
17:15 -- 17:45\smallskip\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 728
L.~Cruz-Filipe, P.~Schneider-Kamp\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 729
Formalizing Size-Optimal Sorting Networks: Extracting a
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 730
Certified Proof Checker\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 731
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 732
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 733
\end{tabular}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 734
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 735
\end{figure}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 736
165
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 737
\end{document}