booklet.tex
author Christian Urban <christian dot urban at kcl dot ac dot uk>
Fri, 14 Aug 2015 08:47:49 +0800
changeset 267 0254a6cb1182
parent 266 7a052c75818b
child 268 a792b2f23afe
permissions -rw-r--r--
updated
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
165
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     1
\documentclass[11pt]{report}
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
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>
parents: 165
diff changeset
     4
\usepackage{fontspec}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 165
diff changeset
     5
\usepackage[sc]{mathpazo}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 165
diff changeset
     6
\setmainfont[Ligatures=TeX]{Palatino Linotype}
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
     7
\usepackage{fancyvrb}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
     8
\usepackage[table]{xcolor}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
     9
\usepackage{floatpag}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
    10
\floatpagestyle{empty}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
    11
\definecolor{linkcolor}{rgb}{0,0,0.5}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
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>
parents: 166
diff changeset
    13
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
    14
%\usepackage{xeCJK}
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
    15
%\setCJKmainfont[BoldFont=STZhongsong, ItalicFont=STKaiti]{STSong}
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
    16
%\setCJKsansfont[BoldFont=STHeiti]{STXihei}
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
    17
%\setCJKmonofont{STFangsong}
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
    18
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
    19
168
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 166
diff changeset
    20
\def\xyzemail{xingyuanzhang at 126 dot com}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 166
diff changeset
    21
\def\cwemail{chunhanwu at 126 dot com} 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 166
diff changeset
    22
 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 166
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>
parents: 168
diff changeset
    25
\title{\LARGE\bf ITP 2015 Conference Booklet}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 168
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>
parents: 169
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>
parents: 165
diff changeset
    35
In short
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 165
diff changeset
    36
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 165
diff changeset
    37
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 165
diff changeset
    38
\item[(1)] you need to make a bank transfer for the conference 
198
63c7c2c9e14a updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 191
diff changeset
    39
fee in your local currency, and  
166
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 165
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>
parents: 166
diff changeset
    41
  (\xyzemail)
166
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 165
diff changeset
    42
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 165
diff changeset
    43
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 165
diff changeset
    44
\noindent Xingyuan will then confirm that the payment has been
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 165
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>
parents: 168
diff changeset
    46
piao} to reclaim the conference fee, you need to contact 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 168
diff changeset
    47
Xingyuan directly before making any money transfer. 
166
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 165
diff changeset
    48
\medskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 165
diff changeset
    49
 
170
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 169
diff changeset
    50
\noindent The early conference fee is RMB 3300, which is
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 169
diff changeset
    51
approximately \pounds{}350, \$533, or \euro{}488. It must be
198
63c7c2c9e14a updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 191
diff changeset
    52
transferred via bank transfer and must be made in your local 
63c7c2c9e14a updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 191
diff changeset
    53
currency; we cannot accept any other form of payment. The 
63c7c2c9e14a updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 191
diff changeset
    54
tutorials can be registered independently from the conference. 
170
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 169
diff changeset
    55
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 169
diff changeset
    56
The conference fee includes lunches during the conference. It
172
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 170
diff changeset
    57
also covers the excursion, the conference banquet and a
170
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 169
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>
parents: 169
diff changeset
    62
Early conference fee until 31.~July: & RMB 3300\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 169
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>
parents: 169
diff changeset
    65
Additional banquet dinner and excursion: & RMB 530\\
169
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 168
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>
parents: 169
diff changeset
    68
Isabelle tutorial (21 -- 23 August): & RMB 250\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 169
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
51c1e01c586b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 190
diff changeset
    73
\noindent The amount payable needs to be
190
46525a2c7ced updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 180
diff changeset
    74
transferred to the account:
166
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 165
diff changeset
    75
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 165
diff changeset
    76
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 165
diff changeset
    77
\begin{tabular}{ll}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 165
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>
parents: 169
diff changeset
    79
                         &    Sub-branch, Nanjing, China\medskip\\

Account holder's address:& \\
169
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 168
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>
parents: 168
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>
parents: 169
diff changeset
    82
transferral contains your full name as reference (additional
198
63c7c2c9e14a updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 191
diff changeset
    83
information field), and is in your local currency 
63c7c2c9e14a updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 191
diff changeset
    84
(e.g.~\euro, \$, \pounds)!} Otherwise we will have no idea 
63c7c2c9e14a updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 191
diff changeset
    85
