diff -r 371ff7ca8a05 -r adc5e4b511e7 booklet.tex
--- a/booklet.tex	Sat Aug 22 15:05:02 2015 +0800
+++ b/booklet.tex	Mon Aug 24 16:21:40 2015 +0800
@@ -939,8 +939,8 @@
   \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\
   \hline
   11:30 -- 12:30 (chair: R.~Thiemann)\smallskip\\
-  A.~Anand, R.~Knepper\\ 
-  ROSCoq: Robots Powered by Constructive Reals\smallskip\\
+  (moved to Thursday)\\ 
+  \smallskip\\
   H.~Chan, M.~Norrish\\
   Mechanisation of AKS Algorithm: Part 1 – the Main Theorem\\
   \hline
@@ -1070,7 +1070,7 @@
    \hline
    \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}20 mins coffee break}\\
    \hline
-   11:30 -- 12:30 (chair: TBD)\smallskip\\
+   11:30 -- 12:30 (chair: D.~Pichardie)\smallskip\\
    F.~Sieczkowski, A.~Bizjak, L.~Birkedal\\ 
    ModuRes: A Coq Library for Modular Reasoning about Concurrent Higher-Order Imperative Programming 
    Languages\smallskip\\
@@ -1098,10 +1098,12 @@
    \hline
    \multicolumn{1}{@{}|l|@{}}{\hspace{-1mm}\cellcolor{blue!20}short coffee break}\\
    \hline
-   17:15 -- 17:45 (chair: TBD)\smallskip\\
+   17:15 -- 18:15 (chair: TBD)\smallskip\\
    L.~Cruz-Filipe, P.~Schneider-Kamp\\
    Formalizing Size-Optimal Sorting Networks: Extracting a 
-   Certified Proof Checker\\
+   Certified Proof Checker\smallskip\\
+   A.~Anand, R.~Knepper\\ 
+   ROSCoq: Robots Powered by Constructive Reals\\
    \hline
    \end{tabular} 
 \end{tabular}}