--- 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}