974 O.~Kunčar, A.~Popescu\\ |
974 O.~Kunčar, A.~Popescu\\ |
975 A Consistent Foundation for Isabelle/HOL\\ |
975 A Consistent Foundation for Isabelle/HOL\\ |
976 \hline |
976 \hline |
977 \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\ |
977 \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\ |
978 \hline |
978 \hline |
979 10:20 -- 11:10\smallskip\\ |
979 10:20 -- 11:10 (chair: TBD)\smallskip\\ |
980 Z.~Paraskevopoulou \textit{et al}\\ |
980 Z.~Paraskevopoulou \textit{et al}\\ |
981 Foundational Property-Based Testing\smallskip\\ |
981 Foundational Property-Based Testing\smallskip\\ |
982 C.~Kaliszyk, J.~Urban, J.~Vyskocil\\ |
982 C.~Kaliszyk, J.~Urban, J.~Vyskocil\\ |
983 Learning To Parse on Aligned Corpora (Rough Diamond)\\ |
983 Learning To Parse on Aligned Corpora (Rough Diamond)\\ |
984 \hline |
984 \hline |
985 \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\ |
985 \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\ |
986 \hline |
986 \hline |
987 11:30 -- 12:30\smallskip\\ |
987 11:30 -- 12:30 (chair: TBD)\smallskip\\ |
988 F.~Sieczkowski, A.~Bizjak, L.~Birkedal\\ |
988 F.~Sieczkowski, A.~Bizjak, L.~Birkedal\\ |
989 ModuRes: A Coq Library for Modular Reasoning about Concurrent Higher-Order Imperative Programming |
989 ModuRes: A Coq Library for Modular Reasoning about Concurrent Higher-Order Imperative Programming |
990 Languages\smallskip\\ |
990 Languages\smallskip\\ |
991 S.~Boulmé, A.~Maréchal\\ |
991 S.~Boulmé, A.~Maréchal\\ |
992 Refinement to Certify Abstract Interpretations, Illustrated |
992 Refinement to Certify Abstract Interpretations, Illustrated |
1001 Formalization of Error-Correcting Codes: from Hamming to Modern Coding |
1001 Formalization of Error-Correcting Codes: from Hamming to Modern Coding |
1002 Theory\\ |
1002 Theory\\ |
1003 \hline |
1003 \hline |
1004 \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}30 mins coffee break}\\ |
1004 \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}30 mins coffee break}\\ |
1005 \hline |
1005 \hline |
1006 16:00 -- 17:00\smallskip\\ |
1006 16:00 -- 17:00 (chair: TBD)\smallskip\\ |
1007 P.~Lammich\\ |
1007 P.~Lammich\\ |
1008 Refinement to Imperative/HOL\smallskip\\ |
1008 Refinement to Imperative/HOL\smallskip\\ |
1009 B.~Barras, C.~Tankink, E.~Tassi\\ |
1009 B.~Barras, C.~Tankink, E.~Tassi\\ |
1010 Asynchronous Processing of Coq Documents: |
1010 Asynchronous Processing of Coq Documents: |
1011 from the Kernel up to the User Interface\\ |
1011 from the Kernel up to the User Interface\\ |
1012 \hline |
1012 \hline |
1013 \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}short coffee break}\\ |
1013 \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}short coffee break}\\ |
1014 \hline |
1014 \hline |
1015 17:15 -- 17:45\smallskip\\ |
1015 17:15 -- 17:45 (chair: TBD)\smallskip\\ |
1016 L.~Cruz-Filipe, P.~Schneider-Kamp\\ |
1016 L.~Cruz-Filipe, P.~Schneider-Kamp\\ |
1017 Formalizing Size-Optimal Sorting Networks: Extracting a |
1017 Formalizing Size-Optimal Sorting Networks: Extracting a |
1018 Certified Proof Checker\\ |
1018 Certified Proof Checker\\ |
1019 \hline |
1019 \hline |
1020 \end{tabular} |
1020 \end{tabular} |