booklet.tex
author Christian Urban <christian dot urban at kcl dot ac dot uk>
Mon, 17 Aug 2015 10:00:26 +0800
changeset 278 b3176148b835
parent 277 69ed50eeeb3d
child 279 d1ce0705a775
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
271
024686c71dda updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
    14
\usepackage{xeCJK}
257
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  
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
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
269
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   123
need help, please let us know. If you need help while 
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   124
travelling, the local organisers can be reached on their 
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   125
mobile:
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   126
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   127
\begin{center}
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   128
\begin{tabular}{ll}
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   129
Xingyuan: & (+86)\hspace{2mm}13814081536\\
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   130
Chunhan:  & (+86)\hspace{2mm}15312993807\\
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   131
\end{tabular}
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   132
\end{center}
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   133
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   134
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
   135
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
   136
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
   137
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   138
\begin{itemize}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   139
\item \textbf{Weather}\hspace{3mm} 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   140
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
   141
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
   142
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
   143
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
   144
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   145
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   146
\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
   147
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
   148
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
   149
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
   150
have to buy bottles yourself. Remember, Chinese are famous for
269
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   151
nibbling on a bottle of 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
   152
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
   153
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   154
\item \textbf{Traffic}\hspace{3mm} 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   155
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
   156
China, you probably will be mostly going around on foot. Be
276
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   157
careful though: You might come from a region where traffic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   158
rules are organised so that pedestrians are mostly treated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   159
with respect by all other road users, or even have an
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   160
``elevated status'' because they are considered the
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   161
``weakest''. Traffic in China is, in contrast, organised more,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   162
shall we say, according to a Darwinian model: Under no
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   163
circumstance assume a car (or even a bicycle or one of the
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   164
many noiseless electric motor bikes) will stop for you. As
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   165
pedestrian, you have to take care of everybody else.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   166
Therefore, whenever possible cross roads at traffic lights and
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   167
even if the light shows green for you, look out for cars that
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   168
pay no attention to this fact. Also, zebra crossings do
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   169
\emph{not}, I repeat, \emph{do not} have any special meaning
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   170
in China for the road users higher up the traffic ladder
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   171
(i.e.~bicycles and above). Even if it sounds too funny, take
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   172
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
   173
life-expectancy. 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   174
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   175
\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
   176
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
   177
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
   178
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
   179
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
   180
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
   181
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
   182
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
   183
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
   184
travelling. 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   185
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   186
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
   187
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
   188
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
   189
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
   190
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
   191
from online demands.
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   192
   
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   193
\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
   194
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
   195
\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
   196
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
   197
status on Facebook to ``unavailable'' for the period of time
272
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   198
you will be in China. Ditto Twitter. Skype and Facetime, in 
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   199
contrast, work fine.
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   200
276
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   201
\item \textbf{Map of Hotel / Taxis}\hspace{3mm} 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   202
While more and more young Chinese are exposed to English, you
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   203
cannot rely on anyone of the general public speaking more than
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   204
a few words. Rather, you have to always calculate with the
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   205
very, very likely scenario that nobody speaks any English at
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   206
all and all signs around you are written in characters that do
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   207
not give you the slightest idea what they are about. This
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   208
means you always have to prepare your travelling beforehand
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   209
and ask us for help if you are unsure! 
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   210
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   211
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
   212
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
   213
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
   214
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
   215
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
   216
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
   217
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
   218
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
   219
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
   220
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
   221
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
   222
somebody had the ``great'' idea to be nasty to teachers
270
86c5aa644505 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   223
(amongst others). So the education these people were able to
86c5aa644505 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 269
diff changeset
   224
receive when they were in their teens was rather rudimentary.
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   225
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
   226
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
   227
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
   228
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
   229
