--- 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