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