\usepackage{dina4}

\usepackage{fancyvrb}

\usepackage[table]{xcolor}

\usepackage{floatpag}

\floatpagestyle{empty}

\definecolor{linkcolor}{rgb}{0,0,0.5}

\usepackage[colorlinks=true,linkcolor=linkcolor,citecolor=linkcolor,filecolor=linkcolor,pagecolor=linkcolor,urlcolor=linkcolor]{hyperref}

\chapter{Arrival}

Welcome in China. You made it to the airport. Unless your are

one of the very few foreigners who can speak and read Chinese,

potentially the most challenging part of your journey is about

to begin. Below we explain how to get to Hanyuan Hotel in Nanjing

from Shanghai Pudong Airport and from Nanjing Lukou Airport. If you

arrive from somewhere else and need help, please let us know.

China is generally a safe country for travelling, if the usual

precautions are taken. We assume you have never been in China 

before, therefore let us still start with some general points.

\begin{itemize}

\item \textbf{Weather}\hspace{3mm} 

Unfortunately end of August is the time when it will be especially

hot in Nanjing (over 30$^{\circ}$C). Be prepared with lots of

light clothes, but do not forget a jumper, or sweater, since many

places are air-conditioned. It can also rain.

\item \textbf{Bottled water}\hspace{3mm}

Whereas in many places it is safe to drink water from taps,

do not take chances and drink only bottled water! During the

conference we will provide bottled water. In other places you

have to buy bottles yourself. Remember, Chinese are famous for

nibbling on hot tea the whole day, even in sweltering 

temperatures. There is a reason for this. 

\item \textbf{Traffic}\hspace{3mm} 

Do not even think of renting a car in China. Hence, while in

China, you probably will be mostly going around on foot. Be

careful though: You might come from a region where traffic rules are

organised so that pedestrians are mostly

treated with respect by all other road users, or even have an

``elevated status'' because they are considered the ``weakest''. 

Traffic in China is, in contrast, organised more, shall we say, 

according to a Darwinian model: Under no circumstance assume a

car (or even a bicycle or the noiseless electric motor bikes) will stop for you. As pedestrian, you

have to take care of everybody else. Therefore, whenever

possible cross roads at traffic lights and even if the light

shows green for you, look out for cars that pay no attention to this

fact. Also, zebra crossings do \emph{not}, I repeat, \emph{do not} 

have any special meaning in

China for the road users higher up the traffic ladder

(i.e.~bicycles and above). 

Even if it sounds too funny, take

our word and head this advice\ldots{}it might increase your

life-expectancy. 

\item \textbf{Free Public Wifi / Mobile Phones}\hspace{3mm}

While free public wifi is nowadays pretty ubiquitous in big

cities in China (Starbucks, Costas, McDonalds are obvious

places where to find wifi), you need a working mobile phone in

order to use it. You will have to register your number when

you log in, and the wifi operator will then send you a

password token via SMS. The problem is that chances are great

your mobile phone will \emph{not} work in China. Therefore do

not assume you can check information on the Internet while

travelling. 

At the hotel there will be wifi (with the super-secure

password: 123456789). But again, do not assume you can

download that last episode of the Daily Show: while bandwidth

will generally be enough for reading email, be prepared for an

uninterrupted stay in China, free from any disturbance coming

from online demands.

\item \textbf{Google etc}\hspace{3mm}There are two Great Walls in

China: one prevents you from accessing Google, for example. Use

\url{www.aol.com} or \url{www.bing.com} instead as your preferred

search engine. Also, if you care about such things, set you 

status on Facebook to ``unavailable'' for the period of time

you will be in China. 

\item \textbf{Map of Hotel}\hspace{3mm} test

\end{itemize}

\section{Travel from Nanjing Lukou Airport}

\subsection{Taxi\label{nanjingtaxi}}

\section{Travel from Shanghai Pudong Airport}

Many of the participants will arrive at Shanghai Pudong

Airport. From there, in short, you have to get to (1) the Hong

Qiao railway station and then from there to (2) Nanjing Nan

railway station. From Nanjing Nan, you can follow the