where the money came from, and will not be able to receive
63c7c2c9e14a updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 191
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>
parents: 169
diff changeset
    87
covers all bank fees.\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 169
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>
parents: 169
diff changeset
    89
details to Chunhan 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 169
diff changeset
    90
(\cwemail).\bigskip
166
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 165
diff changeset
    91
170
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 169
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>
parents: 169
diff changeset
    93
online travel web-pages, the price there is higher. The
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 169
diff changeset
    94
easiest is to send Chunhan your name, arrival and departure
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 169
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>
parents: 169
diff changeset
    96
hotel, which you might need for your visa application. 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 169
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>
parents: 169
diff changeset
    98
MasterCard.
166
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 165
diff changeset
    99
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 165
diff changeset
   100
\section{Visa}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 165
diff changeset
   101
168
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 166
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>
parents: 175
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>
parents: 166
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>
parents: 166
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>
parents: 166
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>
parents: 169
diff changeset
   107
will need an invitation letter, which Chunhan will send you
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 169
diff changeset
   108
(\cwemail). You need to provide him with your name, title, 
180
dda7cb026a2e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 179
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>
parents: 169
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>
parents: 169
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>
parents: 169
diff changeset
   112
application.

252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   113
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   114
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   115
\chapter{Arrival}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   116
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   117
Welcome in China. You made it to the destination airport.
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   118
Unless your are one of the very few foreigners who can speak
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   119
and read Chinese, potentially the most challenging part of
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   120
your journey is about to begin. Below we explain how to get to
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   121
Hanyuan Hotel in Nanjing from Nanjing Lukou Airport and from
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   122
Shanghai Pudong Airport. If you arrive from somewhere else and
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   123
need help, please let us know.
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   124
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   125
China is generally a safe country for travelling, if the usual
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   126
precautions are taken. We assume you have never been in China 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   127
before, therefore let us still start with some general points.
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   128
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   129
\begin{itemize}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   130
\item \textbf{Weather}\hspace{3mm} 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   131
Unfortunately end of August is the time when it will be especially
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   132
hot in Nanjing (usually above 30$^{\circ}$C). Be prepared with lots of
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   133
light clothes, but do not forget a jumper, or sweater, since many
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   134
places are air-conditioned. It can also rain.
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   135
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   136
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   137
\item \textbf{Bottled Water}\hspace{3mm}
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   138
Whereas in many places it is safe to drink water from taps,
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   139
do not take chances and drink only bottled water! During the
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   140
conference we will provide bottled water. In other places you
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   141
have to buy bottles yourself. Remember, Chinese are famous for
267
0254a6cb1182 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 266
diff changeset
   142
nibbling on a bottle with hot tea the whole day, even in sweltering 
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   143
temperatures. There is a reason for this. 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   144
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   145
\item \textbf{Traffic}\hspace{3mm} 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   146
Do not even think of renting a car in China. Hence, while in
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   147
China, you probably will be mostly going around on foot. Be
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   148
careful though: You might come from a region where traffic rules are
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   149
organised so that pedestrians are mostly
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   150
treated with respect by all other road users, or even have an
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   151
``elevated status'' because they are considered the ``weakest''. 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   152
Traffic in China is, in contrast, organised more, shall we say, 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   153
according to a Darwinian model: Under no circumstance assume a
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   154
car (or even a bicycle or one of the noiseless electric motor bikes) will stop for you. As pedestrian, you
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   155
have to take care of everybody else. Therefore, whenever
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   156
possible cross roads at traffic lights and even if the light
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   157
shows green for you, look out for cars that pay no attention to this
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   158
fact. Also, zebra crossings do \emph{not}, I repeat, \emph{do not} 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   159
have any special meaning in
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   160
China for the road users higher up the traffic ladder
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   161
(i.e.~bicycles and above). 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   162
Even if it sounds too funny, take
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   163
our word and head this advice\ldots{}it might increase your
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   164
life-expectancy. 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   165
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   166
\item \textbf{Free Public Wifi / Mobile Phones}\hspace{3mm}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   167
While free public wifi is nowadays pretty ubiquitous in big
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   168
cities in China (Starbucks, Costas, McDonalds are obvious
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   169
places where to find wifi), you need a working mobile phone in
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   170
order to use it. You will have to register your number when
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   171
you log in, and the wifi operator will then send you a
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   172
password token via SMS. The problem is that chances are great
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   173
your mobile phone will \emph{not} work in China. Therefore do
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   174
not assume you can check information on the Internet while
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   175
travelling. 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   176
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   177
At the hotel there will be wifi (with the super-secure
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   178
password: 123456789). But again, do not assume you can
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   179
download that last episode of the Daily Show: while bandwidth
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   180
will generally be enough for reading email, be prepared for an
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   181
uninterrupted stay in China, free from any disturbance coming
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   182
from online demands.
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   183
   
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   184
\item \textbf{Google etc}\hspace{3mm}There are two Great Walls in
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   185
China: one prevents you from accessing Google, for example. Use
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   186
\url{www.aol.com} or \url{www.bing.com} instead as your preferred
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   187
search engine. Also, if you care about such things, set your 
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   188
status on Facebook to ``unavailable'' for the period of time
267
0254a6cb1182 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 266
diff changeset
   189
