# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1439439788 -28800
# Node ID 955b54dc16cc350846ce9b3f47b982032cb9d9c2
# Parent  803fa2e4993f196b15b11e7d54f3cb1c78e133fc
updated booklet

diff -r 803fa2e4993f -r 955b54dc16cc booklet.pdf
Binary file booklet.pdf has changed
diff -r 803fa2e4993f -r 955b54dc16cc booklet.tex
--- a/booklet.tex	Thu Aug 13 07:37:12 2015 +0800
+++ b/booklet.tex	Thu Aug 13 12:23:08 2015 +0800
@@ -1,8 +1,15 @@
 \documentclass[11pt]{report}
+\usepackage{dina4}
 \usepackage{eurosym}
 \usepackage{fontspec}
 \usepackage[sc]{mathpazo}
 \setmainfont[Ligatures=TeX]{Palatino Linotype}
+\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}
 
 \def\xyzemail{xingyuanzhang at 126 dot com}
 \def\cwemail{chunhanwu at 126 dot com} 
@@ -97,10 +104,406 @@
 He will e-mail you the invitation letter. You might also need
 your hotel booking (see above) and flight details for the visa
 application.

-\chapter{Post-Arrival}
+
+
+\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}
 
-TBD 
+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.
 
 %weather, electrical connectors
 
+\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\\ 
+   Asynchronous Processing of Coq Documents: 
+   from the Kernel up to the User Interface\\
+   \hline
+   \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}short coffee break}\\
+   \hline
+   17:15 -- 17:45\smallskip\\
+   L.~Cruz-Filipe, P.~Schneider-Kamp\\
+   Formalizing Size-Optimal Sorting Networks: Extracting a 
+   Certified Proof Checker\\
+   \hline
+   \end{tabular} 
+\end{tabular}}
+\end{center}
+\end{figure}
+
 \end{document}