1089 O.~Kunčar, A.~Popescu\\ |
1089 O.~Kunčar, A.~Popescu\\ |
1090 A Consistent Foundation for Isabelle/HOL\\ |
1090 A Consistent Foundation for Isabelle/HOL\\ |
1091 \hline |
1091 \hline |
1092 \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\ |
1092 \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\ |
1093 \hline |
1093 \hline |
1094 10:20 -- 11:10 (chair: TBD)\smallskip\\ |
1094 10:20 -- 11:10 (chair: S.~Boulm\'e)\smallskip\\ |
1095 Z.~Paraskevopoulou \textit{et al}\\ |
1095 Z.~Paraskevopoulou \textit{et al}\\ |
1096 Foundational Property-Based Testing\smallskip\\ |
1096 Foundational Property-Based Testing\smallskip\\ |
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 |
1116 Formalization of Error-Correcting Codes: from Hamming to Modern Coding |
1116 Formalization of Error-Correcting Codes: from Hamming to Modern Coding |
1117 Theory\\ |
1117 Theory\\ |
1118 \hline |
1118 \hline |
1119 \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}30 mins coffee break}\\ |
1119 \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}30 mins coffee break}\\ |
1120 \hline |
1120 \hline |
1121 16:00 -- 17:00 (chair: TBD)\smallskip\\ |
1121 16:00 -- 17:00 (chair: G.~Malecha)\smallskip\\ |
1122 P.~Lammich\\ |
1122 P.~Lammich\\ |
1123 Refinement to Imperative/HOL\smallskip\\ |
1123 Refinement to Imperative/HOL\smallskip\\ |
1124 B.~Barras, C.~Tankink, E.~Tassi\\ |
1124 B.~Barras, C.~Tankink, E.~Tassi\\ |
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 -- 18:15 (chair: TBD)\smallskip\\ |
1130 17:15 -- 18:15 (chair: M.~Moscato)\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\smallskip\\ |
1133 Certified Proof Checker\smallskip\\ |
1134 A.~Anand, R.~Knepper\\ |
1134 A.~Anand, R.~Knepper\\ |
1135 ROSCoq: Robots Powered by Constructive Reals\\ |
1135 ROSCoq: Robots Powered by Constructive Reals\\ |