you will be in China. Ditto Twitter. 
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   190
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   191
\item \textbf{Map of Hotel / Taxis}\hspace{3mm} While more and 
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   192
more young Chinese are exposed to English, you cannot 
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   193
rely on anyone of the general public speaking more than a few
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   194
words. Rather, you have to always calculate with the very, 
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   195
very likely scenario that nobody speaks any English at all
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   196
and all
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   197
signs round you are written in characters that do not give you the 
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   198
slightest idea what they are about. This means you always
265
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   199
have to prepare your travelling beforehand and ask us for help
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   200
if you are unsure! 
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   201
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   202
One part of \emph{every} trip preparation, including your
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   203
arrival, should be to carry with you a printed copy of the map
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   204
where the Hanyuan Hotel is located (see Fig.~\ref{hanyuan}).
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   205
When you want to go to the hotel by taxi, you need to show the map to
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   206
the driver, since telling Hanyuan Hotel will most probably not
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   207
be understood and also the driver most likely does not know
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   208
where it is located. Showing the map will also guard against
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   209
the possible situation where a taxi driver cannot actually
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   210
read the address.\footnote{You might sneer at this. But
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   211
remember: the prime age of Chinese taxi drivers appears to be
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   212
50 plus. If you can also remember, between 1966 and 1976
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   213
somebody had the ``great'' idea to be nasty to teachers
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   214
(amonst others). So the education these people were able to
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   215
receive when their were in their teens was rather rudimentary.
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   216
Given that the ability of reading Chinese characters takes
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   217
years of arduous studying, it is glaringly obvious that it is
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   218
not their fault.} Take the map always with you: it might be
265
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   219
your life-line for avoiding unpleasant situations. For 
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   220
travelling inside Nanjing, taxis can be hailed at the
265
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   221
street curb.
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   222
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   223
\item \textbf{Cash / Credit Cards}\hspace{3mm}While foreign
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   224
credit cards are accepted in a number of places, including
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   225
the hotel,\footnote{Visa and Mastercard} these places are 
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   226
considered ``upmarked'' in China. So if you insist on being able
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   227
to use your credit card, you will often be paying some form of 
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   228
premium. Cash still rules many aspects of Chinese life
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   229
(metro ticket, taxi journey,\ldots{}) where foreign credit cards 
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   230
are of no use (China has its own credit card system which is
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   231
accepted more widely, but also not everywhere). Pretty much the 
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   232
only places where cash can be obtained with a foreign credit 
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   233
card are ATMs in Chinese banks.\footnote{MORE INFO NEEDED}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   234
\end{itemize}
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   235
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   236
\begin{figure}[p]
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   237
\begin{tabular}{l}
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   238
Address of Hanyuan Hotel:\medskip\\
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   239
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   240
%司机师傅,请将我送往``{\bf 童卫路20号翰苑宾馆}'',其位置如地图中红色A点所示。\\
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   241
%酒店电话:02584393962。谢谢!
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   242
\end{tabular}
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   243
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   244
\begin{center}
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   245
\makebox[0mm]{\includegraphics[scale=0.5]{travel_guide/badu.png}}
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   246
\end{center}
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   247
\caption{The location of the Hanyuan Hotel. Please print out!
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   248
\label{hanyuan}} 
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   249
\end{figure}
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   250
 
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   251
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   252
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   253
\section{Travel from Nanjing Lukou Airport to the Hanyuan Hotel}
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   254
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   255
There are essentially three options depending on how frugal
267
0254a6cb1182 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 266
diff changeset
   256