travelling inside Nanjing, taxis can be hailed at the
268
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   230
street curb. You need to pay them in cash. They are always
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   231
metered.
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   232
276
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   233
%There is a slight chance you will come across one of the all 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   234
%electric taxi, which are slightly more expensive, than ``normal''
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   235
%taxis. You can recognise them as they are the only taxis built
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   236
%by the maker BYD and look more like a compact SUV, rather than
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   237
%the ``normal'' sedan-style taxi. I have not driven yet in one,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   238
%but have seen them in the Xinjiekou shopping area. If you do not
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   239
%want to pay the additional price tag, you are assumed to just
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   240
%wave them away and wait for the next taxi.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   241
268
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   242
\item \textbf{Tips in Restaurants, Taxi}\hspace{3mm}One easy
271
024686c71dda updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   243
aspect of travelling in China are matters to do with tipping:
269
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   244
no tips are expected when paying at a restaurant, for a taxi 
268
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   245
journey etc. The good thing about this is you are treated as a 
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   246
nice customer, if you are a nice customer (meaning you treat 
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   247
staff with respect).
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   248
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   249
\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
   250
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
   251
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
   252
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
   253
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
   254
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
   255
(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
   256
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
   257
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
   258
only places where cash can be obtained with a foreign credit 
271
024686c71dda updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   259
card are ATMs in Chinese banks. There are several not far
024686c71dda updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   260
from the hotel.
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   261
\end{itemize}
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   262
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   263
\begin{figure}[p]
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   264
\begin{tabular}{l}
272
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   265
For the driver:\medskip\\
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   266
271
024686c71dda updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   267
司机师傅,请将我送往``{\bf 童卫路20号翰苑宾馆}'',其位置如地图中红色A点所示。\\
024686c71dda updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   268
酒店电话:02584393962。谢谢!
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   269
\end{tabular}
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   270
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   271
\begin{center}
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   272
\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
   273
\end{center}
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   274
\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
   275
\label{hanyuan}} 
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   276
\end{figure}
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   277
 
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   278
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   279
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   280
\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
   281
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   282
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
   283
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
   284
to the hotel:
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   285
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   286
\begin{itemize}
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   287
\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
   288
      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
   289
      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
   290
      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
   291
      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
   292
      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
   293
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   294
\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
   295
      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
   296
      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
   297
      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
   298
      Fig.~\ref{metronanjing}, Nanjing Nan will be the last
268
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   299
      stop on Line~S1. At Nanjing Nan Railway Station you need to go
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   300
      to the taxi stand, which means leaving the metro via exit 
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   301
      2B and follow the signs for ``Taxi (Underground)''.
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   302
      The way is marked yellow in the map below. 
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   303
      This option takes approximately
265
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   304
      55 minutes and costs 7 RMB for the metro ticket and
276
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   305
      around 36 RMB for the taxi.\\[-10mm]\mbox{}
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   306
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   307
      \begin{center}
276
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   308
      \includegraphics[scale=0.19]{travel_guide/ggg.jpg}
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   309
      \end{center}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   310
271
024686c71dda updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   311
\item If you already prepared to pay 7 RMB for the metro, why
276
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   312
      not adding 2 more and going the whole way by metro? 
271
024686c71dda updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   313
      This is the third
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   314
      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
   315
      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
   316
      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
   317
      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
   318
      (see Fig.~\ref{metronanjing}). Both
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   319
      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
   320
      This is another disadvantage of this option if you have 
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   321
      a heavy suitcase. See the map shown in Fig.~\ref{hotelmap}
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   322
      for directions.
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   323
 \end{itemize}
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   324
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   325
\begin{figure}[p]
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   326
\begin{center}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   327
\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
   328
\end{center}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   329
\caption{Metro map of Nanjing. Stations
269
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   330
Xiamafang and Muxuyuan on Line 2 (red line) are 
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   331
closest to the hotel.\label{metronanjing}} 
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   332
\end{figure}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   333
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   334
\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
   335
272
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   336
Like most Chinese metro stations, entering the metro station at the
265
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   337
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
   338
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
   339
see ticket machines
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   340
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   341
\begin{center}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   342
\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
   343
\hspace{4mm}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   344
\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
   345
\end{center}
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   346
265
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   347
\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
   348
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
   349
