diff -r 7a6b87adebc8 -r 66ef2a2c64fb Slides/Slides6.thy
--- a/Slides/Slides6.thy	Wed Apr 13 13:44:25 2011 +0100
+++ b/Slides/Slides6.thy	Fri Apr 22 00:18:25 2011 +0800
@@ -12,7 +12,7 @@
 (*>*)
 
 text_raw {*
-  \renewcommand{\slidecaption}{Shanghai, 12.~April 2011}
+  \renewcommand{\slidecaption}{Hefei, 15.~April 2011}
 
   \newcommand{\abst}[2]{#1.#2}% atom-abstraction
   \newcommand{\pair}[2]{\langle #1,#2\rangle} % pairing
@@ -128,6 +128,23 @@
 *}
 
 
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{3 Points}
+  \large
+  \begin{itemize}
+  \item It is easy to make mistakes.\bigskip
+  \item Theorem provers can prevent mistakes, {\bf if} the problem
+  is formulated so that it is suitable for theorem provers.\bigskip
+  \item This re-formulation can be done, even in domains where
+  we do not expect it.
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
 
 text_raw {*
 
@@ -186,15 +203,12 @@
 
   \end{tabular}\medskip
 
-
-  
-
-
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 
 *}
 
+
 text_raw {*
 
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -333,7 +347,7 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}<1->[c]
-  \frametitle{Theorem Provers}
+  \frametitle{Lessons Learned}
 
   \begin{itemize}
   \item Theorem provers help with keeping large proofs consistent;
@@ -738,13 +752,13 @@
 
   \begin{textblock}{6}(9.5,6.18)
   \begin{flushright}
-  \color{gray}``derivative for a char'' 
+  \color{gray}``derivative w.r.t.~a char'' 
   \end{flushright}
   \end{textblock}
 
   \begin{textblock}{6}(9.5,12.1)
   \begin{flushright}
-  \color{gray}``deriv.~for a string'' 
+  \color{gray}``deriv.~w.r.t.~a string'' 
   \end{flushright}
   \end{textblock}
 
@@ -861,10 +875,10 @@
   \end{itemize}
 
 
-  I can think of two reasons why this is a good definition:\medskip
+  There are many reasons why this is a good definition:\medskip
   \begin{itemize}
   \item pumping lemma
-  \item closure properties of regular languages (closed under complement)
+  \item closure properties of regular languages\\ (e.g.~closure under complement)
   \end{itemize}
 
   \end{frame}}
@@ -909,6 +923,24 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}[c]
+  \frametitle{}
+  \large
+  \begin{center}
+  \begin{tabular}{p{9cm}}
+  My point:\bigskip\\
+
+  The theory about regular languages can be reformulated 
+  to be more suitable for theorem proving.
+  \end{tabular}
+  \end{center}
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
   \frametitle{\LARGE The Myhill-Nerode Theorem}
 
   \begin{itemize}
@@ -925,7 +957,6 @@
 
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-
 *}
 
 text_raw {*
@@ -1055,7 +1086,7 @@
   \smath{R_1}: & \smath{\{[]\}}\\
   \smath{R_2}: & \smath{\{[c]\}}\\
   \smath{R_3}: & \smath{U\!N\!IV - \{[], [c]\}}\\[6mm]
-  \multicolumn{2}{l}{\onslide<2->{\smath{X \stackrel{c}{\longrightarrow} Y \dn X ; [c] \subseteq Y}}}
+  \multicolumn{2}{l}{\onslide<2->{\smath{X \stackrel{c}{\longrightarrow} Y \dn X ;; [c] \subseteq Y}}}
   \end{tabular}
 
   \end{tabular}
@@ -1345,7 +1376,7 @@
   \begin{itemize}
   \item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_L) \;\Leftrightarrow\; L\; \text{is regular}}
   \bigskip\pause
-  \item regular languages are closed under complementation; this is easy
+  \item regular languages are closed under complementation; this is now easy\medskip
   \begin{center}
   \smath{U\!N\!IV /\!/ \approx_L \;\;=\;\; U\!N\!IV /\!/ \approx_{-L}}
   \end{center}
@@ -1423,7 +1454,7 @@
 
   \begin{itemize}
   \item We formalised the Myhill-Nerode theorem based on 
-  regular expressions (DFA are difficult to deal with in a theorem prover).\smallskip
+  regular expressions only (DFAs are difficult to deal with in a theorem prover).\smallskip
 
   \item Seems to be a common theme: algorithms need to be reformulated
   to better suit formal treatment.\smallskip
@@ -1432,7 +1463,7 @@
   implement the matcher directly inside the theorem prover
   (ongoing work).\smallskip
 
-  \item Parsing is a vast field and seems to offer new results. 
+  \item Parsing is a vast field which seem to offer new results. 
   \end{itemize}
 
   \end{frame}}
@@ -1450,23 +1481,126 @@
   \alert{\Large Questions?}
   \end{tabular}}
 
-  %\begin{center}
-  %\bf \underline{Short Bio:}
-  %\end{center}
-  %\mbox{}\\[-17mm]\mbox{}\small
-  %\begin{itemize}
-  %\item PhD in Cambridge
-  %\item Emmy-Noether Fellowship in Munich
-  %\item main results in nominal reasoning and nominal unification
-  %\end{itemize}
+  \begin{center}
+  \bf \underline{Short Bio:}
+  \end{center}
+  \mbox{}\\[-17mm]\mbox{}\small
+  \begin{itemize}
+  \item PhD in Cambridge
+  \item Emmy-Noether Research Fellowship at the TU Munich
+  \item talks at: CMU, Yale, Princeton, MIT,$\ldots$
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Future Research}
+
+  My existing strengths:\bigskip
+
+  \begin{itemize}
+  \item Isabelle (implementation)\bigskip
+  \item background in logic, programming languages, formal methods
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Future Research}
+
+  I want to have a single logic framework in which I can
+  write programs and prove their correctness.\bigskip
+
+  \begin{itemize}
+  \item extensions of HOL (IO, modules, advanced types)
+  \item high-level programming languages
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Future Research}
+
+  Compilers\bigskip
+
+  \begin{itemize}
+  \item the high-level language needs to be compiled to correct machine
+  code
+  \item compiler verification, machine code verification
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Future Research}
+
+  Stronger type-systems\bigskip
+
+  \begin{itemize}
+  \item ``correct by construction''
+  \item GADTs, dependent types
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Future Research}
+
+  Proof automation\bigskip
+
+  \begin{itemize}
+  \item external tools generate ``proof-certificates''
+  \item certificates are imported into Isabelle
+  \item GPU based external provers
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Future Research}
+
+  Large-scale applications\bigskip
+
+  \begin{itemize}
+  \item verification of Java-Script, Scala,$\ldots$
+  \item interesting code (INTEL in Shanghai)
+  \end{itemize}
 
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 *}
 
 
-
-
 (*<*)
 end
 (*>*)
\ No newline at end of file