suggestions in Section \ref{nanjingtaxi}. Overall this will

take approximately 3h of travelling to the hotel. 

\subsection*{From Shanghai Pudong Airport to Hong Qiao Train Station}

For the first leg to Hong Qiao train station there are

essentially two travel options: one recommended by locals

and being the more sensible option is to take the airport bus;

the other is by the World's only commercial Maglev train 

and a change to the metro. 

\begin{itemize}

\item \textbf{Option 1 by Airport bus}: 

At the Pudong Airport follow the signs for Airport Bus, or Airport

Ring Bus. You have to take Line 1, which operates between 7:00

and 23:00. The bus stop where you have to wait is 

\begin{center}

\begin{minipage}[t]{10cm}

\mbox{\includegraphics{travel_guide/image005.jpg}}

\end{minipage}

\end{center}

The waiting time is around 30 minutes ??? The ticket costs 30

RMB (\euro{}4.25, \$5) and can be bought on the bus. This

however requires cash. While you wait, be prepared to be

harassed by taxi drivers, who insist on driving you to Hong Qiao

train station. You can ignore them: it will cost you more,

around 100 RMB; the bus is comfortable and air-conditioned,

unlike the taxi; and, like the taxi driver, the bus driver

already aims for maximum possible speed given good 

road conditions. 

The airport bus takes around 1h and makes only two stops at

the very end of the journey. Both stops are in near

proximity. You have to take the \emph{second} stop at Hong Qiao

Railway Station. You will be able to see the big signs of

Hong Qiao Railway Station when you approach the station. Do 

not take the exit for Hong Qiao International Airport.

\item \textbf{Option 2 Maglev train / Metro}: 

Of course travelling on the Maglev is pretty cool\ldots{}

reaching speeds of 415 km/h at certain(!) times of the day,

namely 9:02--10:47 and 15:02--16:47. At other time it will 

travel only at ``lame'' 300 km/h. Anyway, a

ticket will set you back around 50 RMB (\euro{}7, \$8). The

ticket can be paid in cash or credit card. To take this option 

at the airport, you will need to follow the Maglev signs. The problem with

this option, however, is that you can only go until ??? Then you have to

change into the overcrowded metro line ??? The change to the

metro is a short walk from the Maglev. You have to first buy a

ticket at the metro station and then take Line ... The good thing

about this option is that metro travelling in Shanghai is

pretty easy for foreigners as all stations are signed out in letters. Overall

the journey time of this option is also around 1h. So unless

you really want to sample the feeling of travelling for 7

minutes at 415 km/h, we recommend Option 1 by bus. 

\end{itemize}

\subsection*{From Hong Qiao Train Station to Nanjing Nan via

High-Speed Train}

The airport bus will stop directly in front of the southern

part of the Hong Qiao train station. As background, train

stations above the village level in China are organised more

like an airport, than the sleepy train station you might be

familiar with. Therefore you first have to go through a

security gate where luggage is checked and you padded by a

security guard. The security guard might be of either sex and

this is seen as normal by Chinese. The entire check is done

orderly, but appears to be only a token check and so

fortunately is very speedy. 

Next you need to buy a train ticket. There are ticket

counters, see left below, signed out in the main hall. 

\begin{center}

\includegraphics[scale=0.8]{travel_guide/image038.jpg}

\includegraphics[scale=0.8]{travel_guide/image040.jpg} 

\end{center}

\noindent You have to queue on the longer queue and buy a

ticket for Nanjing Nan (Nan stands for South station). You

will need to show your passport in order to buy a ticket. The

ticket will cost around 135 RMB and looks like this:

The G-Number (G42 above) stands for the train number. Then

there is the coach number and seat number. The ticket above is

for second class (-\ -). For the short duration of the trip

there is no real need to buy a ticket for first class.

Next you have to wait for your train on the main concourse of

the station. On the main display the platform of your train

will be displayed 30 minutes before departure. Assuming you

have some time, rest for a moment and take in the atmosphere

of a typical Chinese train station\ldots nothing like what you

can experience, for example, at Clapham Junction during

