booklet.tex
author Christian Urban <christian dot urban at kcl dot ac dot uk>
Sun, 16 Aug 2015 20:02:48 +0800
changeset 275 f12df1a3ab0c
parent 274 42b793ea9897
child 276 5a76422d8c6c
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
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   157
careful though: You might come from a region where traffic rules are
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   158
organised so that pedestrians are mostly
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   159
treated with respect by all other road users, or even have an
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   160
``elevated status'' because they are considered the ``weakest''. 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   161
Traffic in China is, in contrast, organised more, shall we say, 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   162
according to a Darwinian model: Under no circumstance assume a
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   163
car (or even a bicycle or one of the noiseless electric motor bikes) will stop for you. As pedestrian, you
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   164
have to take care of everybody else. Therefore, whenever
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   165
possible cross roads at traffic lights and even if the light
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   166
shows green for you, look out for cars that pay no attention to this
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   167
fact. Also, zebra crossings do \emph{not}, I repeat, \emph{do not} 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   168
have any special meaning in
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   169
China for the road users higher up the traffic ladder
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   170
(i.e.~bicycles and above). 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   171
Even if it sounds too funny, take
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   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
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   201
\item \textbf{Map of Hotel / Taxis}\hspace{3mm} While more and 
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   202
more young Chinese are exposed to English, you cannot 
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   203
rely on anyone of the general public speaking more than a few
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   204
words. Rather, you have to always calculate with the very, 
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   205
very likely scenario that nobody speaks any English at all
272
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   206
and all signs around you are written in characters that do 
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   207
not give you the 
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   208
slightest idea what they are about. This means you always
265
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   209
have to prepare your travelling beforehand and ask us for help
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   210
if you are unsure! 
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   211
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   212
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
   213
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
   214
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
   215
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
   216
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
   217
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
   218
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
   219
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
   220
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
   221
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
   222
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
   223
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
   224
(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
   225
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
   226
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
   227
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
   228
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
   229
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
   230
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
   231
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
   232
metered.
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   233
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   234
\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
   235
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
   236
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
   237
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
   238
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
   239
staff with respect).
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   240
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   241
\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
   242
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
   243
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
   244
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
   245
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
   246
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
   247
(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
   248
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
   249
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
   250
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
   251
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
   252
from the hotel.
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   253
\end{itemize}
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   254
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   255
\begin{figure}[p]
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   256
\begin{tabular}{l}
272
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   257
For the driver:\medskip\\
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   258
271
024686c71dda updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   259
司机师傅,请将我送往``{\bf 童卫路20号翰苑宾馆}'',其位置如地图中红色A点所示。\\
024686c71dda updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   260
酒店电话:02584393962。谢谢!
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   261
\end{tabular}
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{center}
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   264
\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
   265
\end{center}
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   266
\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
   267
\label{hanyuan}} 
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   268
\end{figure}
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   269
 
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   270
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   271
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   272
\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
   273
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   274
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
   275
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
   276
to the hotel:
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   277
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   278
\begin{itemize}
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   279
\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
   280
      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
   281
      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
   282
      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
   283
      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
   284
      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
   285
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   286
\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
   287
      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
   288
      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
   289
      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
   290
      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
   291
      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
   292
      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
   293
      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
   294
      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
   295
      This option takes approximately
265
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   296
      55 minutes and costs 7 RMB for the metro ticket and
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   297
      around 36 RMB for the taxi.
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   298
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   299
      \begin{center}
272
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   300
      \includegraphics[scale=0.3]{travel_guide/ggg.jpg}
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   301
      \end{center}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   302
271
024686c71dda updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   303
\item If you already prepared to pay 7 RMB for the metro, why
024686c71dda updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   304
      not adding 2 more RMBs and going the whole way by metro? 
024686c71dda updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   305
      This is the third
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   306
      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
   307
      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
   308
      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
   309
      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
   310
      (see Fig.~\ref{metronanjing}). Both
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   311
      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
   312
      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
   313
      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
   314
      for directions.
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   315
 \end{itemize}
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   316
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   317
\begin{figure}[p]
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   318
\begin{center}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   319
\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
   320
\end{center}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   321
\caption{Metro map of Nanjing. Stations
269
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   322
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
   323
closest to the hotel.\label{metronanjing}} 
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   324
\end{figure}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   325
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   326
\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
   327