counter, who might not speak any English). You need to select 
268
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   350
the destination station on the touch screen (shown on
267
0254a6cb1182 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 266
diff changeset
   351
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
   352
RMB bank notes, or 1 RMB coins. If you do not have them yet,
269
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   353
you will need to get your ticket from the counter.
271
024686c71dda updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   354
After paying, the machine will issue a blue plastic chip which
272
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   355
is your ticket. This chip needs to be swiped when going
267
0254a6cb1182 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 266
diff changeset
   356
through the gates of the metro (shown on the right below). 
271
024686c71dda updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   357
At the end of your journey you will have to return the blue 
024686c71dda updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   358
chip at the exit gate.
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   359
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   360
\begin{center}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   361
\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
   362
\hspace{4mm}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   363
\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
   364
\end{center}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   365
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   366
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   367
\section{Travel from Shanghai Pudong Airport}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   368
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   369
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
   370
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
   371
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
   372
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
   373
but you can also take the metro as explained in the previous
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   374
section. Overall this will take approximately 4h of travelling
265
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   375
to the hotel. 
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   376
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   377
\subsection*{From Shanghai Pudong Airport to Hong Qiao Railway Station}
166
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 165
diff changeset
   378
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   379
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
   380
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
   381
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
   382
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
   383
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
   384
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   385
\begin{itemize}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   386
\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
   387
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   388
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
   389
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
   390
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
   391
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   392
\begin{center}
272
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   393
\includegraphics[scale=0.9]{travel_guide/image005.jpg}
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   394
\end{center}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   395
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   396
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
   397
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
   398
\$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
   399
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
   400
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
   401
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
   402
comfortable and air-conditioned, unlike the taxi; and, like
271
024686c71dda updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   403
the taxi driver, the bus driver appears to aim for maximum
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   404
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
   405
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   406
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   407
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
   408
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
   409
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
   410
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
   411
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
   412
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
   413
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   414
\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
   415
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
   416
reaching speeds of 415 km/h at certain(!) times of the day,
276
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   417
namely 9:02--10:47 and 15:02--16:47. At other times it will
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   418
travel at mere speeds of 300 km/h, which you get in China also
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   419
with conventional high-speed trains. Anyway, a ticket for the
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   420
Maglev will set you back around 50 RMB (\euro{}7, \$8). The
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   421
ticket can be paid in cash or by credit card. The service of
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   422
the Maglev starts at 7:02 and finished the day at 21:42. To
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   423
take this option at the airport, you will need to follow the
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   424
Maglev signs. The main problem with this option, however, is
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   425
that you can only travel until Longyang Road Station and then
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   426
have to change into the overcrowded and much, much slower
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   427
metro Line 2. The change to the metro is a short walk from the
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   428
Maglev. You have to first buy a ticket inside the metro
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   429
station. The good thing about this option is that metro
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   430
travelling in Shanghai is pretty easy for foreigners as all
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   431
stations are signed out in letters. For buying a ticket for
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   432
the metro, check the section about buying a metro ticket in
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   433
Nanjing (the procedure is pretty universal in China; the only
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   434
exception is that in Shanghai the metro ticket is a paper
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   435
ticket, while in Nanjing it is a blue plastic chip).
266
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   436
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   437
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
   438
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
   439
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
   440
\end{itemize}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   441
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   442
\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
   443
High-Speed Train}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   444
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   445
The airport bus will stop directly in front of the southern
272
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   446
part of the Hong Qiao Railway Station. As background, train
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   447
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
   448
like an airport, than the more sleepy train station you might be
272
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   449
familiar with. Therefore, you first have to go through a
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   450
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
   451
security guard. The security guard might be of either sex and
268
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   452
this is seen as normal by Chinese. 
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 need to buy a train ticket. There are ticket
268
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   455
counters, see left below, signed out in the main hall. (Unlike
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   456
the metro, ticket machines for trains are of no use for you,
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   457
because you would need a Chinese ID-card in order to buy
269
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   458
anything with them.)
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   459
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   460
\begin{center}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   461
\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
   462
\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
   463
\end{center}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   464
268
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   465
\noindent You have to queue on the usually longer queue and
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   466
buy a ticket for Nanjing Nan (Nan stands for South station).
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   467
You will need to show your passport in order to buy a ticket.
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   468
The ticket will cost around 135 RMB and looks like this:
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   469
266
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   470
\begin{center}
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   471
\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
   472
\end{center}
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   473
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   474
\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
   475
