itp-2015: comparison booklet.tex

equal deleted inserted replaced

-:42f24df619f8
+:0500c07aed6e
 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.
 \begin{itemize}
-\item\textbf{Near the hotel}\hspace{3mm}The Hanyuan hotel is
+\item\textbf{Near the Hotel}\hspace{3mm}The Hanyuan hotel is
 located on 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
 one at the big street. An ATM machine is situated a few
 minutes down the smaller TongWei Road.
 for the Slender West Lake. We are going to enter the Slender West
 Lake area from its North Gate. The walking tour at Slender
 West Lake will be lead by two guides speaking English.
 Wiki has some rudimentary information at
 \url{https://en.wikipedia.org/wiki/Slender_West_Lake}.
-%\item After the walk, we will board boats which will bring
+\item After the walk, we will board boats which will bring
-%  us to the South Gate of the lake.
+us to the South Gate of the lake.
 \item The banquet restaurant (named Lion
 Pavilion) is located on the campus
 of Yangzhou University. It  will take us 5 minute walk
 from the South Gate to get there.
 \item We expect that the shuttle bus brings us back starting
 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\\
+16:00 -- 17:00 (chair:~H.~Herbelin)\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\\
 T.~Nipkow\\
 Amortized Complexity Verified\\
 \hline
 \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\
 \hline
-10:20 -- 11:10\smallskip\\
+10:20 -- 11:10 (chair: J.~Urban)\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
 L.~Birkedal\\
 \textbf{Invited Talk}\\
 \hline
 \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}2hs lunch break}\\
 \hline
-14:30 -- 15:30\smallskip\\
+14:30 -- 15:30 (chair: A.~Fox)\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\\
+16:00 -- 17:00 (chair: S.~Blazy)\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\\
 \begin{figure}[p]
 \begin{center}
 \rotatebox{90}{
 \small
 \begin{tabular}[t]{@{} *{2}{c @{\hspace{4mm}}} @{}}
-\mbox{}\\[-30mm]
+\mbox{}\\[-20mm]
 \begin{tabular}[t]{|@{\hspace{0.5mm}}L{90mm}@{\hspace{0.5mm}}|}
 \multicolumn{1}{c}{\textbf{Wednesday}}\\
 \hline
 9:00 -- 10:00\smallskip\\
 R.~Spadotti\\
 \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\\
+9:00 -- 10:00 (chair: G.~Smolka)\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\\
 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\\
+14:30 -- 15:30 (chair: C.~Wu)\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\\

changeset 273	0500c07aed6e
parent 272	42f24df619f8
child 274	42b793ea9897