booklet.tex
changeset 252 955b54dc16cc
parent 198 63c7c2c9e14a
child 257 69b5b4380046
equal deleted inserted replaced
246:803fa2e4993f 252:955b54dc16cc
     1 \documentclass[11pt]{report}
     1 \documentclass[11pt]{report}
       
     2 \usepackage{dina4}
     2 \usepackage{eurosym}
     3 \usepackage{eurosym}
     3 \usepackage{fontspec}
     4 \usepackage{fontspec}
     4 \usepackage[sc]{mathpazo}
     5 \usepackage[sc]{mathpazo}
     5 \setmainfont[Ligatures=TeX]{Palatino Linotype}
     6 \setmainfont[Ligatures=TeX]{Palatino Linotype}
       
     7 \usepackage{fancyvrb}
       
     8 \usepackage[table]{xcolor}
       
     9 \usepackage{floatpag}
       
    10 \floatpagestyle{empty}
       
    11 \definecolor{linkcolor}{rgb}{0,0,0.5}
       
    12 \usepackage[colorlinks=true,linkcolor=linkcolor,citecolor=linkcolor,filecolor=linkcolor,pagecolor=linkcolor,urlcolor=linkcolor]{hyperref}
     6 
    13 
     7 \def\xyzemail{xingyuanzhang at 126 dot com}
    14 \def\xyzemail{xingyuanzhang at 126 dot com}
     8 \def\cwemail{chunhanwu at 126 dot com} 
    15 \def\cwemail{chunhanwu at 126 dot com} 
     9  
    16  
    10    
    17    
   118 DOB, work address, e-mail and paper title (if you present a paper). 
   125 DOB, work address, e-mail and paper title (if you present a paper). 
   119 He will e-mail you the invitation letter. You might also need
   126 He will e-mail you the invitation letter. You might also need
   120 your hotel booking (see above) and flight details for the visa
   127 your hotel booking (see above) and flight details for the visa
   121 application.
   128 application.
   122 
   129 
   123 \chapter{Post-Arrival}
   130 
   124 
   131 
   125 TBD 
   132 \chapter{Arrival}
       
   133 
       
   134 Welcome in China. You made it to the airport. Unless your are
       
   135 one of the very few foreigners who can speak and read Chinese,
       
   136 potentially the most challenging part of your journey is about
       
   137 to begin. Below we explain how to get to Hanyuan Hotel in Nanjing
       
   138 from Shanghai Pudong Airport and from Nanjing Lukou Airport. If you
       
   139 arrive from somewhere else and need help, please let us know.
       
   140 
       
   141 China is generally a safe country for travelling, if the usual
       
   142 precautions are taken. We assume you have never been in China 
       
   143 before, therefore let us still start with some general points.
       
   144 
       
   145 \begin{itemize}
       
   146 \item \textbf{Weather}\hspace{3mm} 
       
   147 Unfortunately end of August is the time when it will be especially
       
   148 hot in Nanjing (over 30$^{\circ}$C). Be prepared with lots of
       
   149 light clothes, but do not forget a jumper, or sweater, since many
       
   150 places are air-conditioned. It can also rain.
       
   151 
       
   152 
       
   153 \item \textbf{Bottled water}\hspace{3mm}
       
   154 Whereas in many places it is safe to drink water from taps,
       
   155 do not take chances and drink only bottled water! During the
       
   156 conference we will provide bottled water. In other places you
       
   157 have to buy bottles yourself. Remember, Chinese are famous for
       
   158 nibbling on hot tea the whole day, even in sweltering 
       
   159 temperatures. There is a reason for this. 
       
   160 
       
   161 \item \textbf{Traffic}\hspace{3mm} 
       
   162 Do not even think of renting a car in China. Hence, while in
       
   163 China, you probably will be mostly going around on foot. Be
       
   164 careful though: You might come from a region where traffic rules are
       
   165 organised so that pedestrians are mostly
       
   166 treated with respect by all other road users, or even have an
       
   167 ``elevated status'' because they are considered the ``weakest''. 
       
   168 Traffic in China is, in contrast, organised more, shall we say, 
       
   169 according to a Darwinian model: Under no circumstance assume a
       
   170 car (or even a bicycle or the noiseless electric motor bikes) will stop for you. As pedestrian, you
       
   171 have to take care of everybody else. Therefore, whenever
       
   172 possible cross roads at traffic lights and even if the light
       
   173 shows green for you, look out for cars that pay no attention to this
       
   174 fact. Also, zebra crossings do \emph{not}, I repeat, \emph{do not} 
       
   175 have any special meaning in
       
   176 China for the road users higher up the traffic ladder
       
   177 (i.e.~bicycles and above). 
       
   178 Even if it sounds too funny, take
       
   179 our word and head this advice\ldots{}it might increase your
       
   180 life-expectancy. 
       
   181 
       
   182 \item \textbf{Free Public Wifi / Mobile Phones}\hspace{3mm}
       
   183 While free public wifi is nowadays pretty ubiquitous in big
       
   184 cities in China (Starbucks, Costas, McDonalds are obvious
       
   185 places where to find wifi), you need a working mobile phone in
       
   186 order to use it. You will have to register your number when
       
   187 you log in, and the wifi operator will then send you a
       
   188 password token via SMS. The problem is that chances are great
       
   189 your mobile phone will \emph{not} work in China. Therefore do
       
   190 not assume you can check information on the Internet while
       
   191 travelling. 
       
   192 
       
   193 At the hotel there will be wifi (with the super-secure
       
   194 password: 123456789). But again, do not assume you can
       
   195 download that last episode of the Daily Show: while bandwidth
       
   196 will generally be enough for reading email, be prepared for an
       
   197 uninterrupted stay in China, free from any disturbance coming
       
   198 from online demands.
       
   199    
       
   200 \item \textbf{Google etc}\hspace{3mm}There are two Great Walls in
       
   201 China: one prevents you from accessing Google, for example. Use
       
   202 \url{www.aol.com} or \url{www.bing.com} instead as your preferred
       
   203 search engine. Also, if you care about such things, set you 
       
   204 status on Facebook to ``unavailable'' for the period of time
       
   205 you will be in China. 
       
   206 
       
   207 \item \textbf{Map of Hotel}\hspace{3mm} test
       
   208 \end{itemize}
       
   209 
       
   210 \section{Travel from Nanjing Lukou Airport}
       
   211 
       
   212 \subsection{Taxi\label{nanjingtaxi}}
       
   213 
       
   214 \section{Travel from Shanghai Pudong Airport}
       
   215 
       
   216 Many of the participants will arrive at Shanghai Pudong
       
   217 Airport. From there, in short, you have to get to (1) the Hong
       
   218 Qiao railway station and then from there to (2) Nanjing Nan
       
   219 railway station. From Nanjing Nan, you can follow the
       
   220 suggestions in Section \ref{nanjingtaxi}. Overall this will
       
   221 take approximately 3h of travelling to the hotel. 
       
   222 
       
   223 \subsection*{From Shanghai Pudong Airport to Hong Qiao Train Station}
       
   224 
       
   225 For the first leg to Hong Qiao train station there are
       
   226 essentially two travel options: one recommended by locals
       
   227 and being the more sensible option is to take the airport bus;
       
   228 the other is by the World's only commercial Maglev train 
       
   229 and a change to the metro. 
       
   230 
       
   231 \begin{itemize}
       
   232 \item \textbf{Option 1 by Airport bus}: 
       
   233 
       
   234 At the Pudong Airport follow the signs for Airport Bus, or Airport
       
   235 Ring Bus. You have to take Line 1, which operates between 7:00
       
   236 and 23:00. The bus stop where you have to wait is 
       
   237 
       
   238 \begin{center}
       
   239 \begin{minipage}[t]{10cm}
       
   240 \mbox{\includegraphics{travel_guide/image005.jpg}}
       
   241 \end{minipage}
       
   242 \end{center}
       
   243 
       
   244 The waiting time is around 30 minutes ??? The ticket costs 30
       
   245 RMB (\euro{}4.25, \$5) and can be bought on the bus. This
       
   246 however requires cash. While you wait, be prepared to be
       
   247 harassed by taxi drivers, who insist on driving you to Hong Qiao
       
   248 train station. You can ignore them: it will cost you more,
       
   249 around 100 RMB; the bus is comfortable and air-conditioned,
       
   250 unlike the taxi; and, like the taxi driver, the bus driver
       
   251 already aims for maximum possible speed given good 
       
   252 road conditions. 
       
   253 
       
   254 
       
   255 The airport bus takes around 1h and makes only two stops at
       
   256 the very end of the journey. Both stops are in near
       
   257 proximity. You have to take the \emph{second} stop at Hong Qiao
       
   258 Railway Station. You will be able to see the big signs of
       
   259 Hong Qiao Railway Station when you approach the station. Do 
       
   260 not take the exit for Hong Qiao International Airport.
       
   261 
       
   262 \item \textbf{Option 2 Maglev train / Metro}: 
       
   263 Of course travelling on the Maglev is pretty cool\ldots{}
       
   264 reaching speeds of 415 km/h at certain(!) times of the day,
       
   265 namely 9:02--10:47 and 15:02--16:47. At other time it will 
       
   266 travel only at ``lame'' 300 km/h. Anyway, a
       
   267 ticket will set you back around 50 RMB (\euro{}7, \$8). The
       
   268 ticket can be paid in cash or credit card. To take this option 
       
   269 at the airport, you will need to follow the Maglev signs. The problem with
       
   270 this option, however, is that you can only go until ??? Then you have to
       
   271 change into the overcrowded metro line ??? The change to the
       
   272 metro is a short walk from the Maglev. You have to first buy a
       
   273 ticket at the metro station and then take Line ... The good thing
       
   274 about this option is that metro travelling in Shanghai is
       
   275 pretty easy for foreigners as all stations are signed out in letters. Overall
       
   276 the journey time of this option is also around 1h. So unless
       
   277 you really want to sample the feeling of travelling for 7
       
   278 minutes at 415 km/h, we recommend Option 1 by bus. 
       
   279 \end{itemize}
       
   280 
       
   281 \subsection*{From Hong Qiao Train Station to Nanjing Nan via
       
   282 High-Speed Train}
       
   283 
       
   284 The airport bus will stop directly in front of the southern
       
   285 part of the Hong Qiao train station. As background, train
       
   286 stations above the village level in China are organised more
       
   287 like an airport, than the sleepy train station you might be
       
   288 familiar with. Therefore you first have to go through a
       
   289 security gate where luggage is checked and you padded by a
       
   290 security guard. The security guard might be of either sex and
       
   291 this is seen as normal by Chinese. The entire check is done
       
   292 orderly, but appears to be only a token check and so
       
   293 fortunately is very speedy. 
       
   294 
       
   295 Next you need to buy a train ticket. There are ticket
       
   296 counters, see left below, signed out in the main hall. 
       
   297 
       
   298 \begin{center}
       
   299 \includegraphics[scale=0.8]{travel_guide/image038.jpg}
       
   300 \includegraphics[scale=0.8]{travel_guide/image040.jpg} 
       
   301 \end{center}
       
   302 
       
   303 \noindent You have to queue on the longer queue and buy a
       
   304 ticket for Nanjing Nan (Nan stands for South station). You
       
   305 will need to show your passport in order to buy a ticket. The
       
   306 ticket will cost around 135 RMB and looks like this:
       
   307 
       
   308 The G-Number (G42 above) stands for the train number. Then
       
   309 there is the coach number and seat number. The ticket above is
       
   310 for second class (-\ -). For the short duration of the trip
       
   311 there is no real need to buy a ticket for first class.
       
   312 
       
   313 Next you have to wait for your train on the main concourse of
       
   314 the station. On the main display the platform of your train
       
   315 will be displayed 30 minutes before departure. Assuming you
       
   316 have some time, rest for a moment and take in the atmosphere
       
   317 of a typical Chinese train station\ldots nothing like what you
       
   318 can experience, for example, at Clapham Junction during
       
   319 rush-hour.\footnote{Trivia, in case you did not know: Clapham Junction
       
   320 supposedly is the biggest train station in Europe in terms of
       
   321 passengers and rail tracks.}
       
   322 
       
   323 Once you know the platform, go to the gate. Be careful, the
       
   324 gates are nestled between the shops and might be easily
       
   325 overlooked. For each platform there are two gates labelled `A'
       
   326 and `B', respectively. `A' stands for the front of the train 
       
   327 and `B' for the rear -- you know which one to go from your 
       
   328 ticket.
   126 
   329 
   127 %weather, electrical connectors
   330 %weather, electrical connectors
   128 
   331 
       
   332 \newlength{\cw}
       
   333 \setlength{\cw}{100mm}
       
   334 \newcolumntype{L}[1]{>{\raggedright\let\newline\\\arraybackslash\hspace{0pt}}m{#1}}
       
   335 
       
   336 \begin{figure}[p]
       
   337 \begin{center}
       
   338 \rotatebox{90}{
       
   339 \small
       
   340 \begin{tabular}[t]{@{}*{2}{c @{\hspace{4mm}}} @{}}
       
   341  \mbox{}\\[-20mm]
       
   342  \begin{tabular}[t]{@{}|@{\hspace{0.5mm}}L{\cw}@{\hspace{0.5mm}}|}
       
   343   \multicolumn{1}{c}{\textbf{Monday}}\\
       
   344   \hline
       
   345   9:00 -- 10:00\smallskip\\
       
   346   Short Intro Session\smallskip\\
       
   347   M.~Moscato, C.~Munoz, A.~Smith\\
       
   348   Affine Arithmetic and Applications to Real-Number Proving\\
       
   349   \hline
       
   350   \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\
       
   351   \hline
       
   352   10:20 -- 11:10\smallskip\\
       
   353   J.~Hölzl, A.~Lochbihler, D.~Traytel\\ 
       
   354   A Formalized Hierarchy of Probabilistic System Types (Proof 
       
   355   Pearl)\smallskip\\
       
   356   F.~Immler\\ 
       
   357   A Verified Enclosure for the Lorenz Attractor (Rough 
       
   358   Diamond)\\
       
   359   \hline
       
   360   \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\
       
   361   \hline
       
   362   11:30 -- 12:30\smallskip\\
       
   363   A.~Anand, R.~Knepper\\ 
       
   364   ROSCoq: Robots Powered by Constructive Reals\smallskip\\
       
   365   H.~Chan, M.~Norrish\\
       
   366   Mechanisation of AKS Algorithm: Part 1 – the Main Theorem\\
       
   367   \hline
       
   368   \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}2hs lunch break}\\
       
   369   \hline
       
   370   14:30 -- 15:30\smallskip\\
       
   371   S.~Schneider, G.~Smolka, S.~Hack\\ 
       
   372   A First-Order Functional Intermediate Language for Verified 
       
   373   Compilers\smallskip\\
       
   374   A.~Fox\\ 
       
   375   Improved Tool Support for Machine-Code Decompilation in 
       
   376   HOL4\\
       
   377   \hline
       
   378   \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}30 mins coffee break}\\
       
   379   \hline
       
   380   16:00 -- 17:00\smallskip\\
       
   381   F.~Besson, S.~Blazy, P.~Wilke\\ 
       
   382   A Concrete Memory Model for CompCert\smallskip\\
       
   383   T.~Tuerk, M.~Myreen, R.~Kumar\\
       
   384   Pattern Matches in HOL: A New Representation and Improved Code 
       
   385   Generation\\
       
   386   \hline
       
   387   \end{tabular} 
       
   388 & \begin{tabular}[t]{|@{\hspace{0.5mm}}p{\cw}@{\hspace{0.5mm}}|}
       
   389   \multicolumn{1}{c}{\textbf{Tuesday}}\\
       
   390   \hline
       
   391   9:00 -- 10:00 (chair: M.~Norrish)\smallskip\\
       
   392   A.~Charguéraud, F.~Pottier\\
       
   393   Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find 
       
   394   Implementation\smallskip\\
       
   395   T.~Nipkow\\ 
       
   396   Amortized Complexity Verified\\
       
   397   \hline
       
   398   \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\
       
   399   \hline
       
   400   10:20 -- 11:10\smallskip\\
       
   401   S.~Blazy, D.~Demange, D.~Pichardie\\
       
   402   Validating Dominator Trees for a Fast, Verified Dominance 
       
   403   Test\smallskip\\
       
   404   A.~Lochbihler, A.~Maximova\\
       
   405   Stream Fusion for Isabelle’s Code Generator (Rough 
       
   406   Diamond)\\
       
   407   \hline
       
   408   \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\
       
   409   \hline
       
   410   11:30 -- 12:30 (chair: X.~Zhang)\smallskip\\
       
   411   L.~Birkedal\\
       
   412   \textbf{Invited Talk}\\
       
   413   \hline
       
   414   \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}2hs lunch break}\\
       
   415   \hline
       
   416   14:30 -- 15:30\smallskip\\
       
   417   M.~Abdulaziz, M.~Norrish, C.~Gretton\\
       
   418   Verified Over-Approximation of the Diameters of Propositionally Factored Transition 
       
   419   Systems\smallskip\\
       
   420   T.~Prathamesh\\
       
   421   Formalizing Knot Theory in Isabelle/HOL\\
       
   422   \hline
       
   423   \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}30 mins coffee break}\\
       
   424   \hline
       
   425   16:00 -- 17:00\smallskip\\
       
   426   S.~Schäfer, T.~Tebbi, G.~Smolka\\ 
       
   427   Autosubst: Reasoning with de Bruijn Terms and Parallel 
       
   428   Substitutions\smallskip\\
       
   429   P.~Maksimovic, A.~Schmitt\\
       
   430   HOCore in Coq\\
       
   431   \hline
       
   432   \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}short coffee break}\\
       
   433   \hline
       
   434   17:15 -- 18:00\smallskip\\
       
   435   \textbf{ITP Business Meeting}\\
       
   436   \hline
       
   437   \end{tabular}
       
   438 \end{tabular}}
       
   439 \end{center}
       
   440 \end{figure}
       
   441 
       
   442 \begin{figure}[p]
       
   443 \begin{center}
       
   444 \rotatebox{90}{
       
   445 \small
       
   446 \begin{tabular}[t]{@{} *{2}{c @{\hspace{4mm}}} @{}}
       
   447    \mbox{}\\[-30mm]
       
   448    \begin{tabular}[t]{|@{\hspace{0.5mm}}L{90mm}@{\hspace{0.5mm}}|}
       
   449       \multicolumn{1}{c}{\textbf{Wednesday}}\\
       
   450    \hline
       
   451    9:00 -- 10:00\smallskip\\
       
   452    R.~Spadotti\\
       
   453    A Mechanized Theory of Regular Trees in Dependent Type 
       
   454    Theory\smallskip\\
       
   455    G.~Smolka, S.~Schäfer, C.~Doczkal\\
       
   456    Transfinite Constructions in Classical Type Theory\\
       
   457    \hline
       
   458    \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}30 mins coffee break}\\
       
   459    \hline
       
   460    10:30 -- 11:30\\
       
   461    M.~Norrish\\
       
   462    \textbf{Invited Talk}\\
       
   463    \hline
       
   464    \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}1h Lunch break}\\
       
   465    \hline
       
   466    12:30 -- 21:30\smallskip\\
       
   467    Excursion to Ge Yuan Garden and Slender West Lake\smallskip\\
       
   468    Bus departs at 12:30 sharp from the hotel\smallskip\\
       
   469    Dinner will be at the Lion Pavilion restaurant which is close
       
   470    to the Slender West Lake\smallskip\\
       
   471    We expect to be back at the hotel around 22:30\\
       
   472    \hline
       
   473    \end{tabular}
       
   474  & \begin{tabular}[t]{|@{\hspace{0.5mm}}L{130mm}@{\hspace{0.5mm}}|@{}}
       
   475    \multicolumn{1}{c}{\textbf{Thursday}}\\
       
   476    \hline
       
   477    9:00 -- 10:00\smallskip\\
       
   478    B.~Fallenstein, R.~Kumar\\ 
       
   479    Proof-Producing Reflection for HOL, with an Application 
       
   480    to Model Polymorphism\smallskip\\ 
       
   481    O.~Kunčar, A.~Popescu\\ 
       
   482    A Consistent Foundation for Isabelle/HOL\\
       
   483    \hline
       
   484    \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\
       
   485    \hline
       
   486    10:20 -- 11:10\smallskip\\
       
   487    Z.~Paraskevopoulou \textit{et al}\\ 
       
   488    Foundational Property-Based Testing\smallskip\\
       
   489    C.~Kaliszyk, J.~Urban, J.~Vyskocil\\ 
       
   490    Learning To Parse on Aligned Corpora (Rough Diamond)\\
       
   491    \hline
       
   492    \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\
       
   493    \hline
       
   494    11:30 -- 12:30\smallskip\\
       
   495    F.~Sieczkowski, A.~Bizjak, L.~Birkedal\\ 
       
   496    ModuRes: A Coq Library for Modular Reasoning about Concurrent Higher-Order Imperative Programming 
       
   497    Languages\smallskip\\
       
   498    S.~Boulmé, A.~Maréchal\\
       
   499    Refinement to Certify Abstract Interpretations, Illustrated 
       
   500    on Linearization for Polyhedra\\
       
   501    \hline
       
   502    \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}2hs lunch break}\\
       
   503    \hline
       
   504    14:30 -- 15:30\smallskip\\
       
   505    C.~Sternagel, R.~Thiemann\\
       
   506    Deriving Comparators and Show-Functions in Isabelle/HOL\smallskip\\
       
   507    R.~Affeldt, J.~Garrigue\\
       
   508    Formalization of Error-correcting Codes: from Hamming to Modern Coding 
       
   509    Theory\\
       
   510    \hline
       
   511    \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}30 mins coffee break}\\
       
   512    \hline
       
   513    16:00 -- 17:00\smallskip\\
       
   514    P.~Lammich\\
       
   515    Refinement to Imperative/HOL\smallskip\\
       
   516    B.~Barras, C.~Tankink, E.~Tassi\\ 
       
   517    Asynchronous Processing of Coq Documents: 
       
   518    from the Kernel up to the User Interface\\
       
   519    \hline
       
   520    \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}short coffee break}\\
       
   521    \hline
       
   522    17:15 -- 17:45\smallskip\\
       
   523    L.~Cruz-Filipe, P.~Schneider-Kamp\\
       
   524    Formalizing Size-Optimal Sorting Networks: Extracting a 
       
   525    Certified Proof Checker\\
       
   526    \hline
       
   527    \end{tabular} 
       
   528 \end{tabular}}
       
   529 \end{center}
       
   530 \end{figure}
       
   531 
   129 \end{document}  
   532 \end{document}