number, which identifies the train also on the large displays
268
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   476
at the hall. Below that number is the date and departure time,
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   477
in this case 2015-08-12 and departure time 10:28. To the right
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   478
is the coach number (14) and seat number (09C). Just below
271
024686c71dda updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   479
from that is the sign that the ticket is for second class (二). 
024686c71dda updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   480
For the short duration of the trip there is no real need
268
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   481
to buy a ticket for first class. On the top right-hand corner
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   482
is the platform signed out (10A). If not, you have to look
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   483
at the large display in the hall to get this information.
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   484
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   485
Next you have to wait for your train on the main concourse of
268
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   486
the station. Assuming you have some time, rest for a moment
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   487
and take in the atmosphere of a typical Chinese train
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   488
station\ldots{} definitely busy. Once you know the
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   489
platform, go to the gate. Be careful, the gates are nestled
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   490
between shops and can be easily overlooked. For each platform
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   491
there are two gates labelled `A' and `B', respectively. They
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   492
are on opposite sides of the main hall. `A' stands for the
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   493
front of the train and `B' for the rear -- you know which one
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   494
to go to from the coach number on your ticket. When the gates
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   495
are opened for your train you need to show again your passport
266
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   496
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
   497
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
   498
266
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   499
\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
   500
269
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   501
Like in the section for travelling from Nanjing Lukou Airport,
268
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   502
there are two option you can take from Nanjing Nan. The only
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   503
difference is that the train station has a different taxi
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   504
stand, which is signed out at the station. At the taxi stand
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   505
you need to take a yellow taxi that goes to ``Nanjing
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   506
Downtown''. The taxi will cost around 36 RMB and needs to be
269
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   507
paid in cash. Show the driver the map in Fig~\ref{hanyuan}.
166
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 165
diff changeset
   508
179
1d2f20938399 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 178
diff changeset
   509
%weather, electrical connectors
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   510
%% when does the welcome reception start?
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   511
%% breakfast needs more coffee
166
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 165
diff changeset
   512
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   513
\chapter{Conference}
265
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   514
272
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   515
The Isabelle tutorial will take place from Friday (21st) to
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   516
Sunday (23rd) in a conference room on the 4th floor of Hanyuan
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   517
Hotel. There will be a reception desk of ITP from Thursday
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   518
until Sunday on the 1st floor close to the hotel check in.
277
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   519
The welcome reception is on Sunday (23th) at ??? and close
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   520
to the hotel reception. The ITP conference will take place on the 6th
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   521
floor and starting from Monday the reception desk will be just
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   522
outside the conference hall. On Wednesday (26th) afternoon
276
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   523
we will leave for ITP-excursion to Yangzhou and the Slender
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   524
West Lake (see Sect.~\ref{excursion}). The Coq tutorial will
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   525
take place from Thursday (27th) until Saturday (29th) on the
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   526
4th floor. The programme of the talks is at the end of this
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   527
booklet.
271
024686c71dda updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   528
272
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   529
Breakfast and lunches are served on 1st floor next to hotel
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   530
registration desk. The breakfast buffet is open from 7:00
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   531
until 9:00. When you check into the hotel, you will receive a
277
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   532
green paper ticket for each day, which you have to show before
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   533
going to breakfast. Hanyuan Hotel also includes a very good
276
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   534
restaurant on the 2nd floor, but unfortunately it is a bit 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   535
on the pricier side for China.
265
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   536
272
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   537
\begin{itemize}
276
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   538
\item\textbf{Near the Hotel}\hspace{3mm}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   539
The Hanyuan hotel is located at the intersection of a big road
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   540
(Houbiaoying Road 后标营路) and a smaller road (TongWei Road 童卫路).
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   541
If you need a taxi to go to Downtown Nanjing, for example, it
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   542
is probably the easiest to hail down a taxi at the big street.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   543
An ATM machine is situated a few minutes down the smaller
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   544
TongWei Road. If you want to take a walk in the evening,
277
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   545
Xingyuan suggests a stroll through the Purple Mountain Area on
276
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   546
the top-right in the map in Fig.~\ref{hotelmap}. This area is
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   547
approximately a 15 minutes walk away from the hotel and
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 275
diff changeset
   548
