equal
deleted
inserted
replaced
966 Diamond)\\ |
966 Diamond)\\ |
967 \hline |
967 \hline |
968 \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\ |
968 \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\ |
969 \hline |
969 \hline |
970 11:30 -- 12:30 (chair: R.~Thiemann)\smallskip\\ |
970 11:30 -- 12:30 (chair: R.~Thiemann)\smallskip\\ |
971 A.~Anand, R.~Knepper\\ |
971 (moved to Thursday)\\ |
972 ROSCoq: Robots Powered by Constructive Reals\smallskip\\ |
972 \smallskip\\ |
973 H.~Chan, M.~Norrish\\ |
973 H.~Chan, M.~Norrish\\ |
974 Mechanisation of AKS Algorithm: Part 1 – the Main Theorem\\ |
974 Mechanisation of AKS Algorithm: Part 1 – the Main Theorem\\ |
975 \hline |
975 \hline |
976 \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}2hs lunch break}\\ |
976 \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}2hs lunch break}\\ |
977 \hline |
977 \hline |
1097 C.~Kaliszyk, J.~Urban, J.~Vyskocil\\ |
1097 C.~Kaliszyk, J.~Urban, J.~Vyskocil\\ |
1098 Learning To Parse on Aligned Corpora (Rough Diamond)\\ |
1098 Learning To Parse on Aligned Corpora (Rough Diamond)\\ |
1099 \hline |
1099 \hline |
1100 \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\ |
1100 \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\ |
1101 \hline |
1101 \hline |
1102 11:30 -- 12:30 (chair: TBD)\smallskip\\ |
1102 11:30 -- 12:30 (chair: D.~Pichardie)\smallskip\\ |
1103 F.~Sieczkowski, A.~Bizjak, L.~Birkedal\\ |
1103 F.~Sieczkowski, A.~Bizjak, L.~Birkedal\\ |
1104 ModuRes: A Coq Library for Modular Reasoning about Concurrent Higher-Order Imperative Programming |
1104 ModuRes: A Coq Library for Modular Reasoning about Concurrent Higher-Order Imperative Programming |
1105 Languages\smallskip\\ |
1105 Languages\smallskip\\ |
1106 S.~Boulmé, A.~Maréchal\\ |
1106 S.~Boulmé, A.~Maréchal\\ |
1107 Refinement to Certify Abstract Interpretations, Illustrated |
1107 Refinement to Certify Abstract Interpretations, Illustrated |
1125 Asynchronous Processing of Coq Documents: |
1125 Asynchronous Processing of Coq Documents: |
1126 from the Kernel up to the User Interface\\ |
1126 from the Kernel up to the User Interface\\ |
1127 \hline |
1127 \hline |
1128 \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}short coffee break}\\ |
1128 \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}short coffee break}\\ |
1129 \hline |
1129 \hline |
1130 17:15 -- 17:45 (chair: TBD)\smallskip\\ |
1130 17:15 -- 18:15 (chair: TBD)\smallskip\\ |
1131 L.~Cruz-Filipe, P.~Schneider-Kamp\\ |
1131 L.~Cruz-Filipe, P.~Schneider-Kamp\\ |
1132 Formalizing Size-Optimal Sorting Networks: Extracting a |
1132 Formalizing Size-Optimal Sorting Networks: Extracting a |
1133 Certified Proof Checker\\ |
1133 Certified Proof Checker\smallskip\\ |
|
1134 A.~Anand, R.~Knepper\\ |
|
1135 ROSCoq: Robots Powered by Constructive Reals\\ |
1134 \hline |
1136 \hline |
1135 \end{tabular} |
1137 \end{tabular} |
1136 \end{tabular}} |
1138 \end{tabular}} |
1137 \end{center} |
1139 \end{center} |
1138 \end{figure} |
1140 \end{figure} |