272
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   328
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
   329
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
   330
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
   331
see ticket machines
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   332
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   333
\begin{center}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   334
\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
   335
\hspace{4mm}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   336
\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
   337
\end{center}
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   338
265
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   339
\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
   340
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
   341
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
   342
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
   343
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
   344
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
   345
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
   346
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
   347
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
   348
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
   349
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
   350
chip at the exit gate.
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   351
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   352
\begin{center}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   353
\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
   354
\hspace{4mm}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   355
\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
   356
\end{center}
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   357
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   358
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   359
\section{Travel from Shanghai Pudong Airport}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   360
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   361
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
   362
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
   363
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
   364
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
   365
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
   366
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
   367
to the hotel. 
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   368
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   369
\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
   370
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   371
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
   372
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
   373
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
   374
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
   375
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
   376
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   377
\begin{itemize}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   378
\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
   379
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   380
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
   381
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
   382
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
   383
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   384
\begin{center}
272
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   385
\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
   386
\end{center}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   387
259
8f9400787bf4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 257
diff changeset
   388
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
   389
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
   390
\$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
   391
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
   392
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
   393
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
   394
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
   395
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
   396
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
   397
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   398
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   399
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
   400
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
   401
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
   402
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
   403
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
   404
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
   405
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   406
\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
   407
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
   408
reaching speeds of 415 km/h at certain(!) times of the day,
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   409
namely 9:02--10:47 and 15:02--16:47. At other times it will 
267
0254a6cb1182 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 266
diff changeset
   410
travel at mere speeds of 300 km/h, which you get in China
265
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   411
also with conventional high-speed trains.  Anyway, a
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   412
ticket for the Maglev will set you back around 50 RMB (\euro{}7, \$8). The
271
024686c71dda updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   413
ticket can be paid in cash or by  credit card. 
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   414
The service of the Maglev
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   415
starts at 7:02 and finished the day at 21:42.
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   416
To take this option 
265
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   417
at the airport, you will need to follow the Maglev signs. The 
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   418
main problem with
269
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   419
this option, however, is that you can only travel until  Longyang 
257
69b5b4380046 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 252
diff changeset
   420
Road Station and then have to
265
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   421
change into the overcrowded and much, much slower metro Line 2. 
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   422
The change to the
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   423
metro is a short walk from the Maglev. You have to first buy a
268
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   424
ticket inside the metro station. The good thing
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   425
about this option is that metro travelling in Shanghai is
265
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   426
pretty easy for foreigners as all stations are signed out in 
269
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   427
letters. For buying a ticket for the metro, check the section
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   428
about buying a metro ticket in Nanjing (the procedure is 
271
024686c71dda updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   429
pretty universal in China; the only exception is that 
024686c71dda updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   430
in Shanghai the metro ticket is a paper ticket, while in
024686c71dda updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   431
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
   432
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   433
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
   434
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
   435
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
   436
\end{itemize}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   437
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   438
\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
   439
High-Speed Train}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   440
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   441
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
   442
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
   443
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
   444
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
   445
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
   446
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
   447
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
   448
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
   449
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   450
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
   451
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
   452
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
   453
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
   454
anything with them.)
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   455
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   456
\begin{center}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   457
\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
   458
\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
   459
\end{center}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   460
268
a792b2f23afe booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 267
diff changeset
   461
\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
   462
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
   463
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
   464
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
   465
266
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   466
\begin{center}
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   467
\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
   468
\end{center}
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   469
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   470
\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
   471
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
   472
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
   473
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
   474
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
   475
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
   476
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
   477
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
   478
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
   479
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
   480
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   481
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
   482
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
   483
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
   484
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
   485
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
   486
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
   487
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
   488
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
   489
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
   490
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
   491
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
   492
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
   493
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
   494
266
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   495
\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
   496
269
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   497
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
   498
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
   499
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
   500
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
   501
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
   502
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
   503
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
   504
179
1d2f20938399 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 178
diff changeset
   505
%weather, electrical connectors
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   506
%% when does the welcome reception start?
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   507
%% breakfast needs more coffee
166
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 165
diff changeset
   508
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   509
\chapter{Conference}
265
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   510
272
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   511
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
   512
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
   513
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
   514
until Sunday on the 1st floor close to the hotel check in.
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   515
There will be a welcome reception on Sunday (23th) also on the
272
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   516
first floor. 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
   517
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
   518