contains for example the Sun Yat Sen memorial and the Linggu
277
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   549
pagoda (below right).
272
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   550
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   551
\begin{center}
277
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   552
\includegraphics[scale=0.40]{travel_guide/map1a.jpg}
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   553
\hspace{5mm}
277
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   554
\includegraphics[scale=0.38]{travel_guide/linggusu.jpg}
272
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   555
\end{center}
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   556
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   557
\item\textbf{Metro Stations Near the Hotel}\hspace{3mm}
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   558
There are two metro stations near the hotel (Muxuyan and
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   559
Xiamafang stations), which are pretty much the same distance
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   560
from the hotel (see map in Fig~\ref{hotelmap}). Muxuyuan is
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   561
easier to reach: just down TongWei Road and then turn left
277
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   562
down the hill of NingHang Road (宁杭公路). The entrance of the
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   563
metro is on the left-hand side. However it is not the most
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   564
scenic route. More scenic is the walk to Xiamafang Metro
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   565
Station through the campus of the Nanjing Agriculture
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   566
University. Unfortunately the way is not so straightforward.
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   567
If you are unfamiliar with the way, we suggest you walk to
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   568
Muxuyuan station; once you followed some locals and know the
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   569
way, go to Xiamafang Station.
272
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   570
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   571
\begin{figure}[p]
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   572
\includegraphics[scale=0.45]{travel_guide/map2.jpg}
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   573
\caption{Shops and restaurants in the vicinity of the hotel.
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   574
A relatively large shopping area including a large supermarket
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   575
(indicated with a red star)
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   576
is near the Xiamafang metro station.\label{hotelmap}}
272
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   577
\end{figure}
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   578
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   579
\item\textbf{Shops and Restaurants Near the Hotel}\hspace{3mm}
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   580
There is a very nice shopping area close to Xiamafang Metro 
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   581
Station. There is a wide selection of restaurants in this
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   582
area including Xingyuan's favourite restaurant for having
277
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   583
lunch on workdays. It is called ?? and situated behind the 
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   584
KFC.
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   585
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   586
\begin{center}
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   587
\includegraphics[scale=0.05]{travel_guide/rest.jpg}
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   588
\end{center}
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   589
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   590
\noindent This area also contains a ``Mickey Mouse bakery'',
277
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   591
which stocks pastries similar to the ones you might find in a 
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   592
Western bakery (just in case you get bored of the baozi
277
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   593
at breakfast in the hotel). There is also pizza place in 
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   594
case you need  must eat something different than Chinese. 
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   595
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   596
There is also a smaller shopping area in the ``middle'' of 
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   597
Tongwei road including some native restaurants, and also some
277
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   598
restaurants on the opposite side of Houbiao\-ying Road. A smaller
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   599
supermarket is at the end of Tongwei Road and a bigger one
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   600
in the Xiamafang area.
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   601
\end{itemize}
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   602
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   603
\section{Further Afield}
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   604
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   605
If you take the metro, you are very quickly in the downtown
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   606
area of Nanjing (see metro map in Fig.~\ref{metronanjing}). 
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   607
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   608
\begin{itemize}
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   609
\item\textbf{Shopping}\hspace{3mm}
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   610
The most serious shopping malls in Nanjing can be found in the
277
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   611
area around Xinjiekou and Daxinggong metro stations (on
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   612
Line~2). Be aware that especially in multi-brand shopping
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   613
malls the shopping goes like this: (1) You find something you
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   614
like. (2) You agree the prize with the shop-assistant. (3) You
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   615
get a piece of paper, which you need to take to a cashier
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   616
nearby. (4) You pay there, get another piece of paper, which
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   617
you take back to the store, where you (5) receive your goods.
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   618
Another ``quirk'' of shopping in China is that when the sale says,
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   619
for example, ``80\% off'', it is actually 20\% off, meaning
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   620
you pay only 80\% of the original price.
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   621
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   622
\item\textbf{Restaurants}\hspace{3mm}The most famous area
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   623
for restaurants in Nanjing is near the Confucius Temple, which
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   624
is near the Fuzimiao Metro Station on Line~3. There you
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   625
can find traditional-style houses and enjoy indigenous foods. 
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   626
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   627
\item\textbf{Sight-Seeing}\hspace{3mm}Nanjing, being a former 
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   628
capital, possessed one of the most impressive city walls. 
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   629
Today you can see remainders at the North Gate near 
277
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   630
Zhonghuamen Metro Station on Line~1. From the station follow
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   631
the red line in the map below.
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   632
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   633
\begin{center}
278
b3176148b835 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 277
diff changeset
   634
