\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}
%\usepackage{xeCJK}
%\setCJKmainfont[BoldFont=STZhongsong, ItalicFont=STKaiti]{STSong}
%\setCJKsansfont[BoldFont=STHeiti]{STXihei}
%\setCJKmonofont{STFangsong}
\def\xyzemail{xingyuanzhang at 126 dot com}
\def\cwemail{chunhanwu at 126 dot com}
\begin{document}
\title{\LARGE\bf ITP 2015 Conference Booklet}
\author{Xingyuan Zhang, Chunhan Wu and Christian Urban}
\date{\today}
%%\tableofcontents
\maketitle
\chapter{Pre-Arrival}
\section{Registration and Conference Fee}
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\\
(\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
piao} to reclaim the conference fee, you need to contact
Xingyuan directly before making any money transfer.
\medskip
\noindent The early conference fee is RMB 3300, which is
approximately \pounds{}350, \$533, or \euro{}488. It must be
transferred via bank transfer and must be made in your local
currency; we cannot accept any other form of payment. The
tutorials can be registered independently from the conference.
The conference fee includes lunches during the conference. It
also covers the excursion, the conference banquet and a
welcome reception.
\begin{center}
\begin{tabular}{l@{\hspace{4mm}}l}
Early conference fee until 31.~July: & RMB 3300\\
Late conference fee from 1.~August: & RMB 3800\bigskip\\
Additional banquet dinner and excursion: & RMB 530\\
(one is included in the conference fee)\bigskip\\
Isabelle tutorial (21 -- 23 August): & RMB 250\\
Coq tutorial (27 -- 29 August): & RMB 200\\
\end{tabular}
\end{center}
\noindent The amount payable needs to be
transferred to the account:
\begin{center}
\begin{tabular}{ll}
Account holder's name:& Zhang Xingyuan\medskip\\
Beneficiary bank:& BANK OF CHINA\medskip\\
Swift Code:& BKCHCNBJ940\medskip\\
Account number:& 504066588897\medskip\\
Beneficiary bank address:& Nanjing Mei Hua Shan Zhuang\\
& Sub-branch, Nanjing, China\medskip\\
Account holder's address:& \\
& Suite 2106, Building 20,\\
& 20 Biao Ying,\\
& Qinhuai District,\\
& Nanjing, Jiangsu Province,\\
& People's Republic of China.\\
\end{tabular}
\end{center}
\noindent {\bf Please make doubly-sure that your bank
transferral contains your full name as reference (additional
information field), and is in your local currency
(e.g.~\euro, \$, \pounds)!} Otherwise we will have no idea
where the money came from, and will not be able to receive
the money on our end. Please also make sure that your transferral
covers all bank fees.\bigskip
\section{Hotel Booking}
In short, you need to send your arrival and departure
details to Chunhan
(\cwemail).\bigskip
\noindent While it is possible to book the hotel via official
online travel web-pages, the price there is higher. The
easiest is to send Chunhan your name, arrival and departure
dates and he will send you back a booking ticket from Hanyuan
hotel, which you might need for your visa application.
You can pay the hotel when you arrive using Visa or
MasterCard.
\section{Visa}
Please be aware that for travelling to China you will need a
visa, for which you have to apply {\bf beforehand}. It often takes
one or two weeks before a visa is granted. Though if you
are prepared to pay a higher application fee, then you can
shorten the delay to a few days. For the visa you
will need an invitation letter, which Chunhan will send you
(\cwemail). You need to provide him with your name, title,
DOB, work address, e-mail and paper title (if you present a paper).
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{Arrival}
Welcome in China. You made it to the destination 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 (usually above 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 one of 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 your
status on Facebook to ``unavailable'' for the period of time
you will be in China. Ditto Twitter. If you do want to access
those services, you need a VPN back home.
\item \textbf{Map of Hotel / Taxis}\hspace{3mm} While more and
more young Chinese are exposed to English, you cannot
rely on anyone of the general public speaking more than a few
words. Rather, you have to always calculate with the very,
very likely scenario that nobody speaks any English and all
signs are written in characters that do not give you the
slightest idea what they are about. This means you always
have to prepare your travelling beforehand.
One part of every trip preparation should be to carry with you
a printed copy of the map where the Hanyuan Hotel is located
(see Fig.~\ref{hanyuan}). When you want to go to the hotel, you need to show the map to the
driver, since telling Hanyuan Hotel will most probably not be
understood and also the driver most likely does not know where
it is located. Showing the map will also guard against the
situation where a taxi driver cannot actually read the
address.\footnote{You might sneer at this. But remember: the
prime age of Chinese taxi drivers appears to be 50 plus. If
you can also remember, between 1966 and 1976 somebody had the
``great'' idea to be nasty to teachers (amonst others). So the
education these people were able to receive when their were
teens was rather rudimentary. Given that the ability of
reading Chinese characters takes years of arduous studying, it
is glaringly obvious that it is not their fault.}
\begin{figure}[p]
\begin{tabular}{l}
Address of Hanyuan Hotel:\medskip\\
%司机师傅，请将我送往``{\bf 童卫路20号翰苑宾馆}''，其位置如地图中红色A点所示。\\
%酒店电话：02584393962。谢谢！
\end{tabular}
\begin{center}
\makebox[0mm]{\includegraphics[scale=0.5]{travel_guide/badu.png}}
\end{center}
\caption{The location of the Hanyuan Hotel. Please print out!
\label{hanyuan}}
\end{figure}
\end{itemize}
\section{Travel from Nanjing Lukou Airport}
There are essentially three options depending on how frugal
or adventurous you want to be:
\begin{itemize}
\item The first option is to take a taxi for the whole journey
from the airport to the hotel. Follow the taxi signs at
the airport and take a yellow taxi. The journey will
cost you around 130 RMB (\euro{}19, \$21) and takes
about 45 minutes. Show the driver the map in
Fig.~\ref{hanyuan}. The taxi needs to be paid in cash.
\item A bit less expensive is going first by Metro Line S1
from the airport to Nanjing Nan Railway Station. The
metro will operate between 6:40 and 22:00. As you can
see below, Nanjing Nan will be the last stop with
Line~S1. At Nanjing Nan Railway Station you go to the
taxi stand, which is explained below, and take a taxi
from there. This option takes approximately 55 minutes
and costs 6 RMB for the metro ticket and around 36 RMB
for the taxi.
\item
\end{itemize}
\subsubsection*{Getting a Ticket for the Metro}
\subsubsection*{Taxi stations at Nanjing Lukou Airport and
Nanjing Nan Railway Station}
\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}
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 15 minutes during peak hours, or
30 minutes at other times.
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 times it will
travel only at mere speeds of 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.
The service of the Maglev
starts at 7:02 and finished the day at 21:42.
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 Longyang
Road Station and then have to
change into the overcrowded metro Line 2. 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 2. 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 around 2h. 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}