outside the conference hall. On Wednesday (26th) afternoon
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   519
there will be the ITP-excursion to Yangzhou and the Slender
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   520
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
   521
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
   522
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
   523
booklet.
271
024686c71dda updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 270
diff changeset
   524
272
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   525
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
   526
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
   527
until 9:00. When you check into the hotel, you will receive a
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   528
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
   529
going to breakfast. Hanyuan Hotel also includes a very good
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   530
restaurant, but unfortunately it is a bit on the pricier side.
265
9d6713f010b4 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 259
diff changeset
   531
272
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   532
\begin{itemize}
273
0500c07aed6e updated statistics
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   533
\item\textbf{Near the Hotel}\hspace{3mm}The Hanyuan hotel is 
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   534
located at the intersection of a big road (NingHang Road 宁杭公路)
272
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   535
and a smaller road (TongWei Road 童卫路). If you need a taxi to
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   536
go to Downtown Nanjing, for example, it is probably the easiest to hail 
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   537
down a taxi at the big street. An ATM machine is situated a few 
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   538
minutes down the smaller TongWei Road. If you want to take a 
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   539
walk in the evening, Xingyuan suggest a stroll through the 
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   540
Purple Mountain Area on the top-right in the map in 
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   541
Fig.~\ref{hotelmap}. This area is approximately a 15 minutes 
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   542
walk away from the hotel and contains for example the Sun Yat 
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   543
Sen memorial and the Linggu pagoda.
272
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   544
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   545
\begin{center}
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   546
\includegraphics[scale=0.45]{travel_guide/map1a.jpg}
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   547
\hspace{5mm}
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   548
\includegraphics[scale=0.43]{travel_guide/linggusu.jpg}
272
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   549
\end{center}
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   550
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   551
\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
   552
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   553
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
   554
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
   555
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
   556
easier to reach: just down TongWei Road and then turn left
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   557
down the hill. The entrance of the metro is on the left-hand
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   558
side. However it is not the most scenic route. More scenic is
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   559
the walk to Xiamafang Metro Station through the campus of the
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   560
Nanjing Agriculture University. Unfortunately the way is not
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   561
so straightforward. If you are unfamiliar with the way, we
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   562
suggest you walk to Muxuyuan station; once you followed some
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   563
locals and know the way, go to Xiamafang station.
272
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   564
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   565
\begin{figure}[p]
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   566
\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
   567
\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
   568
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
   569
(indicated with a red star)
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   570
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
   571
\end{figure}
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   572
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   573
\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
   574
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
   575
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
   576
area including Xingyuan's favourite restaurant for having
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   577
lunch on workdays
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   578
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   579
\begin{center}
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   580
\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
   581
\end{center}
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   582
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   583
\noindent This area also contains a ``Mickey Mouse bakery'',
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   584
which stocks pastries similar to ones you might find in a 
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   585
Western bakery (just in case you get bored of the baozi
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   586
at breakfast in the hotel) and a pizza place in case you need 
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   587
to eat something different than Chinese. 
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   588
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   589
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
   590
Tongwei road including some native restaurants, and also some
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   591
restaurants on the opposite side of NingHang Road. A smaller
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   592
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
   593
in the Xiamafang area.
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   594
\end{itemize}
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
\section{Further Afield}
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   597
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   598
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
   599
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
   600
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   601
\begin{itemize}
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   602
\item\textbf{Shopping}\hspace{3mm}
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   603
The most serious shopping malls in Nanjing can be found in the
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   604
area around Xinjiekou and Daxinggong metro stations (on Line~2).
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   605
Especially in multi-brand shopping malls the shopping goes
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   606
like this: You find something you like. You agree the prize
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   607
with the shop-assistant. You get a piece of paper, which you
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   608
need to take to a cashier nearby. You pay there, get another
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   609
piece of paper, which you take back to the store, where you
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   610
receive your goods. Another quirk of shopping in China is that
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   611
when the sale says, for example, ``80\% off'', it is actually
275
f12df1a3ab0c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 274
diff changeset
   612
20\% off, meaning 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
   613
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   614
\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
   615
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
   616
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
   617
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
   618
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   619
\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
   620
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
   621