\includegraphics[scale=0.4]{travel_guide/map3.jpg}
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   635
\hspace{5mm}
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   636
\includegraphics[scale=0.3]{travel_guide/gate.jpg}
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   637
\end{center}
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   638
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   639
277
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   640
\noindent There is also another substantial section of the
278
b3176148b835 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 277
diff changeset
   641
remaining city wall visible in an area very close to the hotel
b3176148b835 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 277
diff changeset
   642
(you can see it from the hotel if you have a room sufficiently
b3176148b835 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 277
diff changeset
   643
high up): Walk the Houbiaoying Road towards the city centre;
b3176148b835 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 277
diff changeset
   644
once you traversed the river, bear right. You will see a tall
b3176148b835 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 277
diff changeset
   645
wall build of grey stones.
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   646
278
b3176148b835 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 277
diff changeset
   647
\begin{center}
b3176148b835 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 277
diff changeset
   648
\includegraphics[scale=0.4]{travel_guide/map5.jpg}
b3176148b835 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 277
diff changeset
   649
\end{center}
b3176148b835 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 277
diff changeset
   650
b3176148b835 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 277
diff changeset
   651
Another scenic spot is the Xuanwu Lake, which is dotted with
277
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   652
several beautiful small islands and a good place to have a
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   653
walk. You can reach the lake by going to Xuanwumen Metro
278
b3176148b835 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 277
diff changeset
   654
Station at Line~1. Xingyuan suggests the walk indicated red
b3176148b835 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 277
diff changeset
   655
below where you leave from Jimingsi Station on Line~3.
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   656
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   657
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   658
\begin{center}
278
b3176148b835 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 277
diff changeset
   659
\includegraphics[scale=0.3]{travel_guide/map4.jpg}
b3176148b835 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 277
diff changeset
   660
\hspace{5mm}
b3176148b835 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 277
diff changeset
   661
\includegraphics[scale=1.0]{travel_guide/xianwulake.jpg}
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   662
\end{center}
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   663
275
f12df1a3ab0c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 274
diff changeset
   664
\noindent The ultimate bird's-eye view of Nanjing you can have
278
b3176148b835 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 277
diff changeset
   665
from the Zifeng Tower. For this you have to go to Guluo
277
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   666
Metro Station on Line~1. According to Wiki, the Zifeng
278
b3176148b835 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 277
diff changeset
   667
Tower is the 11th tallest building in the World (to
277
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   668
compare, the Shard in London is ranked 92nd and the Sears
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   669
Tower in Chicago is 12th).
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   670
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   671
\end{itemize}
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   672
272
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   673
\section{Schedule of the Excursion\label{excursion}}
266
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   674
277
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   675
On Wednesday afternoon there will be the traditional
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   676
ITP-excursion, this time to a Chinese garden in Yangzhou and
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   677
to the Slender West Lake. You might like to note a few points:

\begin{itemize}
\item The conference session on Wednesday will end at 11:30,
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   678
      and you should finish lunch no later than 12:20 in order
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   679
      to get to the hotel lobby.
\item Boarding the shuttle bus is at 12:30 sharp!
266
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   680
\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
   681
  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
   682
  small garden in traditional Chinese style. We will be there
