nominal2: comparison Slides/Slides6.thy

equal deleted inserted replaced

-:7a6b87adebc8
+:66ef2a2c64fb
 Cons  ("_::/_" [66,65] 65)
 (*>*)
 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
 \newcommand{\susp}{{\boldsymbol{\cdot}}}% for suspensions
 \newcommand{\unit}{\langle\rangle}% unit
 \end{frame}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 *}
+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 {*
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \mode<presentation>{
 \color{gray}{relied on their proof in a safety critical system (proof carrying code)}
 \end{tabular}
 \end{tabular}\medskip
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
 text_raw {*
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \mode<presentation>{
 text_raw {*
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \mode<presentation>{
 \begin{frame}<1->[c]
-\frametitle{Theorem Provers}
+\frametitle{Lessons Learned}
 \begin{itemize}
 \item Theorem provers help with keeping large proofs consistent;
 make them modifiable.\medskip
 \end{flushright}
 \end{textblock}
 \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}
 \begin{textblock}{6}(9.5,13.98)
 \begin{flushright}
 \item A \alert{regular language} is one where there is a DFA that
 recognises it.\bigskip\pause
 \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}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 text_raw {*
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \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}
 \item provides necessary and suf\!ficient conditions for a language
 being regular (pumping lemma only necessary)\medskip
 \end{center}
 \end{itemize}
 \end{frame}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 *}
 text_raw {*
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \mode<presentation>{
 \multicolumn{2}{l}{\smath{U\!N\!IV /\!/\approx_L} produces}\\[4mm]
 \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}
 \end{frame}}
 \frametitle{\LARGE What Have We Achieved?}
 \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}
 \end{itemize}
 \begin{frame}[c]
 \frametitle{\LARGE Conclusion}
 \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
 \item The most interesting aspect is that we are able to
 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}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 *}
 \mbox{}\\[13mm]
 \alert{\LARGE Thank you very much!}\\
 \alert{\Large Questions?}
 \end{tabular}}
-%\begin{center}
+\begin{center}
-%\bf \underline{Short Bio:}
+\bf \underline{Short Bio:}
-%\end{center}
+\end{center}
-%\mbox{}\\[-17mm]\mbox{}\small
+\mbox{}\\[-17mm]\mbox{}\small
-%\begin{itemize}
+\begin{itemize}
-%\item PhD in Cambridge
+\item PhD in Cambridge
-%\item Emmy-Noether Fellowship in Munich
+\item Emmy-Noether Research Fellowship at the TU Munich
-%\item main results in nominal reasoning and nominal unification
+\item talks at: CMU, Yale, Princeton, MIT,$\ldots$
-%\end{itemize}
+\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
 (*>*)

changeset 2771	66ef2a2c64fb
parent 2764	03de62208942