Today you can see remainders at the North Gate near 
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   622
Zhonghuamen Mtro Station on Line~1. From the station follow
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   623
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
   624
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   625
\begin{center}
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   626
\includegraphics[scale=0.8]{travel_guide/map3.jpg}
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   627
\hspace{5mm}
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   628
\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
   629
\end{center}
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   630
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   631
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   632
\noindent There is also another substantial and impressive
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   633
section of the remaining city visible very close to the hotel:
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   634
Walk the NingHuan Road towards the city centre, once you
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   635
traversed the river, bear right. You will see a rather
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   636
tall wall build of grey stones.
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   637
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   638
Another scenic spot is the Xuanwu Lake, dotted with several
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   639
beautiful small islands and a good place to have a walk. You
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   640
can reach the lake by taking exit Xuanwumen at Line~3. 
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   641
Xingyuan suggest the walk indicated red below.
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   642
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   643
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   644
\begin{center}
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   645
\includegraphics[scale=0.8]{travel_guide/map4.jpg}
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   646
\end{center}
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   647
275
f12df1a3ab0c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 274
diff changeset
   648
\noindent The ultimate bird's-eye view of Nanjing you can have
f12df1a3ab0c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 274
diff changeset
   649
from the Zifeng Tower. For this you have to go to Guluo Metro
f12df1a3ab0c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 274
diff changeset
   650
Station on Line~1. According to Wiki, the Zifeng Tower is the
f12df1a3ab0c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 274
diff changeset
   651
11th tallest building in the World (to compare, the Shard is
f12df1a3ab0c updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 274
diff changeset
   652
ranked 92nd and the Sears Tower 12th).
274
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   653
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   654
\end{itemize}
42b793ea9897 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 273
diff changeset
   655
272
42f24df619f8 updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 271
diff changeset
   656
\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
   657
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   658
On Wednesday afternoon there will be the traditional ITP
269
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   659
excursion, this time to a Chinese garden in Yangzhou and to the
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   660
Slender West Lake. You might like to note a few points:

\begin{itemize}
\item The conference session will end at 11:30, and you 
266
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   661
  should finish lunch no later than 12:20 in order to get 
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   662
  to the hotel lobby.
\item Boarding the shuttle bus is at 12:30 sharp!
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   663
\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
   664
  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
   665
  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
   666
  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
   667
  \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
   668
  
266
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   669
\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
   670
  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
   671
  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
   672
  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
   673
  Wiki has some rudimentary information at
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   674
  \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
   675
\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
   676
  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
   677
  Pavilion) is located on the campus 
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   678
  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
   679
    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
   680
  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
   681
\end{itemize}
7a052c75818b updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 265
diff changeset
   682
269
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   683
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   684
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   685
\newlength{\cw}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   686
\setlength{\cw}{100mm}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   687
\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
   688
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   689
\begin{figure}[p]
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   690
\begin{center}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   691
\rotatebox{90}{
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   692
\small
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   693
\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
   694
 \mbox{}\\[-15mm]
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   695
 \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
   696
  \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
   697
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   698
  9:00 -- 10:00\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   699
  Short Intro Session\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   700
  M.~Moscato, C.~Munoz, A.~Smith\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   701
  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
   702
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   703
  \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
   704
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   705
  10:20 -- 11:10\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   706
  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
   707
  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
   708
  Pearl)\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   709
  F.~Immler\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   710
  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
   711
  Diamond)\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   712
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   713
  \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
   714
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   715
  11:30 -- 12:30\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   716
  A.~Anand, R.~Knepper\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   717
  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
   718
  H.~Chan, M.~Norrish\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   719
  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
   720
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   721
  \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
   722
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   723
  14:30 -- 15:30\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   724
  S.~Schneider, G.~Smolka, S.~Hack\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   725
  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
   726
  Compilers\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   727
  A.~Fox\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   728
  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
   729
  HOL4\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   730
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   731
  \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
   732
  \hline
273
0500c07aed6e updated statistics
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   733
  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
   734
  F.~Besson, S.~Blazy, P.~Wilke\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   735
  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
   736
  T.~Tuerk, M.~Myreen, R.~Kumar\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   737
  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
   738
  Generation\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   739
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   740
  \end{tabular} 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   741
& \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
   742
  \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
   743
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   744
  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
   745
  A.~Charguéraud, F.~Pottier\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   746
  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
   747
  Implementation\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   748
  T.~Nipkow\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   749
  Amortized Complexity Verified\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   750
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   751
  \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
   752
  \hline