or adventurous you want to be to travel from the Nanjing Airport 
0254a6cb1182 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 266
diff changeset
   257
to the hotel:
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   258
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   259
\begin{itemize}
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   260
\item The first option is to take a taxi for the whole journey
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   261
      from the airport to the hotel. Follow the taxi signs at
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   262
      the airport and take a yellow taxi. The journey will
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   263
      cost you around 130 RMB (\euro{}19, \$21) and takes
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   264
      about 45 minutes. Show the driver the map in
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   265
      Fig.~\ref{hanyuan}. The taxi needs to be paid in cash.
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   266
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   267
\item A bit less expensive is going first by Metro Line S1
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   268
      from the airport to Nanjing Nan Railway Station (Nanjing
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   269
      South Railway Station). The metro will operate between
265
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   270
      6:40 and 22:00. As you can see in the map shown in
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   271
      Fig.~\ref{metronanjing}, Nanjing Nan will be the last
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   272
      stop on Line~S1. At Nanjing Nan Railway Station you go
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   273
      to the taxi stand, which means following the yellow path
265
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   274
      in the map below. To reach the taxi stand, you need to
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   275
      leave the metro via exit 2B and follow the signs for
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   276
      ``Taxi (Underground)''. This option takes approximately
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   277
      55 minutes and costs 7 RMB for the metro ticket and
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   278
      around 36 RMB for the taxi.
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   279
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   280
      \begin{center}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   281
      \includegraphics[scale=0.4]{travel_guide/ggg.jpg}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   282
      \end{center}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   283
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   284
\item If you already paid the fixed price for the metro, why
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   285
      not going the whole way by metro? This is the third
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   286
      option. The disadvantage is that you need to change
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   287
      at Nanjing Nan Railway Station to Line 3 and at 
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   288
      Daxinggong to Line 2 for Xiamafang or Muxuyuan, which
265
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   289
      are the closest stations to the Hanyuan Hotel 
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   290
      (see Fig.~\ref{metronanjing}). Both
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   291
      stations then need a 15 minutes walk to the hotel.
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   292
      This is another disadvantage of this option if you have 
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   293
      a heavy suitcase.
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   294
\end{itemize}
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   295
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   296
\begin{figure}[p]
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   297
\begin{center}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   298
\makebox[0mm]{\includegraphics[scale=1.1]{travel_guide/metromapnanjing.png}}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   299
\end{center}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   300
\caption{Metro map of Nanjing. Stations
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   301
Xiamafang and Muxuyuan on Line 2 are 
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   302
closest to the hotel.\label{metronanjing}} 
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   303
\end{figure}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   304
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   305
\subsubsection*{Getting a Ticket for the Metro in Nanjing}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   306
265
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   307
Like in all metro stations, entering the metro station at the
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   308
airport means you have to go through a brief security check
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   309
where your luggage will be X-rayed. After the check you will
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   310
see ticket machines
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   311
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   312
\begin{center}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   313
\includegraphics[scale=0.27]{travel_guide/20150331_110412.jpg}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   314
\hspace{4mm}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   315
\includegraphics[scale=0.27]{travel_guide/20150331_110548.jpg}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   316
\end{center}
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   317
265
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   318
\noindent which can change the language to English (in this
267
0254a6cb1182 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 266
diff changeset
   319
way you can avoid having to talk to a sales person in the ticket 
0254a6cb1182 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 266
diff changeset
   320
counter, who might not speak any English). You need to select 
0254a6cb1182 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 266
diff changeset
   321
the destination station in the screen (shown on
0254a6cb1182 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 266
diff changeset
   322
the right). Next you need to pay for the ticket with 10 RMB or 5
265
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   323
RMB bank notes, or 1 RMB coins. If you do not have them yet,
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   324
you will need to go to the counter near the ticket machines.
267
0254a6cb1182 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 266
diff changeset
   325
After paying, the machine will issue a blue plastic coin which
265
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   326
is your ticket. This coin needs to be swiped when going
267
0254a6cb1182 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 266
diff changeset
   327
