itp-2015: comparison booklet.tex

equal deleted inserted replaced

-:0500c07aed6e
+:42b793ea9897
 In short
 \begin{itemize}
 \item[(1)] you need to make a bank transfer for the conference
 fee in your local currency, and
-\item[(2)] you need to email Xingyuan with your details\\
+\item[(2)] you need to email Xingyuan with your details
 (\xyzemail)
 \end{itemize}
 \noindent Xingyuan will then confirm that the payment has been
 received. Note that if you are Chinese and need a \emph{fa
 Daxinggong to Line 2 for Xiamafang or Muxuyuan, which
 are the closest stations to the Hanyuan Hotel
 (see Fig.~\ref{metronanjing}). Both
 stations then need a 15 minutes walk to the hotel.
 This is another disadvantage of this option if you have
-a heavy suitcase.
+a heavy suitcase. See the map shown in Fig.~\ref{hotelmap}
-\end{itemize}
+for directions.
+\end{itemize}
 \begin{figure}[p]
 \begin{center}
 \makebox[0mm]{\includegraphics[scale=1.1]{travel_guide/metromapnanjing.png}}
 \end{center}
 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 it is best to take a taxi,
 but you can also take the metro as explained in the previous
-section. Overall this will take approximately 3h of travelling
+section. Overall this will take approximately 4h of travelling
 to the hotel.
-\subsection*{From Shanghai Pudong Airport to Hong Qiao Train Station}
+\subsection*{From Shanghai Pudong Airport to Hong Qiao Railway 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
 you need to take a yellow taxi that goes to ``Nanjing
 Downtown''. The taxi will cost around 36 RMB and needs to be
 paid in cash. Show the driver the map in Fig~\ref{hanyuan}.
 %weather, electrical connectors
+%% when does the welcome reception start?
-\chapter{At the Conference}
+%% breakfast needs more coffee
+\chapter{Conference}
 The Isabelle tutorial will take place from Friday (21st) to
 Sunday (23rd) in a conference room on the 4th floor of Hanyuan
 Hotel. There will be a reception desk of ITP from Thursday
 until Sunday on the 1st floor close to the hotel check in.
-There will be a reception buffet on Sunday (23th) also on the
+There will be a welcome reception on Sunday (23th) also on the
 first floor. The ITP conference will take place on the 6th
-floor and the reception desk will be just outside the
+floor and starting from Monday the reception desk will be just
-conference hall. On Wednesday (26th) afternoon there will be
+outside the conference hall. On Wednesday (26th) afternoon
-the ITP-excursion to Yangzhou and the Slender West Lake (see
+there will be the ITP-excursion to Yangzhou and the Slender
-Sect.~\ref{excursion}). The
+West Lake (see Sect.~\ref{excursion}). The Coq tutorial will
-Coq tutorial will take place from Thursday (27th) until
+take place from Thursday (27th) until Saturday (29th) on the
-Saturday (29th) on the 4th floor. The programme of the talks
+4th floor. The programme of the talks is at the end of this
-is at the end of this booklet.
+booklet.
 Breakfast and lunches are served on 1st floor next to hotel
 registration desk. The breakfast buffet is open from 7:00
 until 9:00. When you check into the hotel, you will receive a
 green paper ticket for each day which you have to show before
-going to breakfast.
+going to breakfast. Hanyuan Hotel also includes a very good
+restaurant, but unfortunately it is a bit on the pricier side.
 \begin{itemize}
 \item\textbf{Near the Hotel}\hspace{3mm}The Hanyuan hotel is
-located on the intersection of a big road (NingHang Road 宁杭公路)
+located at the intersection of a big road (NingHang Road 宁杭公路)
 and a smaller road (TongWei Road 童卫路). If you need a taxi to
-go to downtown, for example, it is probably the easies to hail
+go to Downtown Nanjing, for example, it is probably the easiest to hail
-one at the big street. An ATM machine is situated a few
+down a taxi at the big street. An ATM machine is situated a few
-minutes down the smaller TongWei Road.
+minutes down the smaller TongWei Road. If you want to take a
+walk in the evening, Xingyuan suggest a stroll through the
+Purple Mountain Area on the top-right in the map in
+Fig.~\ref{hotelmap}. This area is approximately a 15 minutes
+walk away from the hotel and contains for example the Sun Yat
+Sen memorial and the Linggu pagoda.
 \begin{center}
 \includegraphics[scale=0.45]{travel_guide/map1a.jpg}
-\end{center}
+\hspace{5mm}
-\end{itemize}
+\includegraphics[scale=0.43]{travel_guide/linggusu.jpg}
+\end{center}
+\item\textbf{Metro Stations Near the Hotel}\hspace{3mm}
+There are two metro stations near the hotel (Muxuyan and
+Xiamafang stations), which are pretty much the same distance
+from the hotel (see map in Fig~\ref{hotelmap}). Muxuyuan is
+easier to reach: just down TongWei Road and then turn left
+down the hill. The entrance of the metro is on the left-hand
+side. However it is not the most scenic route. More scenic is
+the walk to Xiamafang Metro Station through the campus of the
+Nanjing Agriculture University. Unfortunately the way is not
+so straightforward. If you are unfamiliar with the way, we
+suggest you walk to Muxuyuan station; once you followed some
+locals and know the way, go to Xiamafang station.
 \begin{figure}[p]
 \includegraphics[scale=0.45]{travel_guide/map2.jpg}
+\caption{Shops and restaurants in the vicinity of the hotel.
+A relatively large shopping area including a large supermarket
+(indicated with a red star)
+is near the Xiamafang metro station.\label{hotelmap}}
 \end{figure}
+\item\textbf{Shops and Restaurants Near the Hotel}\hspace{3mm}
+There is a very nice shopping area close to Xiamafang Metro
+Station. There is a wide selection of restaurants in this
+area including Xingyuan's favourite restaurant for having
+lunch on workdays
+\begin{center}
+\includegraphics[scale=0.05]{travel_guide/rest.jpg}
+\end{center}
+\noindent This area also contains a ``Mickey Mouse bakery'',
+which stocks pastries similar to ones you might find in a
+Western bakery (just in case you get bored of the baozi
+at breakfast in the hotel) and a pizza place in case you need
+to eat something different than Chinese.
+There is also a smaller shopping area in the ``middle'' of
+Tongwei road including some native restaurants, and also some
+restaurants on the opposite side of NingHang Road. A smaller
+supermarket is at the end of Tongwei Road and a bigger one
+in the Xiamafang area.
+\end{itemize}
+\section{Further Afield}
+If you take the metro, you are very quickly in the downtown
+area of Nanjing (see metro map in Fig.~\ref{metronanjing}).
+\begin{itemize}
+\item\textbf{Shopping}\hspace{3mm}
+The most serious shopping malls in Nanjing can be found in the
+area around Xinjiekou and Daxinggong metro stations (on Line~2).
+Especially in multi-brand shopping malls the shopping goes
+like this: You find something you like. You agree the prize
+with the shop-assistant. You get a piece of paper, which you
+need to take to a cashier nearby. You pay there, get another
+piece of paper, which you take back to the store, where you
+receive your goods. Another quirk of shopping in China is that
+when the sale says, for example, ``80\% off'', it is actually
+20\% off, meaning you pay 80\% of the original price.
+\item\textbf{Restaurants}\hspace{3mm}The most famous area
+for restaurants in Nanjing is near the Confucius Temple, which
+is near the Fuzimiao Metro Station on Line~3. There you
+can find traditional-style houses and enjoy indigenous foods.
+\item\textbf{Sight-Seeing}\hspace{3mm}Nanjing, being a former
+capital, possessed one of the most impressive city walls.
+Today you can see remainders at the North Gate near
+Zhonghuamen Mtro Station on Line~1. From the station follow
+the red line in the map below.
+\begin{center}
+\includegraphics[scale=0.8]{travel_guide/map3.jpg}
+\hspace{5mm}
+\includegraphics[scale=0.3]{travel_guide/gate.jpg}
+\end{center}
+\noindent There is also another substantial and impressive
+section of the remaining city visible very close to the hotel:
+Walk the NingHuan Road towards the city centre, once you
+traversed the river, bear right. You will see a rather
+tall wall build of grey stones.
+Another scenic spot is the Xuanwu Lake, dotted with several
+beautiful small islands and a good place to have a walk. You
+can reach the lake by taking exit Xuanwumen at Line~3.
+Xingyuan suggest the walk indicated red below.
+\begin{center}
+\includegraphics[scale=0.8]{travel_guide/map4.jpg}
+\end{center}
+\noindent
+The ultimate bird's-eye view of Nanjing you can have
+from the Zifeng Tower. For this you have to go to Guluo
+Metro Station on Line~1.
+\end{itemize}
 \section{Schedule of the Excursion\label{excursion}}
 On Wednesday afternoon there will be the traditional ITP
 excursion, this time to a Chinese garden in Yangzhou and to the
 \item We expect that the shuttle bus brings us back starting
 around 21:30 and we should be back in the hotel by 23:00.
 \end{itemize}
-\section{While being in Nanjing, Local Attractions}
-%% what is the downtown metro station?
 \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]
+\mbox{}\\[-15mm]
 \begin{tabular}[t]{@{}|@{\hspace{0.5mm}}L{\cw}@{\hspace{0.5mm}}|}
-\multicolumn{1}{c}{\textbf{Monday}}\\
+\multicolumn{1}{c}{\textbf{Monday (6th Floor)\smallskip}}\\
 \hline
 9:00 -- 10:00\smallskip\\
 Short Intro Session\smallskip\\
 M.~Moscato, C.~Munoz, A.~Smith\\
 Affine Arithmetic and Applications to Real-Number Proving\\
 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}}\\
+\multicolumn{1}{c}{\textbf{Tuesday (6th Floor)\smallskip}}\\
 \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\\
 \rotatebox{90}{
 \small
 \begin{tabular}[t]{@{} *{2}{c @{\hspace{4mm}}} @{}}
 \mbox{}\\[-20mm]
 \begin{tabular}[t]{|@{\hspace{0.5mm}}L{90mm}@{\hspace{0.5mm}}|}
-\multicolumn{1}{c}{\textbf{Wednesday}}\\
+\multicolumn{1}{c}{\textbf{Wednesday (6th Floor)\smallskip}}\\
 \hline
 9:00 -- 10:00\smallskip\\
 R.~Spadotti\\
 A Mechanized Theory of Regular Trees in Dependent Type
 Theory\smallskip\\
 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}}\\
+\multicolumn{1}{c}{\textbf{Thursday (6th Floor)\smallskip}}\\
 \hline
 9:00 -- 10:00 (chair: G.~Smolka)\smallskip\\
 B.~Fallenstein, R.~Kumar\\
 Proof-Producing Reflection for HOL, with an Application
 to Model Polymorphism\smallskip\\

changeset 274	42b793ea9897
parent 273	0500c07aed6e
child 275	f12df1a3ab0c