269
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   683
  for approximately 1h. You can find a short description at
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   684
  \url{https://en.wikipedia.org/wiki/Ge_Yuan_Garden}. 
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   685
  
266
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   686
\item After Ge Yuan, we are going to board the shuttle bus again 
269
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   687
  for the Slender West Lake. We are going to enter the Slender West 
266
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   688
  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
   689
  West Lake will be lead by two guides speaking English.
269
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   690
  Wiki has some rudimentary information at
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   691
  \url{https://en.wikipedia.org/wiki/Slender_West_Lake}.
273
0500c07aed6e updated statistics
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   692
\item After the walk, we will board boats which will bring
0500c07aed6e updated statistics
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   693
  us to the South Gate of the lake.
\item The banquet restaurant (named Lion 
266
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   694
  Pavilion) is located on the campus 
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   695
  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
   696
    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
   697
  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
   698
\end{itemize}
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   699
269
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   700
277
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   701
\mbox{}\\[40mm]
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   702
\noindent The organising team wishes you a pleasant stay in 
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   703
Nanjing! If you need any help, please contact us.
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   704
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   705
\begin{center}
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   706
\begin{tabular}{ccc}
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   707
\includegraphics[scale=0.1]{pics/chunhan.jpg} &
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   708
\includegraphics[scale=0.1]{pics/xingyuan.jpg} &
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   709
\includegraphics[scale=0.555]{pics/christian.jpg}\\
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   710
Chunhan Wu & Xingyuan Zhang & Christian Urban
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   711
\end{tabular}
69ed50eeeb3d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 276
diff changeset
   712
\end{center}
269
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   713
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   714
\newlength{\cw}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   715
\setlength{\cw}{100mm}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   716
\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
   717
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   718
\begin{figure}[p]
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   719
\begin{center}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   720
\rotatebox{90}{
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   721
\small
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   722
\begin{tabular}[t]{@{}*{2}{c @{\hspace{4mm}}} @{}}
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   723
 \mbox{}\\[-15mm]
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   724
 \begin{tabular}[t]{@{}|@{\hspace{0.5mm}}L{\cw}@{\hspace{0.5mm}}|}
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   725
  \multicolumn{1}{c}{\textbf{Monday (6th Floor)\smallskip}}\\
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   726
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   727
  9:00 -- 10:00\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   728
  Short Intro Session\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   729
  M.~Moscato, C.~Munoz, A.~Smith\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   730
  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
   731
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   732
  \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
   733
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   734
  10:20 -- 11:10\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   735
  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
   736
  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
   737
  Pearl)\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   738
  F.~Immler\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   739
  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
   740
  Diamond)\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   741
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   742
  \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
   743
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   744
  11:30 -- 12:30\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   745
  A.~Anand, R.~Knepper\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   746
  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
   747
  H.~Chan, M.~Norrish\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   748
  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
   749
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   750
  \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
   751
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   752
  14:30 -- 15:30\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   753
  S.~Schneider, G.~Smolka, S.~Hack\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   754
  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
   755
  Compilers\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   756
  A.~Fox\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   757
  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
   758
  HOL4\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   759
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   760
  \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
   761
  \hline
273
0500c07aed6e updated statistics
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   762
  16:00 -- 17:00 (chair:~H.~Herbelin)\smallskip\\
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   763
  F.~Besson, S.~Blazy, P.~Wilke\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   764
  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
   765
  T.~Tuerk, M.~Myreen, R.~Kumar\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   766
  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
   767
  Generation\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   768
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   769
  \end{tabular} 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   770
& \begin{tabular}[t]{|@{\hspace{0.5mm}}p{\cw}@{\hspace{0.5mm}}|}
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   771
  \multicolumn{1}{c}{\textbf{Tuesday (6th Floor)\smallskip}}\\
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   772
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   773
  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
   774
  A.~Charguéraud, F.~Pottier\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   775
  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
   776
  Implementation\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   777
  T.~Nipkow\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   778
  Amortized Complexity Verified\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   779
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   780
  \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
   781
  \hline
273
0500c07aed6e updated statistics
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   782
  10:20 -- 11:10 (chair: J.~Urban)\smallskip\\
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   783
  S.~Blazy, D.~Demange, D.~Pichardie\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   784
  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
   785
  Test\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   786
  A.~Lochbihler, A.~Maximova\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   787
  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
   788
  Diamond)\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   789
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   790
  \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
   791
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   792
  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
   793
  L.~Birkedal\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   794
  \textbf{Invited Talk}\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   795
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   796
  \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
   797
  \hline
273
0500c07aed6e updated statistics
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   798
  14:30 -- 15:30 (chair: A.~Fox)\smallskip\\
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   799
  M.~Abdulaziz, M.~Norrish, C.~Gretton\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   800
  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
   801
  Systems\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   802
  T.~Prathamesh\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   803
  Formalizing Knot Theory in Isabelle/HOL\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   804
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   805
  \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
   806
  \hline