through the gates of the metro (shown on the right below). 
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   328
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   329
\begin{center}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   330
\includegraphics[scale=0.27]{travel_guide/20150331_110738.jpg}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   331
\hspace{4mm}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   332
\includegraphics[scale=0.27]{travel_guide/IMG_7177.jpg}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   333
\end{center}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   334
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   335
\noindent At the end of your journey you will
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   336
have to return the blue coin at the exit gate. (??)
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   337
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   338
\section{Travel from Shanghai Pudong Airport}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   339
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   340
Many of the participants will arrive at Shanghai Pudong
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   341
Airport. From there, in short, you have to get to (1) the Hong
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   342
Qiao railway station and then from there to (2) Nanjing Nan
265
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   343
railway station. From Nanjing Nan it is best to take a taxi,
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   344
but you can also take the metro as explained in the previous
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   345
section. Overall this will take approximately 3h of travelling
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   346
to the hotel. 
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   347
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   348
\subsection*{From Shanghai Pudong Airport to Hong Qiao Train Station}
166
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 165
diff changeset
   349
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   350
For the first leg to Hong Qiao train station there are
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   351
essentially two travel options: one recommended by locals
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   352
and being the more sensible option is to take the airport bus;
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   353
the other is by the World's only commercial Maglev train 
265
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   354
including a change to the metro. 
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   355
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   356
\begin{itemize}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   357
\item \textbf{Option 1 by Airport bus}: 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   358
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   359
At the Pudong Airport follow the signs for Airport Bus, or Airport
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   360
Ring Bus. You have to take Line 1, which operates between 7:00
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   361
and 23:00. The bus stop where you have to wait is 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   362
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   363
\begin{center}
265
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   364
\includegraphics{travel_guide/image005.jpg}
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   365
\end{center}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   366
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   367
The waiting time is around 15 minutes during peak hours, or 30
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   368
minutes at other times. The ticket costs 30 RMB (\euro{}4.25,
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   369
\$5) and can be bought on the bus. This however requires cash.
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   370
While you wait, be prepared to be harassed by taxi drivers,
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   371
who insist on driving you to Hong Qiao train station. You can
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   372
ignore them: it will cost you more, around 100 RMB; the bus is
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   373
comfortable and air-conditioned, unlike the taxi; and, like
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   374
the taxi driver, the bus driver already aims for maximum
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   375
possible speed given good road conditions. 
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   376
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   377
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   378
The airport bus takes around 1h and makes only two stops at
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   379
the very end of the journey. Both stops are in near
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   380
proximity. You have to take the \emph{second} stop at Hong Qiao
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   381
Railway Station. You will be able to see the big signs of
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   382
Hong Qiao Railway Station when you approach the station. Do 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   383
not take the exit for Hong Qiao International Airport.
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   384
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   385
\item \textbf{Option 2 Maglev train / Metro}: 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   386
Of course travelling on the Maglev is pretty cool\ldots{}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   387
reaching speeds of 415 km/h at certain(!) times of the day,
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   388
namely 9:02--10:47 and 15:02--16:47. At other times it will 
267
0254a6cb1182 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 266
diff changeset
   389
travel at mere speeds of 300 km/h, which you get in China
265
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   390
also with conventional high-speed trains.  Anyway, a
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   391
ticket for the Maglev will set you back around 50 RMB (\euro{}7, \$8). The
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   392
ticket can be paid in cash or with credit card. 
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   393
The service of the Maglev
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   394
starts at 7:02 and finished the day at 21:42.
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   395
To take this option 
265
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   396
at the airport, you will need to follow the Maglev signs. The 
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   397
main problem with
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   398
this option, however, is that you can only go until  Longyang 
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   399
Road Station and then have to
265
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   400
change into the overcrowded and much, much slower metro Line 2. 
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   401
The change to the
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   402
metro is a short walk from the Maglev. You have to first buy a
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   403
ticket at the metro station and then take Line 2. The good thing
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   404
about this option is that metro travelling in Shanghai is
265
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   405
pretty easy for foreigners as all stations are signed out in 
266
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   406
letters. 
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   407
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   408
Overall the journey time of this option is around 2h. So
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   409
unless you really want to sample the feeling of travelling for
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   410
7 minutes at 415 km/h, we recommend Option 1 by bus.
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   411
\end{itemize}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   412
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   413
\subsection*{From Hong Qiao Train Station to Nanjing Nan via
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   414
High-Speed Train}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   415
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   416
The airport bus will stop directly in front of the southern
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   417
part of the Hong Qiao train station. As background, train
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   418
stations above the village level in China are organised more
265
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   419
like an airport, than the more sleepy train station you might be
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   420
familiar with. Therefore you first have to go through a
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   421
security gate where luggage is checked and you padded by a
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   422
security guard. The security guard might be of either sex and
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   423
this is seen as normal by Chinese. The entire check is done
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   424
orderly, but appears to be only a token check and so
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   425
fortunately is very speedy. 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   426
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   427
Next you need to buy a train ticket. There are ticket
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   428
counters, see left below, signed out in the main hall. 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   429
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   430
\begin{center}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   431
\includegraphics[scale=0.8]{travel_guide/image038.jpg}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   432
\includegraphics[scale=0.8]{travel_guide/image040.jpg} 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   433
\end{center}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   434
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   435
\noindent You have to queue on the longer queue and buy a
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   436
ticket for Nanjing Nan (Nan stands for South station). You
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   437
will need to show your passport in order to buy a ticket. The
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   438
ticket will cost around 135 RMB and looks like this:
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   439
266
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   440
\begin{center}
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   441
\includegraphics[scale=0.3]{travel_guide/ticket.jpg}
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   442
\end{center}
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   443
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   444
\noindent The G-Number (G42 above) stands for the train
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   445
number, which identifies the train also on the large displays
267
0254a6cb1182 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 266
diff changeset
   446