rush-hour.\footnote{Trivia, in case you did not know: Clapham Junction

supposedly is the biggest train station in Europe in terms of

passengers and rail tracks.}

Once you know the platform, go to the gate. Be careful, the

gates are nestled between the shops and might be easily

overlooked. For each platform there are two gates labelled `A'

and `B', respectively. `A' stands for the front of the train 

and `B' for the rear -- you know which one to go from your 

ticket.

\newlength{\cw}

\setlength{\cw}{100mm}

\newcolumntype{L}[1]{>{\raggedright\let\newline\\\arraybackslash\hspace{0pt}}m{#1}}

\begin{figure}[p]

\begin{center}

\rotatebox{90}{

\small

\begin{tabular}[t]{@{}*{2}{c @{\hspace{4mm}}} @{}}

 \mbox{}\\[-20mm]

 \begin{tabular}[t]{@{}|@{\hspace{0.5mm}}L{\cw}@{\hspace{0.5mm}}|}

  \multicolumn{1}{c}{\textbf{Monday}}\\

  \hline

  9:00 -- 10:00\smallskip\\

  Short Intro Session\smallskip\\

  M.~Moscato, C.~Munoz, A.~Smith\\

  Affine Arithmetic and Applications to Real-Number Proving\\

  \hline

  \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\

  \hline

  10:20 -- 11:10\smallskip\\

  J.~Hölzl, A.~Lochbihler, D.~Traytel\\ 

  A Formalized Hierarchy of Probabilistic System Types (Proof 

  Pearl)\smallskip\\

  F.~Immler\\ 

  A Verified Enclosure for the Lorenz Attractor (Rough 

  Diamond)\\

  \hline

  \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\

  \hline

  11:30 -- 12:30\smallskip\\

  A.~Anand, R.~Knepper\\ 

  ROSCoq: Robots Powered by Constructive Reals\smallskip\\

  H.~Chan, M.~Norrish\\

  Mechanisation of AKS Algorithm: Part 1 – the Main Theorem\\

  \hline

  \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}2hs lunch break}\\

  \hline

  14:30 -- 15:30\smallskip\\

  S.~Schneider, G.~Smolka, S.~Hack\\ 

  A First-Order Functional Intermediate Language for Verified 

  Compilers\smallskip\\

  A.~Fox\\ 

  Improved Tool Support for Machine-Code Decompilation in 

  HOL4\\

  \hline

  \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}30 mins coffee break}\\

  \hline

  16:00 -- 17:00\smallskip\\

  F.~Besson, S.~Blazy, P.~Wilke\\ 

  A Concrete Memory Model for CompCert\smallskip\\

  T.~Tuerk, M.~Myreen, R.~Kumar\\

  Pattern Matches in HOL: A New Representation and Improved Code 

  Generation\\

  \hline

  \end{tabular} 

& \begin{tabular}[t]{|@{\hspace{0.5mm}}p{\cw}@{\hspace{0.5mm}}|}

  \multicolumn{1}{c}{\textbf{Tuesday}}\\

  \hline

  9:00 -- 10:00 (chair: M.~Norrish)\smallskip\\

  A.~Charguéraud, F.~Pottier\\

  Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find 

  Implementation\smallskip\\

  T.~Nipkow\\ 

  Amortized Complexity Verified\\

  \hline

  \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\

  \hline

  10:20 -- 11:10\smallskip\\

  S.~Blazy, D.~Demange, D.~Pichardie\\

  Validating Dominator Trees for a Fast, Verified Dominance 

  Test\smallskip\\

  A.~Lochbihler, A.~Maximova\\

  Stream Fusion for Isabelle’s Code Generator (Rough 

  Diamond)\\

  \hline

  \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\

  \hline

  11:30 -- 12:30 (chair: X.~Zhang)\smallskip\\

  L.~Birkedal\\

  \textbf{Invited Talk}\\

  \hline

  \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}2hs lunch break}\\

  \hline

  14:30 -- 15:30\smallskip\\

  M.~Abdulaziz, M.~Norrish, C.~Gretton\\

  Verified Over-Approximation of the Diameters of Propositionally Factored Transition 

  Systems\smallskip\\

  T.~Prathamesh\\

  Formalizing Knot Theory in Isabelle/HOL\\

  \hline

  \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}30 mins coffee break}\\

  \hline

  16:00 -- 17:00\smallskip\\

  S.~Schäfer, T.~Tebbi, G.~Smolka\\ 

  Autosubst: Reasoning with de Bruijn Terms and Parallel 

  Substitutions\smallskip\\

  P.~Maksimovic, A.~Schmitt\\

  HOCore in Coq\\

  \hline

  \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}short coffee break}\\

  \hline

  17:15 -- 18:00\smallskip\\

  \textbf{ITP Business Meeting}\\

  \hline

  \end{tabular}

\end{tabular}}

\end{center}

\end{figure}

\begin{figure}[p]

\begin{center}

\rotatebox{90}{

\small

\begin{tabular}[t]{@{} *{2}{c @{\hspace{4mm}}} @{}}

   \mbox{}\\[-30mm]

   \begin{tabular}[t]{|@{\hspace{0.5mm}}L{90mm}@{\hspace{0.5mm}}|}

      \multicolumn{1}{c}{\textbf{Wednesday}}\\

   \hline

   9:00 -- 10:00\smallskip\\

   R.~Spadotti\\

   A Mechanized Theory of Regular Trees in Dependent Type 

   Theory\smallskip\\

   G.~Smolka, S.~Schäfer, C.~Doczkal\\

   Transfinite Constructions in Classical Type Theory\\

   \hline

   \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}30 mins coffee break}\\

   \hline

   10:30 -- 11:30\\

   M.~Norrish\\

   \textbf{Invited Talk}\\

   \hline

   \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}1h Lunch break}\\

   \hline

   12:30 -- 21:30\smallskip\\

   Excursion to Ge Yuan Garden and Slender West Lake\smallskip\\

   Bus departs at 12:30 sharp from the hotel\smallskip\\

   Dinner will be at the Lion Pavilion restaurant which is close

   to the Slender West Lake\smallskip\\

   We expect to be back at the hotel around 22:30\\

   \hline

   \end{tabular}

 & \begin{tabular}[t]{|@{\hspace{0.5mm}}L{130mm}@{\hspace{0.5mm}}|@{}}

   \multicolumn{1}{c}{\textbf{Thursday}}\\

   \hline

   9:00 -- 10:00\smallskip\\

   B.~Fallenstein, R.~Kumar\\ 

   Proof-Producing Reflection for HOL, with an Application 

   to Model Polymorphism\smallskip\\ 

   O.~Kunčar, A.~Popescu\\ 

   A Consistent Foundation for Isabelle/HOL\\

   \hline

   \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\

   \hline

   10:20 -- 11:10\smallskip\\

   Z.~Paraskevopoulou \textit{et al}\\ 

   Foundational Property-Based Testing\smallskip\\

   C.~Kaliszyk, J.~Urban, J.~Vyskocil\\ 

   Learning To Parse on Aligned Corpora (Rough Diamond)\\

   \hline

   \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\

   \hline

   11:30 -- 12:30\smallskip\\

   F.~Sieczkowski, A.~Bizjak, L.~Birkedal\\ 

   ModuRes: A Coq Library for Modular Reasoning about Concurrent Higher-Order Imperative Programming 

   Languages\smallskip\\

   S.~Boulmé, A.~Maréchal\\

   Refinement to Certify Abstract Interpretations, Illustrated 

   on Linearization for Polyhedra\\

   \hline

   \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}2hs lunch break}\\

   \hline

   14:30 -- 15:30\smallskip\\

   C.~Sternagel, R.~Thiemann\\

   Deriving Comparators and Show-Functions in Isabelle/HOL\smallskip\\

   R.~Affeldt, J.~Garrigue\\

   Formalization of Error-correcting Codes: from Hamming to Modern Coding 

   Theory\\

   \hline

   \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}30 mins coffee break}\\

   \hline

   16:00 -- 17:00\smallskip\\

   P.~Lammich\\

   Refinement to Imperative/HOL\smallskip\\

   B.~Barras, C.~Tankink, E.~Tassi\\