273
0500c07aed6e updated statistics
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   807
  16:00 -- 17:00 (chair: S.~Blazy)\smallskip\\
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   808
  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
   809
  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
   810
  Substitutions\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   811
  P.~Maksimovic, A.~Schmitt\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   812
  HOCore in Coq\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   813
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   814
  \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
   815
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   816
  17:15 -- 18:00\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   817
  \textbf{ITP Business Meeting}\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   818
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   819
  \end{tabular}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   820
\end{tabular}}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   821
\end{center}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   822
\end{figure}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   823
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   824
\begin{figure}[p]
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   825
\begin{center}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   826
\rotatebox{90}{
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   827
\small
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   828
\begin{tabular}[t]{@{} *{2}{c @{\hspace{4mm}}} @{}}
273
0500c07aed6e updated statistics
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   829
   \mbox{}\\[-20mm]
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   830
   \begin{tabular}[t]{|@{\hspace{0.5mm}}L{90mm}@{\hspace{0.5mm}}|}
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   831
   \multicolumn{1}{c}{\textbf{Wednesday (6th Floor)\smallskip}}\\
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   832
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   833
   9:00 -- 10:00\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   834
   R.~Spadotti\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   835
   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
   836
   Theory\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   837
   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
   838
   Transfinite Constructions in Classical Type Theory\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   839
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   840
   \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
   841
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   842
   10:30 -- 11:30\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   843
   M.~Norrish\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   844
   \textbf{Invited Talk}\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   845
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   846
   \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
   847
   \hline
269
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   848
   12:30 -- 22:30\smallskip\\
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   849
   Excursion to Ge Yuan Garden and Slender West Lake\smallskip\\
269
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   850
   The bus departs at 12:30 sharp from the hotel.\smallskip\\
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   851
   Dinner will be at the Lion Pavilion restaurant which is close
269
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   852
   to the Slender West Lake.\smallskip\\
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   853
   We expect to be back at the hotel around 22:30.\\
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   854
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   855
   \end{tabular}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   856
 & \begin{tabular}[t]{|@{\hspace{0.5mm}}L{130mm}@{\hspace{0.5mm}}|@{}}
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   857
   \multicolumn{1}{c}{\textbf{Thursday (6th Floor)\smallskip}}\\
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   858
   \hline
273
0500c07aed6e updated statistics
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   859
   9:00 -- 10:00 (chair: G.~Smolka)\smallskip\\
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   860
   B.~Fallenstein, R.~Kumar\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   861
   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
   862
   to Model Polymorphism\smallskip\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   863
   O.~Kunčar, A.~Popescu\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   864
   A Consistent Foundation for Isabelle/HOL\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   865
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   866
   \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
   867
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   868
   10:20 -- 11:10\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   869
   Z.~Paraskevopoulou \textit{et al}\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   870
   Foundational Property-Based Testing\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   871
   C.~Kaliszyk, J.~Urban, J.~Vyskocil\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   872
   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
   873
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   874
   \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
   875
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   876
   11:30 -- 12:30\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   877
   F.~Sieczkowski, A.~Bizjak, L.~Birkedal\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   878
   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
   879
   Languages\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   880
   S.~Boulmé, A.~Maréchal\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   881
   Refinement to Certify Abstract Interpretations, Illustrated 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   882
   on Linearization for Polyhedra\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   883
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   884
   \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
   885
   \hline
273
0500c07aed6e updated statistics
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   886
   14:30 -- 15:30 (chair: C.~Wu)\smallskip\\
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   887
   C.~Sternagel, R.~Thiemann\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   888
   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
   889
   R.~Affeldt, J.~Garrigue\\
269
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   890
   Formalization of Error-Correcting Codes: from Hamming to Modern Coding 
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   891
   Theory\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   892
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   893
   \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
   894
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   895
   16:00 -- 17:00\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   896
   P.~Lammich\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   897
   Refinement to Imperative/HOL\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   898
   B.~Barras, C.~Tankink, E.~Tassi\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   899
   Asynchronous Processing of Coq Documents: 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   900
   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
   901
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   902
   \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
   903
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   904
   17:15 -- 17:45\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   905
   L.~Cruz-Filipe, P.~Schneider-Kamp\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   906
   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
   907
   Certified Proof Checker\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   908
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   909
   \end{tabular} 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   910
\end{tabular}}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   911
\end{center}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   912
\end{figure}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   913
165
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   914
\end{document}