709 is near the Fuzimiao Metro Station on Line~3. There you |
709 is near the Fuzimiao Metro Station on Line~3. There you |
710 can find traditional-style houses and enjoy indigenous foods. |
710 can find traditional-style houses and enjoy indigenous foods. |
711 There is also a myriad of restaurants in the Xinjiekou area. |
711 There is also a myriad of restaurants in the Xinjiekou area. |
712 |
712 |
713 \item\textbf{Sight-Seeing}\hspace{3mm}Nanjing, being a former |
713 \item\textbf{Sight-Seeing}\hspace{3mm}Nanjing, being a former |
714 capital, possessed one of the most impressive city walls. |
714 capital, possessed once one of the most impressive city walls. |
715 Today you can see remainders at the North Gate near |
715 Today you can see remainders at the North Gate near |
716 Zhonghuamen Metro Station on Line~1. From the station follow |
716 Zhonghuamen Metro Station on Line~1. From the station follow |
717 the red line in the map below. |
717 the red line in the map below. |
718 |
718 |
719 \begin{center} |
719 \begin{center} |
726 \noindent There is also another substantial section of the |
726 \noindent There is also another substantial section of the |
727 remaining city wall visible in an area very close to the hotel |
727 remaining city wall visible in an area very close to the hotel |
728 (you can see it from the hotel if you have a room sufficiently |
728 (you can see it from the hotel if you have a room sufficiently |
729 high up): Walk the Houbiaoying Road towards the city centre; |
729 high up): Walk the Houbiaoying Road towards the city centre; |
730 once you traversed the river, bear right. You will see a tall |
730 once you traversed the river, bear right. You will see a tall |
731 wall build of grey stones. |
731 wall build of grey stones. At the beginning it is a restored |
|
732 section, but further down the original wall starts (towards the |
|
733 top-end in the map below). |
732 |
734 |
733 \begin{center} |
735 \begin{center} |
734 \includegraphics[scale=0.4]{travel_guide/map5.jpg} |
736 \includegraphics[scale=0.4]{travel_guide/map5.jpg} |
735 \end{center} |
737 \end{center} |
736 |
738 |
737 Another scenic spot is the Xuanwu Lake, which is dotted with |
739 Another scenic spot in Nanjing is the Xuanwu Lake, which is |
738 several beautiful small islands and a good place to have a |
740 dotted with several beautiful small islands and a good place |
739 walk. You can reach the lake by going to Xuanwumen Metro |
741 to have a walk. You can reach the lake by going to Xuanwumen |
740 Station at Line~1. Xingyuan suggests the walk indicated red |
742 Metro Station at Line~1. Xingyuan suggests the walk indicated |
741 below where you leave from Jimingsi Station on Line~3. |
743 red below where you end up in from Jimingsi Station on Line~3. |
742 |
744 |
743 |
745 |
744 \begin{center} |
746 \begin{center} |
745 \includegraphics[scale=0.3]{travel_guide/map4.jpg} |
747 \includegraphics[scale=0.3]{travel_guide/map4.jpg} |
746 \hspace{5mm} |
748 \hspace{5mm} |
751 from the Zifeng Tower. For this you have to go to Guluo |
753 from the Zifeng Tower. For this you have to go to Guluo |
752 Metro Station on Line~1. According to Wiki, the Zifeng |
754 Metro Station on Line~1. According to Wiki, the Zifeng |
753 Tower is the 11th tallest building in the World (to |
755 Tower is the 11th tallest building in the World (to |
754 compare, the Shard in London is ranked 92nd and the Sears |
756 compare, the Shard in London is ranked 92nd and the Sears |
755 Tower in Chicago is 12th). A ticket for the observation |
757 Tower in Chicago is 12th). A ticket for the observation |
756 platform cost 66 RMB. |
758 platform costs 66 RMB. |
757 |
759 |
758 \end{itemize} |
760 \end{itemize} |
759 |
761 |
760 \section{Schedule of the Excursion\label{excursion}} |
762 \section{Schedule of the Excursion\label{excursion}} |
761 |
763 |
815 \begin{tabular}[t]{@{}*{2}{c @{\hspace{4mm}}} @{}} |
817 \begin{tabular}[t]{@{}*{2}{c @{\hspace{4mm}}} @{}} |
816 \mbox{}\\[-15mm] |
818 \mbox{}\\[-15mm] |
817 \begin{tabular}[t]{@{}|@{\hspace{0.5mm}}L{\cw}@{\hspace{0.5mm}}|} |
819 \begin{tabular}[t]{@{}|@{\hspace{0.5mm}}L{\cw}@{\hspace{0.5mm}}|} |
818 \multicolumn{1}{c}{\textbf{Monday (6th Floor)\smallskip}}\\ |
820 \multicolumn{1}{c}{\textbf{Monday (6th Floor)\smallskip}}\\ |
819 \hline |
821 \hline |
820 9:00 -- 10:00\smallskip\\ |
822 9:00 -- 10:00 (chairs: X.~Zhang, C.~Urban)\smallskip\\ |
821 Short Intro Session\smallskip\\ |
823 Short Intro Session\smallskip\\ |
822 M.~Moscato, C.~Munoz, A.~Smith\\ |
824 M.~Moscato, C.~Munoz, A.~Smith\\ |
823 Affine Arithmetic and Applications to Real-Number Proving\\ |
825 Affine Arithmetic and Applications to Real-Number Proving\\ |
824 \hline |
826 \hline |
825 \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\ |
827 \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\ |
826 \hline |
828 \hline |
827 10:20 -- 11:10\smallskip\\ |
829 10:20 -- 11:10 (chair: T.~Nipkow)\smallskip\\ |
828 J.~Hölzl, A.~Lochbihler, D.~Traytel\\ |
830 J.~Hölzl, A.~Lochbihler, D.~Traytel\\ |
829 A Formalized Hierarchy of Probabilistic System Types (Proof |
831 A Formalized Hierarchy of Probabilistic System Types (Proof |
830 Pearl)\smallskip\\ |
832 Pearl)\smallskip\\ |
831 F.~Immler\\ |
833 F.~Immler\\ |
832 A Verified Enclosure for the Lorenz Attractor (Rough |
834 A Verified Enclosure for the Lorenz Attractor (Rough |
833 Diamond)\\ |
835 Diamond)\\ |
834 \hline |
836 \hline |
835 \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\ |
837 \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\ |
836 \hline |
838 \hline |
837 11:30 -- 12:30\smallskip\\ |
839 11:30 -- 12:30 (chair: R.~Thiemann)\smallskip\\ |
838 A.~Anand, R.~Knepper\\ |
840 A.~Anand, R.~Knepper\\ |
839 ROSCoq: Robots Powered by Constructive Reals\smallskip\\ |
841 ROSCoq: Robots Powered by Constructive Reals\smallskip\\ |
840 H.~Chan, M.~Norrish\\ |
842 H.~Chan, M.~Norrish\\ |
841 Mechanisation of AKS Algorithm: Part 1 – the Main Theorem\\ |
843 Mechanisation of AKS Algorithm: Part 1 – the Main Theorem\\ |
842 \hline |
844 \hline |
843 \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}2hs lunch break}\\ |
845 \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}2hs lunch break}\\ |
844 \hline |
846 \hline |
845 14:30 -- 15:30\smallskip\\ |
847 14:30 -- 15:30 (chair: R.~Kumar)\smallskip\\ |
846 S.~Schneider, G.~Smolka, S.~Hack\\ |
848 S.~Schneider, G.~Smolka, S.~Hack\\ |
847 A First-Order Functional Intermediate Language for Verified |
849 A First-Order Functional Intermediate Language for Verified |
848 Compilers\smallskip\\ |
850 Compilers\smallskip\\ |
849 A.~Fox\\ |
851 A.~Fox\\ |
850 Improved Tool Support for Machine-Code Decompilation in |
852 Improved Tool Support for Machine-Code Decompilation in |
921 \begin{tabular}[t]{@{} *{2}{c @{\hspace{4mm}}} @{}} |
923 \begin{tabular}[t]{@{} *{2}{c @{\hspace{4mm}}} @{}} |
922 \mbox{}\\[-20mm] |
924 \mbox{}\\[-20mm] |
923 \begin{tabular}[t]{|@{\hspace{0.5mm}}L{90mm}@{\hspace{0.5mm}}|} |
925 \begin{tabular}[t]{|@{\hspace{0.5mm}}L{90mm}@{\hspace{0.5mm}}|} |
924 \multicolumn{1}{c}{\textbf{Wednesday (6th Floor)\smallskip}}\\ |
926 \multicolumn{1}{c}{\textbf{Wednesday (6th Floor)\smallskip}}\\ |
925 \hline |
927 \hline |
926 9:00 -- 10:00\smallskip\\ |
928 9:00 -- 10:00 (chair: A.~Charguéraud)\smallskip\\ |
927 R.~Spadotti\\ |
929 R.~Spadotti\\ |
928 A Mechanized Theory of Regular Trees in Dependent Type |
930 A Mechanized Theory of Regular Trees in Dependent Type |
929 Theory\smallskip\\ |
931 Theory\smallskip\\ |
930 G.~Smolka, S.~Schäfer, C.~Doczkal\\ |
932 G.~Smolka, S.~Schäfer, C.~Doczkal\\ |
931 Transfinite Constructions in Classical Type Theory\\ |
933 Transfinite Constructions in Classical Type Theory\\ |
932 \hline |
934 \hline |
933 \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}30 mins coffee break}\\ |
935 \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}30 mins coffee break}\\ |
934 \hline |
936 \hline |
935 10:30 -- 11:30\\ |
937 10:30 -- 11:30 (chair: C.~Urban)\\ |
936 M.~Norrish\\ |
938 M.~Norrish\\ |
937 \textbf{Invited Talk}\\ |
939 \textbf{Invited Talk}\\ |
938 \hline |
940 \hline |
939 \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}1h Lunch break}\\ |
941 \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}1h Lunch break}\\ |
940 \hline |
942 \hline |