diff -r 15b8fc34cb08 -r 5c283ecefda6 Slides/Slides6.thy
--- a/Slides/Slides6.thy	Wed Oct 02 13:17:32 2013 +0100
+++ b/Slides/Slides6.thy	Thu Oct 03 15:29:03 2013 +0100
@@ -1,5 +1,5 @@
 (*<*)
-theory Slides5
+theory Slides6
 imports "~~/src/HOL/Library/LaTeXsugar"
 begin
 
@@ -11,7 +11,7 @@
 
 
 text_raw {*
-  \renewcommand{\slidecaption}{London, 29 August 2012}
+  \renewcommand{\slidecaption}{London, 3 October 2013}
   \newcommand{\bl}[1]{\textcolor{blue}{#1}}                        
   \newcommand{\sout}[1]{\tikz[baseline=(X.base), inner sep=-0.1pt, outer sep=0pt]
   \node [cross out,red, ultra thick, draw] (X) {\textcolor{black}{#1}};}
@@ -21,8 +21,9 @@
   \frametitle{%
   \begin{tabular}{@ {}c@ {}}
   \\[-3mm]
-  \LARGE The Myhill-Nerode Theorem\\[-3mm] 
-  \LARGE in a Theorem Prover\\[0mm] 
+  \Large A Formalisation of the\\[-1mm] 
+  \Large Myhill-Nerode Theorem using\\[-1mm] 
+  \Large Regular Expressions only
   \end{tabular}}
   
   \begin{center}
@@ -35,11 +36,6 @@
   University of Science and Technology in Nanjing
   \end{center}
 
-  \only<2->{
-  \begin{textblock}{6}(9,5.3)
-  \alert{\bf Isabelle/HOL}
-  \end{textblock}}
-
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 *}
@@ -52,20 +48,15 @@
 
   \mbox{}\\[2mm]
   \begin{itemize}
-  \item my background is in 
-  \begin{itemize}
-  \item \normalsize programming languages and theorem provers
-  \item \normalsize develop Nominal Isabelle
-  \end{itemize}\bigskip\bigskip\bigskip\bigskip\bigskip  
+  \item my background is in: 
+    \begin{itemize}
+    \item \normalsize programming languages and 
+    \item \normalsize theorem provers
+    \end{itemize}\medskip
 
-  \item<1->to formalise and mechanically check proofs from 
-  programming language research, TCS \textcolor{gray}{and OS}\bigskip
-
-  \item<2->we found out that the variable convention can lead to
-  faulty proofs\ldots 
+  \item \normalsize develop Nominal Isabelle for reasoning about programming languages\\[-10mm]\mbox{}
   \end{itemize}
   
-  \onslide<2->{
   \begin{center}
   \begin{block}{}
   \color{gray}
@@ -73,145 +64,22 @@
   {\bf\mbox{}\hspace{-1.5mm}Variable Convention:}\\[0mm] 
   If $M_1,\ldots,M_n$ occur in a certain mathematical context
   (e.g. definition, proof), then in these terms all bound variables 
-  are chosen to be different from the free variables.\hfill Henk Barendregt
+  are chosen to be different from the free variables.\hfill ---Henk Barendregt
   \end{block}
-  \end{center}}
-
-
-  \only<1->{
-  \begin{textblock}{6}(10.9,3.5)
-  \includegraphics[scale=0.23]{isabelle1.png}
-  \end{textblock}}
-  
-
-
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-*}
-
-
-
-
-text_raw {*
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \mode<presentation>{
-  \begin{frame}[c]
-  \frametitle{}
+  \end{center}\pause
 
-  \begin{tabular}{c@ {\hspace{2mm}}c}
-  \\[6mm]
-  \begin{tabular}{c}
-  \includegraphics[scale=0.11]{harper.jpg}\\[-2mm]
-  {\footnotesize Bob Harper}\\[-2.5mm]
-  {\footnotesize (CMU)}
-  \end{tabular}
-  \begin{tabular}{c}
-  \includegraphics[scale=0.37]{pfenning.jpg}\\[-2mm]
-  {\footnotesize Frank Pfenning}\\[-2.5mm]
-  {\footnotesize (CMU)}
-  \end{tabular} &
+  \mbox{}\\[-19mm]\mbox{}
 
-  \begin{tabular}{p{6cm}}
-  \raggedright
-  \color{gray}{published a proof on LF in\\ {\bf ACM Transactions on Computational Logic}, 2005,
-  $\sim$31pp}
-  \end{tabular}\\
-
-  \pause
-  \\[0mm]
-  
-  \begin{tabular}{c}
-  \includegraphics[scale=0.36]{appel.jpg}\\[-2mm] 
-  {\footnotesize Andrew Appel}\\[-2.5mm]
-  {\footnotesize (Princeton)}
-  \end{tabular} &
-
-  \begin{tabular}{p{6cm}}
-  \raggedright
-  \color{gray}{relied on their proof in a\\ {\bf security} critical application\\ (proof-carrying code)}
-  \end{tabular}
-  \end{tabular}
-
-  
+  \begin{itemize}
+  \item found an error in an ACM journal paper by Bob Harper and Frank Pfenning 
+  about LF (and fixed it in three ways)
+  \end{itemize}
 
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
 
 
-
-text {*
-  \tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex]
-  \tikzstyle{node1}=[rectangle, minimum size=10mm, rounded corners=3mm, very thick, 
-                     draw=black!50, top color=white, bottom color=black!20]
-  \tikzstyle{node2}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick, 
-                     draw=red!70, top color=white, bottom color=red!50!black!20]
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \mode<presentation>{
-  \begin{frame}<2->[squeeze]
-  \frametitle{} 
-  
-  \begin{columns}
-  
-  \begin{column}{0.8\textwidth}
-  \begin{textblock}{0}(1,2)
-
-  \begin{tikzpicture}
-  \matrix[ampersand replacement=\&,column sep=7mm, row sep=5mm]
-  { \&[-10mm] 
-    \node (def1)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}}; \&
-    \node (proof1) [node1] {\large Proof}; \&
-    \node (alg1)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}}; \\
-    
-    \onslide<4->{\node {\begin{tabular}{c}\small 1st\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
-    \onslide<4->{\node (def2)   [node2] {\large Spec$^\text{+ex}$};} \&
-    \onslide<4->{\node (proof2) [node1] {\large Proof};} \&
-    \onslide<4->{\node (alg2)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\
-     
-    \onslide<5->{\node {\begin{tabular}{c}\small 2nd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
-    \onslide<5->{\node (def3)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&
-    \onslide<5->{\node (proof3) [node1] {\large Proof};} \&
-    \onslide<5->{\node (alg3)   [node2] {\large Alg$^\text{-ex}$};} \\
-
-    \onslide<6->{\node {\begin{tabular}{c}\small 3rd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
-    \onslide<6->{\node (def4)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&
-    \onslide<6->{\node (proof4) [node2] {\large\hspace{1mm}Proof\hspace{1mm}};} \&
-    \onslide<6->{\node (alg4)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\
-  };
-
-  \draw[->,black!50,line width=2mm] (proof1) -- (def1);
-  \draw[->,black!50,line width=2mm] (proof1) -- (alg1);
-  
-  \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (def2);}
-  \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (alg2);}
-
-  \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (def3);}
-  \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (alg3);}
-  
-  \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (def4);}
-  \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (alg4);}
-
-  \onslide<3->{\draw[white,line width=1mm] (1.1,3.2) -- (0.9,2.85) -- (1.1,2.35) -- (0.9,2.0);} 
-  \end{tikzpicture}
-
-  \end{textblock}
-  \end{column}
-  \end{columns}
-
-
-  \begin{textblock}{3}(12,3.6)
-  \onslide<4->{
-  \begin{tikzpicture}
-  \node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{2h};
-  \end{tikzpicture}}
-  \end{textblock}
-
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-
-*}
-
-
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
@@ -219,54 +87,18 @@
   \frametitle{}
 
   \begin{itemize}
-  \item I also found fixable errors in my Ph.D.-thesis about cut-elimination
+  \item found also fixable errors in my Ph.D.-thesis about cut-elimination
   (examined by Henk Barendregt and Andy Pitts)\bigskip
-  \item found flaws in a proof about a classic OS scheduling algorithm
-  --- helped us to implement\\ it correctly and ef$\!$ficiently\\ 
-  {\small\textcolor{gray}{(the existing literature ``proved'' 
-  correct an incorrect algorithm; used in the Mars Pathfinder mission)}}
-  \end{itemize}\bigskip\bigskip\pause
-
-
-  {\bf Conclusion:}\smallskip
-
-  Pencil-and-paper proofs in TCS are not foolproof, 
-  not even expertproof.
-
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-*}
-
-
-text_raw {*
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \mode<presentation>{
-  \begin{frame}[t]
 
-  \small Scott Aaronson (Berkeley/MIT):\\[-7mm]\mbox{}
-  \begin{center}
-  \begin{block}{}
-  \color{gray}
-  \small
-  ``I still remember having to grade hundreds of exams where the
-  students started out by assuming what had to be proved, or filled
-  page after page with gibberish in the hope that, somewhere in the
-  mess, they might accidentally have said something
-  correct. \ldots{}innumerable examples of ``parrot proofs'' ---
-  NP-completeness reductions done in the wrong direction, arguments
-  that look more like LSD trips than coherent chains of logic \ldots{}''
-  \end{block}
-  \end{center}\pause
+  \item formalised a classic OS scheduling algorithm (priority inversion 
+  protocol)
+    \begin{itemize}
+    \item original algorithm was incorrect even being proved correct (with `pencil-and-paper') 
+    \item helped us to implement this algorithm correctly and efficiently\\ 
+    \end{itemize}\bigskip\pause
 
-  \begin{tabular}{@ {}c@ {}}
-  Tobias Nipkow calls this the ``London Underground Phenomenon'':
-  \end{tabular}
-
-  \begin{center}
-  \begin{tabular}{ccc}
-  students & \;\;\raisebox{-8mm}{\includegraphics[scale=0.16]{gap.jpg}}\;\; & proofs
-  \end{tabular}
-  \end{center}
+  \item used Isabelle to prove properties about access controls and OSes
+  \end{itemize}
 
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
@@ -281,7 +113,7 @@
   \begin{textblock}{12.9}(1.5,2.0)
   \begin{block}{}
   \begin{minipage}{12.4cm}\raggedright
-  \large {\bf Motivation:}\\[2mm]I want to teach \alert{students} with
+  \large {\bf Motivation:}\\[2mm]I want to teach \alert{students} 
   theorem\\ provers (especially for inductions).
   \end{minipage}
   \end{block}
@@ -310,12 +142,12 @@
 
   \begin{textblock}{6}(2,4)
   \begin{tabular}{@ {}rrl}
-  \bl{r} & \bl{$::=$}  & \bl{$\varnothing$}\\
-         & \bl{$\mid$} & \bl{[]}\\
-         & \bl{$\mid$} & \bl{c}\\
-         & \bl{$\mid$} & \bl{r$_1$ $\cdot$ r$_2$}\\
-         & \bl{$\mid$} & \bl{r$_1$ + r$_2$}\\
-         & \bl{$\mid$} & \bl{r$^*$}\\
+  \bl{$r$} & \bl{$::=$}  & \bl{$\varnothing$}\\
+           & \bl{$\mid$} & \bl{$[]$}\\
+           & \bl{$\mid$} & \bl{$c$}\\
+           & \bl{$\mid$} & \bl{$r_1 \cdot r_2$}\\
+           & \bl{$\mid$} & \bl{$r_1 + r_2$}\\
+           & \bl{$\mid$} & \bl{$r^*$}\\
   \end{tabular}
   \end{textblock}
 
@@ -327,75 +159,226 @@
   \footnotesize Isabelle:
   \end{textblock}
 
-  \begin{textblock}{6}(7,12)
-  \footnotesize\textcolor{gray}{students have seen them and can be motivated about them}
-  \end{textblock}
-  
-  \end{frame}}
+   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
 
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
-  \begin{frame}<1->[t]
+  \begin{frame}<1-5>[t]
 
   \mbox{}\\[-2mm]
 
   \small
   \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}ll@ {}}
-  \bl{nullable ($\varnothing$)}            & \bl{$=$} & \bl{false} &\\
-  \bl{nullable ([])}           & \bl{$=$} & \bl{true}  &\\
-  \bl{nullable (c)}           & \bl{$=$} & \bl{false} &\\
-  \bl{nullable (r$_1$ + r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) $\vee$ (nullable r$_2$)} & \\ 
-  \bl{nullable (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) $\wedge$ (nullable r$_2$)} & \\
-  \bl{nullable (r$^*$)}          & \bl{$=$} & \bl{true} & \\
+  \bl{$nullable(\varnothing)$}   & \bl{$=$} & \bl{false} &\\
+  \bl{$nullable([])$}            & \bl{$=$} & \bl{true}  &\\
+  \bl{$nullable(c)$}             & \bl{$=$} & \bl{false} &\\
+  \bl{$nullable(r_1 + r_2)$}     & \bl{$=$} & \bl{$nullable(r_1) \vee nullable(r_2)$} & \\ 
+  \bl{$nullable(r_1 \cdot r_2)$} & \bl{$=$} & \bl{$nullable(r_1) \wedge nullable(r_2)$} & \\
+  \bl{$nullable(r^*)$}           & \bl{$=$} & \bl{true} & \\
   \end{tabular}\medskip\pause
 
   \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
-  \bl{der c ($\varnothing$)}            & \bl{$=$} & \bl{$\varnothing$} & \\
-  \bl{der c ([])}           & \bl{$=$} & \bl{$\varnothing$} & \\
-  \bl{der c (d)}           & \bl{$=$} & \bl{if c $=$ d then [] else $\varnothing$} & \\
-  \bl{der c (r$_1$ + r$_2$)} & \bl{$=$} & \bl{(der c r$_1$) + (der c r$_2$)} & \\
-  \bl{der c (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{((der c r$_1$) $\cdot$ r$_2$) + } & \\
-       &          & \bl{\hspace{3mm}(if nullable r$_1$ then der c r$_2$ else $\varnothing$)}\\
-  \bl{der c (r$^*$)}          & \bl{$=$} & \bl{(der c r) $\cdot$ (r$^*$)} &\smallskip\\\pause
+  \bl{$der\,c\,(\varnothing)$}            & \bl{$=$} & \bl{$\varnothing$} & \\
+  \bl{$der\,c\,([])$}            & \bl{$=$} & \bl{$\varnothing$} & \\
+  \bl{$der\,c\,(d)$}             & \bl{$=$} & \bl{if $c = d$ then $[]$ else $\varnothing$} & \\
+  \bl{$der\,c\,(r_1 + r_2)$}     & \bl{$=$} & \bl{$der\,c\,r_1 + der\,c\,r_2$} & \\
+  \bl{$der\,c\,(r_1 \cdot r_2)$} & \bl{$=$} &  \bl{if $nullable(r_1)$}\\
+  & & \bl{then $(der\,c\,r_1) \cdot r_2 + der\, c\, r_2$}\\ 
+  & & \bl{else $(der\, c\, r_1) \cdot r_2$}\\
+  \bl{$der\,c\,(r^*)$}          & \bl{$=$} & \bl{$(der\,c\,r) \cdot r^*$} &\smallskip\\\pause
 
-  \bl{derivative [] r}     & \bl{$=$} & \bl{r} & \\
-  \bl{derivative (c::s) r} & \bl{$=$} & \bl{derivative s (der c r)} & \\
+  \bl{$deriv\,[]\,r$}     & \bl{$=$} & \bl{$r$} & \\
+  \bl{$deriv\,(c::s)\,r$} & \bl{$=$} & \bl{$deriv\,s\,(der\,c\,r)$} & \\
   \end{tabular}\medskip
 
-  \bl{matches r s $=$ nullable (derivative s r)}
+  \bl{$match\,r\,s = nullable (deriv\,s\,r)$}
+
+  \only<4>{
+  \begin{textblock}{10.5}(2,5)
+  \begin{tikzpicture}
+  \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 
+{\normalsize\color{darkgray}
+  \begin{minipage}{10.5cm}
+  \begin{center}
+  a)\;\; \bl{$nullable(r) \Leftrightarrow ""\in {\cal L}(r)$}\medskip
+  \end{center}
+
+  \begin{center}
+  b)\;\; \bl{${\cal L}(der\,c\,r) = Der\,c\,({\cal L}(r))$}
+  \end{center}
+
+  where
+  \begin{center}
+  \bl{$Der\,c\,A \dn \{s\,|\, c\!::\!s \in A\}$}
+  \end{center}\medskip\pause
+
+  \begin{center}
+  c)\;\; \bl{$match\,r\,s \Leftrightarrow s\in{\cal L}(r)$}
+  \end{center}
+  \end{minipage}};
+  \end{tikzpicture}
+  \end{textblock}}
+
   
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
 
 text_raw {*
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \mode<presentation>{
-  \begin{frame}[c]
-  \frametitle{\LARGE Regular Expression Matching\\[-2mm] in Education}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[t]
+\frametitle{\begin{tabular}{c}\bl{$(a?\{n\}) \cdot a\{n\}$}\end{tabular}}
+
+\mbox{}\\[-13mm]
+
+\begin{tikzpicture}[y=.2cm, x=.3cm]
+ 	%axis
+	\draw (0,0) -- coordinate (x axis mid) (30,0);
+    	\draw (0,0) -- coordinate (y axis mid) (0,30);
+    	%ticks
+    	\foreach \x in {0,5,...,30}
+     		\draw (\x,1pt) -- (\x,-3pt)
+			node[anchor=north] {\x};
+    	\foreach \y in {0,5,...,30}
+     		\draw (1pt,\y) -- (-3pt,\y) 
+     			node[anchor=east] {\y}; 
+	%labels      
+	\node[below=0.6cm] at (x axis mid) {\bl{a}s};
+	\node[rotate=90, left=1.2cm] at (y axis mid) {secs};
 
-  \begin{itemize}
-  \item Harper in JFP'99: ``Functional Pearl: Proof- Directed Debugging''\medskip
-  \item Yi in JFP'06: ``Educational Pearl: `Proof-Directed Debugging' revisited 
-  for a first-order version''\medskip\bigskip\bigskip\pause
-  \item Owens et al in JFP'09: ``Regular-expression derivatives re-examined''
-  \bigskip
+	%plots
+	\draw[color=blue] plot[mark=*, mark options={fill=white}] 
+		file {re-python.data};
+	\draw[color=brown] plot[mark=pentagon*, mark options={fill=white} ] 
+		file {re-ruby.data};
+    
+	%legend
+	\begin{scope}[shift={(4,20)}] 
+	\draw[color=blue] (0,0) -- 
+		plot[mark=*, mark options={fill=white}] (0.25,0) -- (0.5,0) 
+		node[right]{\small Python};
+	\draw[yshift=-\baselineskip, color=brown] (0,0) -- 
+		plot[mark=pentagon*, mark options={fill=white}] (0.25,0) -- (0.5,0)
+		node[right]{\small Ruby};
+	\end{scope}
+\end{tikzpicture}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+*}
+
+text_raw {*
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[t]
+\frametitle{\begin{tabular}{c}\bl{$(a?\{n\}) \cdot a\{n\}$}\end{tabular}}
+
+\mbox{}\\[-13mm]
+
+\begin{tabular}{@ {\hspace{-5mm}}l}
+\begin{tikzpicture}[y=.2cm, x=.01cm]
+ 	%axis
+	\draw (0,0) -- coordinate (x axis mid) (1000,0);
+    	\draw (0,0) -- coordinate (y axis mid) (0,30);
+    	%ticks
+    	\foreach \x in {0,200,...,1000}
+     		\draw (\x,1pt) -- (\x,-3pt)
+			node[anchor=north] {\x};
+    	\foreach \y in {0,5,...,30}
+     		\draw (1pt,\y) -- (-3pt,\y) 
+     			node[anchor=east] {\y}; 
+	%labels      
+	\node[below=0.6cm] at (x axis mid) {\bl{a}s};
+	\node[rotate=90, left=1.2cm] at (y axis mid) {secs};
 
-  \begin{quote}\small
-  ``Unfortunately, regular expression derivatives have been lost in the 
-  sands of time, and few computer scientists are aware of them.''
-  \end{quote}
-  \end{itemize}
-  
+	%plots
+	\draw[color=blue] plot[mark=*, mark options={fill=white}] 
+		file {re-python.data};
+         \draw[color=green] plot[mark=square*, mark options={fill=white} ] 
+		file {re2c.data};
+         \draw[color=brown] plot[mark=pentagon*, mark options={fill=white} ] 
+		file {re-ruby.data};
+    
+	%legend
+	\begin{scope}[shift={(100,20)}] 
+	\draw[color=blue] (0,0) -- 
+		plot[mark=*, mark options={fill=white}] (0.25,0) -- (50,0) 
+		node[right]{\small Python};
+	\draw[yshift=-13, color=brown] (0,0) -- 
+		plot[mark=pentagon*, mark options={fill=white}] (0.25,0) -- (50,0)
+		node[right]{\small Ruby};
+	\draw[yshift=13, color=green] (0,0) -- 
+		plot[mark=square*, mark options={fill=white}] (0.25,0) -- (50,0)
+		node[right]{\small nullable + der};	
+	\end{scope}
+\end{tikzpicture}
+\end{tabular}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+*}
+
+text_raw{*
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[t]
+\frametitle{\begin{tabular}{c}\bl{$(a?\{n\}) \cdot a\{n\}$}\end{tabular}}
+
+\mbox{}\\[-9mm]
 
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+\begin{tabular}{@ {\hspace{-5mm}}l}
+\begin{tikzpicture}[y=.2cm, x=.0008cm]
+ 	%axis
+	\draw (0,0) -- coordinate (x axis mid) (12000,0);
+    	\draw (0,0) -- coordinate (y axis mid) (0,30);
+    	%ticks
+    	\foreach \x in {0,2000,...,12000}
+     		\draw (\x,1pt) -- (\x,-3pt)
+			node[anchor=north] {\x};
+    	\foreach \y in {0,5,...,30}
+     		\draw (1pt,\y) -- (-3pt,\y) 
+     			node[anchor=east] {\y}; 
+	%labels      
+	\node[below=0.6cm] at (x axis mid) {\bl{a}s};
+	\node[rotate=90, left=1.2cm] at (y axis mid) {secs};
 
+	%plots
+         \draw[color=green] plot[mark=square*, mark options={fill=white} ] 
+		file {re2b.data};
+	\draw[color=black] plot[mark=square*, mark options={fill=white} ] 
+		file {re3.data};	 
+        \draw[color=blue] plot[mark=*, mark options={fill=white}] 
+		file {re-python.data};
+         \draw[color=brown] plot[mark=pentagon*, mark options={fill=white} ] 
+		file {re-ruby.data};
+    
+	%legend
+	\begin{scope}[shift={(2000,20)}] 
+        \draw[color=blue] (0,0) -- 
+		plot[mark=*, mark options={fill=white}] (0.25,0) -- (50,0) 
+		node[right]{\small Python};
+	\draw[yshift=-13, color=brown] (0,0) -- 
+		plot[mark=pentagon*, mark options={fill=white}] (0.25,0) -- (50,0)
+		node[right]{\small Ruby};
+	\draw[yshift=13, color=green] (0,0) -- 
+		plot[mark=square*, mark options={fill=white}] (0.25,0) -- (50,0)
+		node[right]{\small nullable + der};	
+	\draw[yshift=26, color=black] (0,0) -- 
+		plot[mark=square*, mark options={fill=white}] (0.25,0) -- (50,0)
+		node[right]{\small nullable + der + simplification};	
+	\end{scope}
+\end{tikzpicture}
+\end{tabular}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
 *}
 
+
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
@@ -479,7 +462,7 @@
   \begin{block}{}
   \medskip
   \begin{minipage}{14cm}\raggedright
-  Problems with definition for regularity:\bigskip\\
+  Already problems with defining regularity:\bigskip\\
   \smath{\;\text{is\_regular}(A) \dn \exists M.\;\text{is\_dfa}(M) \wedge {\cal L} (M) = A}\bigskip
   \end{minipage}
   \end{block}
@@ -488,7 +471,7 @@
 
   \only<6->{\underline{A solution}:\;\;use \smath{\text{nat}}s \;@{text "\<Rightarrow>"}\; state nodes\medskip}
 
-  \only<7->{You have to \alert{rename} states!}
+  \only<7->{You have to \alert{rename} states apart!}
 
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
@@ -542,7 +525,7 @@
   
   {\noindent\large\bf\alert{\ldots{}and forget about automata}}\bigskip\bigskip\pause
 
-  Infrastructure for free. But do we lose anything?\medskip\pause
+  Reasoning infrastructure is for free. But do we lose anything?\medskip\pause
 
   \begin{minipage}{1.1\textwidth}
   \begin{itemize}
@@ -572,7 +555,7 @@
   \item provides necessary and suf\!ficient conditions\\ for a language 
   being regular\\ \textcolor{gray}{(pumping lemma only necessary)}\bigskip
 
-  \item key is the equivalence relation:\medskip
+  \item the key notion is the equivalence relation:\medskip
   \begin{center}
   \smath{x \approx_{A} y \,\dn\, \forall z.\; x @ z \in A \Leftrightarrow y @ z \in A}
   \end{center}
@@ -620,7 +603,7 @@
   \begin{tikzpicture}
   \node at (0,0) [shape border rotate=180,single arrow, fill=red,text=white, minimum height=2cm]
   {@{text "\<lbrakk>s\<rbrakk>"}$_{\approx_{A}}$};
-  \draw (0.9,-1.1) node {\begin{tabular}{l}an equivalence class\end{tabular}};
+  \draw (0.9,-1.1) node {\begin{tabular}{l}\;\;an equivalence class\end{tabular}};
   \end{tikzpicture}
   \end{textblock}}
 
@@ -702,7 +685,7 @@
   \mode<presentation>{
   \begin{frame}<-1>[c]
   \frametitle{\begin{tabular}{@ {}l}\LARGE% 
-  Transitions between Eq-Classes\end{tabular}}
+  Transitions\end{tabular}}
 
   \begin{center}
   \begin{tikzpicture}[scale=3]
@@ -1147,30 +1130,31 @@
   \textcolor{blue}{%
   \begin{center}
   \begin{tabular}{@ {}lc@ {\hspace{3mm}}l@ {}}
-  der c $\varnothing$     & $\dn$ & $\varnothing$\\
-  der c []                & $\dn$ & $\varnothing$\\
-  der c d                 & $\dn$ & if c $=$ d then [] else $\varnothing$\\
-  der c ($r_1 + r_2$)     & $\dn$ & (der c $r_1$) $+$ (der c $r_2$)\\
-  der c ($r^*$)       & $\dn$ & (der c $r$) $\cdot$ ($r^*$)\\
-  der c ($r_1 \cdot r_2$) & $\dn$ & ((der c $r_1$) $\cdot$ $r_2$) +\\
-                          &       & \hspace{-3mm}(if nullable $r_1$ then der c $r_2$ else $\varnothing$)\\
+  $der\,c\,\varnothing$     & $\dn$ & $\varnothing$\\
+  $der\,c\,[]$              & $\dn$ & $\varnothing$\\
+  $der\,c\,d$               & $\dn$ & if $c = d$ then $[]$ else $\varnothing$\\
+  $der\,c\,(r_1 + r_2)$     & $\dn$ & $der\,c\,r_1 + der\,c\,r_2$\\
+  $der\,c\,(r^*)$           & $\dn$ & $(der\,c\,r) \cdot r^*$\\
+  $der\,c\,(r_1 \cdot r_2)$ & $\dn$ &  \bl{if $nullable(r_1)$}\\
+  & & \bl{then $(der\,c\,r_1) \cdot r_2 + der\, c\, r_2$}\\ 
+  & & \bl{else $(der\, c\, r_1) \cdot r_2$}\\
   \end{tabular}
   \end{center}}}
 
   \only<2->{
-  \begin{textblock}{13}(1.5,5.7)
+  \begin{textblock}{14.1}(1.5,5.7)
   \begin{block}{}
   \begin{quote}
-  \begin{minipage}{13cm}\raggedright
+  \begin{minipage}{14.1cm}\raggedright\rm
   derivatives refine \smath{x \approx_{{\cal{L}}(r)} y}\bigskip
   \begin{center}
-  \only<2>{\mbox{\hspace{-22mm}}\smath{{\cal{L}}(\text{ders}~x~r) = {\cal{L}}(\text{ders}~y~r)
+  \only<2>{\mbox{\hspace{-22mm}}\smath{{\cal{L}}(deriv~x~r) = {\cal{L}}(deriv~y~r)
     \Longleftrightarrow x \approx_{{\cal{L}}(r)} y}}
-  \only<3>{\mbox{\hspace{-22mm}}\smath{\text{ders}~x~r = \text{ders}~y~r 
+  \only<3>{\mbox{\hspace{-22mm}}\smath{deriv~x~r = deriv~y~r 
    \Longrightarrow x \approx_{{\cal{L}}(r)} y}}
   \end{center}\bigskip
   \
-  \smath{\text{finite}(\text{ders}~A~r)}, but only modulo ACI
+  \smath{\text{finite}(deriv~A~r)}, but only modulo ACI
 
   \begin{center}
   \begin{tabular}{@ {\hspace{-10mm}}rcl}
@@ -1192,20 +1176,21 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}<2>[t]
-  \frametitle{\LARGE\begin{tabular}{c}Partial Derivatives of RExps\end{tabular}}
+  \frametitle{\LARGE\begin{tabular}{c}Partial Derivatives\end{tabular}}
 
  
   \only<2>{%
   \textcolor{blue}{%
   \begin{center}
   \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
-  pder c $\varnothing$     & $\dn$ & \alert{$\{\}$}\\
-  pder c []                & $\dn$ & \alert{$\{\}$}\\
-  pder c d                 & $\dn$ & if c $=$ d then $\{$[]$\}$ else $\{\}$\\
-  pder c ($r_1 + r_2$)     & $\dn$ & (pder c $r_1$) \alert{$\cup$} (der c $r_2$)\\
-  pder c ($r^\star$)       & $\dn$ & (pder c $r$) $\cdot$ $r^\star$\\
-  pder c ($r_1 \cdot r_2$) & $\dn$ & (pder c $r_1$) $\cdot$ $r_2$ \alert{$\cup$}\\
-                           &       & \hspace{-4mm}if nullable $r_1$ then (pder c $r_2$) else $\varnothing$\\
+  $pder\,c\,\varnothing$     & $\dn$ & \alert{$\{\}$}\\
+  $pder\,c\,[]$              & $\dn$ & \alert{$\{\}$}\\
+  $pder\,c\,d$               & $\dn$ & if $c = d$ then $\{[]\}$ else $\{\}$\\
+  $pder\,c\,(r_1 + r_2)$     & $\dn$ & $pder\,c\,r_1 \alert{\cup} pder\,c\,r_2$\\
+  $pder\,c\,(r^\star)$       & $\dn$ & $(pder\,c\,r) \cdot r^\star$\\
+  $pder\,c\,(r_1 \cdot r_2)$ & $\dn$ & \bl{if $nullable(r_1)$}\\
+  & & \bl{then $(pder\,c\,r_1) \cdot r_2 \alert{\cup} pder\, c\, r_2$}\\ 
+  & & \bl{else $(pder\, c\, r_1) \cdot r_2$}\\
   \end{tabular}
   \end{center}}}
 
@@ -1213,7 +1198,7 @@
   \begin{textblock}{6}(8.5,2.7)
   \begin{block}{}
   \begin{quote}
-  \begin{minipage}{6cm}\raggedright
+  \begin{minipage}{6cm}\rm\raggedright
   \begin{itemize}
   \item partial derivatives
   \item by Antimirov~'95
@@ -1237,11 +1222,13 @@
 
   \begin{itemize}
 
-  \item \alt<1>{\smath{\text{pders $x$ $r$ \mbox{$=$} pders $y$ $r$}}}
-            {\smath{\underbrace{\text{pders $x$ $r$ \mbox{$=$} pders $y$ $r$}}_{R}}} 
+  \item \alt<1>{\smath{\text{$pderiv\,x\,r = pderiv\,y\,r$}}}
+            {\smath{\underbrace{\text{$pderiv\,x\,r = pderiv\,y\,r$}}_{R}}} 
         refines \textcolor{blue}{$x$ $\approx_{{\cal L}(r)}$ $y$}\\[16mm]\pause
   \item \smath{\text{finite} (U\!N\!IV /\!/ R)} \bigskip\pause
-  \item Therefore \smath{\text{finite} (U\!N\!IV /\!/ \approx_{{\cal L}(r)})}. Qed.
+  \item Therefore \smath{\text{finite} (U\!N\!IV /\!/ \approx_{{\cal L}(r)})}. Qed.\bigskip\pause
+
+  \item We also gave a direct proof, but not as beautiful.
   \end{itemize}
   
   \only<2->{%
@@ -1310,51 +1297,6 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
 
-text_raw {*
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \mode<presentation>{
-  \begin{frame}[c]
-  \frametitle{\normalsize Formal language theory\ldots\hfill\mbox{}}
-
-  \begin{center}
-  \huge\bf\textcolor{gray}{in Nuprl}
-  \end{center}
-
-  \begin{itemize}
-  \item Constable, Jackson, Naumov, Uribe\medskip
-  \item \alert{18 months} for automata theory from Hopcroft \& Ullman chapters 1--11 (including Myhill-Nerode)
-  \end{itemize}
-
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-
-*}
-
-text_raw {*
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \mode<presentation>{
-  \begin{frame}[c]
-  \frametitle{\normalsize Formal language theory\ldots\hfill\mbox{}}
-
-  \begin{center}
-  \huge\bf\textcolor{gray}{in Coq}
-  \end{center}
-
-  \begin{itemize}
-  \item Filli\^atre, Briais, Braibant and others
-  \item multi-year effort; a number of results in automata theory, e.g.\medskip 
-    \begin{itemize}
-    \item Kleene's thm.~by Filli\^atre (\alert{``rather big''})
-    \item automata theory by Briais (5400 loc)
-    \item Braibant ATBR library, including Myhill-Nerode\\ ($>$7000 loc)
-    \item Mirkin's partial derivative automaton construction (10600 loc)
-    \end{itemize}
-  \end{itemize}
-
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-*}
-
 
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -1364,7 +1306,7 @@
 
   \begin{itemize}
   \item we have never seen a proof of Myhill-Nerode based on
-  regular expressions only\smallskip\pause
+  regular expressions\smallskip\pause
 
   \item great source of examples (inductions)\smallskip\pause
 
@@ -1374,9 +1316,24 @@
   \item second direction (400 / 390 loc)
   \end{itemize}
   
-  \item I am not saying automata are bad; just formal proofs about
-  them are quite dif$\!$ficult\pause\bigskip\medskip
+  \item I am not saying automata are bad; just proofs about
+  them are quite difficult in theorem provers\bigskip
+
+  \item \small our journal paper has just been accepted in JAR (see webpage)
+  \end{itemize}
 
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{\LARGE Future Work}
+
+  \begin{itemize}
+  \item regular expression sub-matching with derivatives (Martin Sulzmann PPDP'12)\bigskip 
   \item parsing with derivatives of grammars\\ (Matt Might ICFP'11)
   \end{itemize}
 
@@ -1387,43 +1344,8 @@
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
-  \begin{frame}[c]
-  \frametitle{\LARGE An Apology}
-
-  \begin{itemize}
-  \item This should all of course be done co-inductively
-  \end{itemize}
-
-  \footnotesize
-  \begin{tabular}{@ {\hspace{4mm}}l}
-  From: Jasmin Christian Blanchette\\
-  To: isabelle-dev@mailbroy.informatik.tu-muenchen.de\\
-  Subject: [isabelle-dev] NEWS\\
-  Date: \alert{\bf Tue, 28 Aug 2012} 17:40:55 +0200\\
-  \\
-  * {\bf HOL/Codatatype}: New (co)datatype package with support for mixed,\\
-  nested recursion and interesting non-free datatypes.\\
-  \\
-  * HOL/Ordinals\_and\_Cardinals: Theories of ordinals and cardinals\\
-  (supersedes the AFP entry of the same name).\\[2mm]
-  Kudos to Andrei and Dmitriy!\\
-  \\
-  Jasmin\\[-1mm]
-  ------------------------------------\\
-  isabelle-dev mailing list\\
-  isabelle-dev@in.tum.de\\
-  \end{tabular}
-
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-*}
-
-
-text_raw {*
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \mode<presentation>{
   \begin{frame}[b]
-  \frametitle{\mbox{}\\[2cm]\textcolor{red}{Thank you very much!\\[5mm]Questions?}}
+  \frametitle{\mbox{}\\[2cm]\textcolor{red}{Thank you very much\\ for listening!\\[5mm]Questions?}}
 
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%