273
0500c07aed6e updated statistics
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   753
  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
   754
  S.~Blazy, D.~Demange, D.~Pichardie\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   755
  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
   756
  Test\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   757
  A.~Lochbihler, A.~Maximova\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   758
  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
   759
  Diamond)\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   760
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   761
  \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
   762
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   763
  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
   764
  L.~Birkedal\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   765
  \textbf{Invited Talk}\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   766
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   767
  \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
   768
  \hline
273
0500c07aed6e updated statistics
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   769
  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
   770
  M.~Abdulaziz, M.~Norrish, C.~Gretton\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   771
  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
   772
  Systems\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   773
  T.~Prathamesh\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   774
  Formalizing Knot Theory in Isabelle/HOL\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   775
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   776
  \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
   777
  \hline
273
0500c07aed6e updated statistics
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   778
  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
   779
  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
   780
  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
   781
  Substitutions\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   782
  P.~Maksimovic, A.~Schmitt\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   783
  HOCore in Coq\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   784
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   785
  \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
   786
  \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   787
  17:15 -- 18:00\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   788
  \textbf{ITP Business Meeting}\\
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
  \end{tabular}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   791
\end{tabular}}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   792
\end{center}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   793
\end{figure}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   794
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   795
\begin{figure}[p]
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   796
\begin{center}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   797
\rotatebox{90}{
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   798
\small
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   799
\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
   800
   \mbox{}\\[-20mm]
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   801
   \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
   802
   \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
   803
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   804
   9:00 -- 10:00\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   805
   R.~Spadotti\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   806
   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
   807
   Theory\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   808
   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
   809
   Transfinite Constructions in Classical Type Theory\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   810
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   811
   \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
   812
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   813
   10:30 -- 11:30\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   814
   M.~Norrish\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   815
   \textbf{Invited Talk}\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   816
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   817
   \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
   818
   \hline
269
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   819
   12:30 -- 22:30\smallskip\\
252
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   820
   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
   821
   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
   822
   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
   823
   to the Slender West Lake.\smallskip\\
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   824
   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
   825
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   826
   \end{tabular}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   827
 & \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
   828
   \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
   829
   \hline
273
0500c07aed6e updated statistics
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   830
   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
   831
   B.~Fallenstein, R.~Kumar\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   832
   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
   833
   to Model Polymorphism\smallskip\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   834
   O.~Kunčar, A.~Popescu\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   835
   A Consistent Foundation for Isabelle/HOL\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   836
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   837
   \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
   838
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   839
   10:20 -- 11:10\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   840
   Z.~Paraskevopoulou \textit{et al}\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   841
   Foundational Property-Based Testing\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   842
   C.~Kaliszyk, J.~Urban, J.~Vyskocil\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   843
   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
   844
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   845
   \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
   846
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   847
   11:30 -- 12:30\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   848
   F.~Sieczkowski, A.~Bizjak, L.~Birkedal\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   849
   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
   850
   Languages\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   851
   S.~Boulmé, A.~Maréchal\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   852
   Refinement to Certify Abstract Interpretations, Illustrated 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   853
   on Linearization for Polyhedra\\
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
   \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
   856
   \hline
273
0500c07aed6e updated statistics
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 272
diff changeset
   857
   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
   858
   C.~Sternagel, R.~Thiemann\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   859
   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
   860
   R.~Affeldt, J.~Garrigue\\
269
63533b57ad89 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   861
   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
   862
   Theory\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   863
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   864
   \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
   865
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   866
   16:00 -- 17:00\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   867
   P.~Lammich\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   868
   Refinement to Imperative/HOL\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   869
   B.~Barras, C.~Tankink, E.~Tassi\\ 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   870
   Asynchronous Processing of Coq Documents: 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   871
   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
   872
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   873
   \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
   874
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   875
   17:15 -- 17:45\smallskip\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   876
   L.~Cruz-Filipe, P.~Schneider-Kamp\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   877
   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
   878
   Certified Proof Checker\\
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   879
   \hline
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   880
   \end{tabular} 
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   881
\end{tabular}}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   882
\end{center}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   883
\end{figure}
955b54dc16cc updated booklet
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 198
diff changeset
   884
165
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   885
\end{document}