at the hall. Below that number is the date and departure time, 2015-08-12
266
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   447
and departure time 10:28. To the right is the coach number
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   448
(14) and seat number (09C). Just below is the sign that the
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   449
ticket above is for second class (-\ -). For the short
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   450
duration of the trip there is no real need to buy a ticket for
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   451
first class. On the top right-hand corner is the platform
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   452
signed out (10A).
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   453
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   454
Next you have to wait for your train on the main concourse of
266
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   455
the station. On the main display, the platform of your train
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   456
will be displayed 30 minutes before departure in case it is
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   457
not on the ticket. Assuming you have some time, rest for a
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   458
moment and take in the atmosphere of a typical Chinese train
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   459
station\ldots Once you know the platform, go to the gate. Be
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   460
careful, the gates are nestled between the shops and might be
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   461
easily overlooked. For each platform there are two gates
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   462
labelled `A' and `B', respectively. `A' stands for the front
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   463
of the train and `B' for the rear -- you know which one to go
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   464
from the coach number on your ticket. When the gates are
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   465
opened for train you need to show again your passport
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   466
verifying that it is you who is travelling on the ticket. The
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   467
journey to Nanjing Nan takes around 1h.
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   468
266
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   469
\subsection*{Nanjing Nan Railway Station to the Hanyuan Hotel}
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   470
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   471
Like in the section for travelling from Nanjing Lukou Airport 
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   472
there are three option you can take. The only difference is 
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   473
that the train station has a different taxi stand, which is 
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   474
signed out at the station. At the taxi stand you need to take
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   475
a yellow taxi that goes to ``Nanjing Downtown''.
166
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 165
diff changeset
   476
179
1d2f20938399 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 178
diff changeset
   477
%weather, electrical connectors
166
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 165
diff changeset
   478
265
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   479
\chapter{Conference Programme}
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   480
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   481
266
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   482
\section{Schedule of the Excursion}
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   483
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   484
On Wednesday afternoon there will be the traditional ITP
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   485
excursion, this time to a Chinese garden in Yangzhou and the
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   486
Slender West Lake. You might like to not a few points:

\begin{itemize}
\item The conference session will end at 11:30, and you 
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   487
  should finish lunch no later than 12:20 in order to get 
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   488
  to the hotel lobby.
\item Boarding the shuttle bus is at 12:30 sharp!
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   489
\item The first leg of the bus journey takes roughly 40 minutes 
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   490
  to Ge Yuan Garden (meaning Bamboo Garden). This is a
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   491
  small garden in traditional Chinese style. We will be there
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   492
  for approximately 1h.
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   493
\item After Ge Yuan, we are going to board the shuttle bus again 
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   494
  for Slender West Lake. We are going to enter the Slender West 
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   495
  Lake area from its North Gate. The walking tour at Slender 
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   496
  West Lake will be lead by two guides speaking English.
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   497
\item After the walk, we will board boats which will bring
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   498
  us to the South Gate of the lake.
\item The banquet restaurant (named Lion 
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   499
  Pavilion) is located on the campus 
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   500
  of Yangzhou University. It  will take us 5 minute walk 
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   501
    from the South Gate to get there.
\item We expect that the shuttle bus brings us back starting 
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   502
  around 21:30 and we should be back in the hotel by 23:00.
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   503
\end{itemize}
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   504
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   505
\newlength{\cw}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   506
\setlength{\cw}{100mm}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   507
\newcolumntype{L}[1]{>{\raggedright\let\newline\\\arraybackslash\hspace{0pt}}m{#1}}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   508
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   509
\begin{figure}[p]
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   510
\begin{center}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   511
\rotatebox{90}{
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   512
\small
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   513
\begin{tabular}[t]{@{}*{2}{c @{\hspace{4mm}}} @{}}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   514
 \mbox{}\\[-20mm]
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   515
 \begin{tabular}[t]{@{}|@{\hspace{0.5mm}}L{\cw}@{\hspace{0.5mm}}|}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   516
  \multicolumn{1}{c}{\textbf{Monday}}\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   517
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   518
  9:00 -- 10:00\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   519
  Short Intro Session\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   520
  M.~Moscato, C.~Munoz, A.~Smith\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   521
  Affine Arithmetic and Applications to Real-Number Proving\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   522
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   523
  \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   524
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   525
  10:20 -- 11:10\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   526
  J.~Hölzl, A.~Lochbihler, D.~Traytel\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   527
  A Formalized Hierarchy of Probabilistic System Types (Proof 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   528
  Pearl)\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   529
  F.~Immler\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   530
  A Verified Enclosure for the Lorenz Attractor (Rough 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   531
  Diamond)\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   532
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   533
  \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   534
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   535
  11:30 -- 12:30\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   536
  A.~Anand, R.~Knepper\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   537
  ROSCoq: Robots Powered by Constructive Reals\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   538
  H.~Chan, M.~Norrish\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   539
  Mechanisation of AKS Algorithm: Part 1 – the Main Theorem\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   540
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   541
  \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}2hs lunch break}\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   542
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   543
  14:30 -- 15:30\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   544
  S.~Schneider, G.~Smolka, S.~Hack\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   545
  A First-Order Functional Intermediate Language for Verified 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   546
  Compilers\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   547
  A.~Fox\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   548
  Improved Tool Support for Machine-Code Decompilation in 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   549
  HOL4\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   550
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   551
  \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}30 mins coffee break}\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   552
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   553
  16:00 -- 17:00\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   554
  F.~Besson, S.~Blazy, P.~Wilke\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   555
  A Concrete Memory Model for CompCert\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   556
  T.~Tuerk, M.~Myreen, R.~Kumar\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   557
  Pattern Matches in HOL: A New Representation and Improved Code 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   558
  Generation\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   559
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   560
  \end{tabular} 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   561
& \begin{tabular}[t]{|@{\hspace{0.5mm}}p{\cw}@{\hspace{0.5mm}}|}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   562
  \multicolumn{1}{c}{\textbf{Tuesday}}\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   563
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   564
  9:00 -- 10:00 (chair: M.~Norrish)\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   565
  A.~Charguéraud, F.~Pottier\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   566
  Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   567
  Implementation\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   568
  T.~Nipkow\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   569
  Amortized Complexity Verified\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   570
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   571
  \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   572
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   573
  10:20 -- 11:10\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   574
  S.~Blazy, D.~Demange, D.~Pichardie\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   575
  Validating Dominator Trees for a Fast, Verified Dominance 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   576
  Test\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   577
  A.~Lochbihler, A.~Maximova\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   578
  Stream Fusion for Isabelle’s Code Generator (Rough 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   579
  Diamond)\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   580
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   581
  \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   582
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   583
  11:30 -- 12:30 (chair: X.~Zhang)\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   584
  L.~Birkedal\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   585
  \textbf{Invited Talk}\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   586
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   587
  \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}2hs lunch break}\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   588
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   589
  14:30 -- 15:30\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   590
  M.~Abdulaziz, M.~Norrish, C.~Gretton\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   591
  Verified Over-Approximation of the Diameters of Propositionally Factored Transition 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   592
  Systems\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   593
  T.~Prathamesh\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   594
  Formalizing Knot Theory in Isabelle/HOL\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   595
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   596
  \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}30 mins coffee break}\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   597
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   598
  16:00 -- 17:00\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   599
  S.~Schäfer, T.~Tebbi, G.~Smolka\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   600
  Autosubst: Reasoning with de Bruijn Terms and Parallel 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   601
  Substitutions\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   602
  P.~Maksimovic, A.~Schmitt\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   603
  HOCore in Coq\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   604
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   605
  \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}short coffee break}\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   606
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   607
  17:15 -- 18:00\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   608
  \textbf{ITP Business Meeting}\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   609
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   610
  \end{tabular}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   611
\end{tabular}}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   612
\end{center}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   613
\end{figure}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   614
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   615
\begin{figure}[p]
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   616
\begin{center}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   617
\rotatebox{90}{
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   618
\small
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   619
\begin{tabular}[t]{@{} *{2}{c @{\hspace{4mm}}} @{}}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   620
   \mbox{}\\[-30mm]
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   621
   \begin{tabular}[t]{|@{\hspace{0.5mm}}L{90mm}@{\hspace{0.5mm}}|}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   622
      \multicolumn{1}{c}{\textbf{Wednesday}}\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   623
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   624
   9:00 -- 10:00\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   625
   R.~Spadotti\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   626
   A Mechanized Theory of Regular Trees in Dependent Type 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   627
   Theory\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   628
   G.~Smolka, S.~Schäfer, C.~Doczkal\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   629
   Transfinite Constructions in Classical Type Theory\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   630
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   631
   \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}30 mins coffee break}\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   632
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   633
   10:30 -- 11:30\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   634
   M.~Norrish\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   635
   \textbf{Invited Talk}\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   636
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   637
   \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}1h Lunch break}\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   638
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   639
   12:30 -- 21:30\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   640
   Excursion to Ge Yuan Garden and Slender West Lake\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   641
   Bus departs at 12:30 sharp from the hotel\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   642
   Dinner will be at the Lion Pavilion restaurant which is close
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   643
   to the Slender West Lake\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   644
   We expect to be back at the hotel around 22:30\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   645
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   646
   \end{tabular}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   647
 & \begin{tabular}[t]{|@{\hspace{0.5mm}}L{130mm}@{\hspace{0.5mm}}|@{}}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   648
   \multicolumn{1}{c}{\textbf{Thursday}}\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   649
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   650
   9:00 -- 10:00\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   651
   B.~Fallenstein, R.~Kumar\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   652
   Proof-Producing Reflection for HOL, with an Application 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   653
   to Model Polymorphism\smallskip\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   654
   O.~Kunčar, A.~Popescu\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   655
   A Consistent Foundation for Isabelle/HOL\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   656
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   657
   \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   658
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   659
   10:20 -- 11:10\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   660
   Z.~Paraskevopoulou \textit{et al}\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   661
   Foundational Property-Based Testing\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   662
   C.~Kaliszyk, J.~Urban, J.~Vyskocil\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   663
   Learning To Parse on Aligned Corpora (Rough Diamond)\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   664
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   665
   \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   666
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   667
   11:30 -- 12:30\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   668
   F.~Sieczkowski, A.~Bizjak, L.~Birkedal\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   669
   ModuRes: A Coq Library for Modular Reasoning about Concurrent Higher-Order Imperative Programming 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   670
   Languages\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   671
   S.~Boulmé, A.~Maréchal\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   672
   Refinement to Certify Abstract Interpretations, Illustrated 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   673
   on Linearization for Polyhedra\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   674
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   675
   \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}2hs lunch break}\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   676
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   677
   14:30 -- 15:30\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   678
   C.~Sternagel, R.~Thiemann\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   679
   Deriving Comparators and Show-Functions in Isabelle/HOL\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   680
   R.~Affeldt, J.~Garrigue\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   681
   Formalization of Error-correcting Codes: from Hamming to Modern Coding 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   682
   Theory\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   683
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   684
   \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}30 mins coffee break}\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   685
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   686
   16:00 -- 17:00\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   687
   P.~Lammich\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   688
   Refinement to Imperative/HOL\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   689
   B.~Barras, C.~Tankink, E.~Tassi\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   690
   Asynchronous Processing of Coq Documents: 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   691
   from the Kernel up to the User Interface\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   692
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   693
   \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}short coffee break}\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   694
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   695
   17:15 -- 17:45\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   696
   L.~Cruz-Filipe, P.~Schneider-Kamp\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   697
   Formalizing Size-Optimal Sorting Networks: Extracting a 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   698
   Certified Proof Checker\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   699
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   700
   \end{tabular} 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   701
\end{tabular}}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   702
\end{center}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   703
\end{figure}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   704
165
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   705
\end{document}