--- a/README	Wed Jul 17 10:33:19 2013 +0100
+++ b/README	Tue Jul 23 09:06:34 2013 +0200
@@ -29,4 +29,11 @@
 isabelle build -d . UTM
 isabelle make utm     -- creates the big session file
 
-isabelle make itp     -- creates paper
\ No newline at end of file
+isabelle make itp     -- creates paper
+
+
+
+============================
+ROOT setup
+
+isabelle build -d . Slides2
\ No newline at end of file

--- a/ROOT	Wed Jul 17 10:33:19 2013 +0100
+++ b/ROOT	Tue Jul 23 09:06:34 2013 +0200
@@ -25,4 +25,4 @@
 session Slides2 in Slides = UTM +
   options [document = pdf, document_output = "..", document_variants = "slides2"]
   theories
-    "Slides2"
\ No newline at end of file
+    "Slides2"

--- a/Slides/Slides2.thy	Wed Jul 17 10:33:19 2013 +0100
+++ b/Slides/Slides2.thy	Tue Jul 23 09:06:34 2013 +0200
@@ -11,10 +11,11 @@
 
 
 notation (latex output)
-  Cons ("_::_" [48,47] 48) and
+  Cons ("_::_" [48,47] 68) and
+  append ("_@_" [65, 64] 65) and
   Oc ("1") and
   Bk ("0") and
-  exponent ("_\<^bsup>_\<^esup>") and
+  exponent ("_\<^bsup>_\<^esup>" [107] 109) and
   inv_begin0 ("I\<^isub>0") and
   inv_begin1 ("I\<^isub>1") and
   inv_begin2 ("I\<^isub>2") and
@@ -86,38 +87,50 @@
   \frametitle{%
   \begin{tabular}{@ {}c@ {}}
   \\[-3mm]
-  \Large Reasoning about Turing Machines\\[-1mm] 
-  \Large and Low-Level Code\\[-3mm] 
+  {\fontsize{20}{20}\selectfont{}Mechanising Turing Machines and}\\[-2mm] 
+  {\fontsize{20}{20}\selectfont{}Computability Theory in Isabelle}\\[-3mm] 
   \end{tabular}}
   
-  \begin{center}
-   Christian Urban\\[1mm]
-  %%\small King's College London
-  \end{center}\bigskip
+  \bigskip\medskip\medskip
  
   \begin{center}
-  in cooperation with Jian Xu and Xingyuan Zhang
+  \begin{tabular}{c@ {\hspace{1cm}}c}
+  \includegraphics[scale=0.29]{jian.jpg}  &
+  \includegraphics[scale=0.034]{xingyuan.jpg} \\
+  Jian Xu & Xingyuan Zhang\\[-3mm]
+  \end{tabular}\\[3mm]
+  \small PLA University of Science and Technology
+  \end{center}
+
+  \begin{center}
+  Christian Urban\\[0mm]
+  \small King's College London
   \end{center}
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
 
+
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}[c]
-  \frametitle{A Trend in Verification}%
+  \frametitle{Why Turing Machines?}%
 
   \begin{itemize}
-  \item in the past:\\
-  \begin{quote}
-  model a problem mathematically and proof properties about the 
-  model
-  \end{quote}\bigskip
+  \item At the beginning, it was just a student project
+  about computability.\smallskip
 
-  \item needs elegance, is still very hard\bigskip\pause
+  \begin{center}
+  \begin{tabular}{c}
+  \includegraphics[scale=0.3]{boolos.jpg}\\[-2mm]
+  \footnotesize Computability and Logic (5th.~ed)\\[-2mm]
+  \footnotesize Boolos, Burgess and Jeffrey\\[2mm]
+  \end{tabular}
+  \end{center}
 
-  \item does not help with ensuring the correctness of running programs
+  \item found an inconsistency in the definition of halting computations
+  (Chap.~3 vs Chap.~8)
   \end{itemize}
 
   \end{frame}}
@@ -128,60 +141,23 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}[c]
-  \frametitle{A Trend in Verification}%
-
-  \begin{itemize}
-  \item make the specification executable (e.g.~Compcert)\bigskip\pause
-
-  you would expect the trend would be to for example model C, implement 
-  your programs in C and verify the programs written in C (e.g.~seL4) 
-  \end{itemize}
-
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-*}
-
-text_raw {*
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \mode<presentation>{
-  \begin{frame}[c]
-  \frametitle{A Trend in Verification}%
+  \frametitle{Some Previous Work}%
 
   \begin{itemize}
-  \item but actually people start to verify machine code directly
-  (e.g.~bignum arithmetic implemented in x86-64 -- 700 instructions)
-
-  \item CPU models exists, but the strategy is to use a small subset
-  which you use in your programs
+  \item Norrish formalised computability theory in HOL starting
+  from the lambda-calculus 
+  \begin{itemize}
+  \item \textcolor{gray}{for technical reasons we could not follow him}
+  \item \textcolor{gray}{some proofs use TMs (Wang tilings)}
   \end{itemize}
-
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-*}
-
-text_raw {*
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \mode<presentation>{
-  \begin{frame}[c]
-  \frametitle{Why Turing Machines}%
+ 
 
-  \begin{itemize}
-  \item at the beginning it was just a nice student project
-  about computability
 
-  \begin{center}
-  \includegraphics[scale=0.3]{boolos.jpg}
-  \end{center}
+  \bigskip
 
-  \item found an inconsistency in the definition of halting computations
-  (Chap.~3 vs Chap.~8)
-  \pause
-
-  \item \small Norrish formalised computability via lambda-calculus (and nominal);
-  Asperti and Riccioti formalised TMs but didn't get proper UTM
+  \item Asperti and Ricciotti formalised TMs in Matita
   \end{itemize}
 
-
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
@@ -193,7 +169,7 @@
   \frametitle{Turing Machines}%
 
   \begin{itemize}
-  \item tapes contain 0 or 1 only
+  \item tapes are lists and contain @{text 0}s or @{text 1}s only
 
   \begin{center}
 \begin{tikzpicture}[scale=1]
@@ -222,13 +198,39 @@
   \end{tikzpicture}
   \end{center}
 
-  \item steps function
+  \item @{text steps} function:
 
-  \begin{quote}
-  What does the tape look like after the TM has executed n steps?
+  \begin{quote}\rm
+  What does the TM claclulate after it has executed @{text n} steps?
   \end{quote}\pause
 
-  designate the 0-state as halting state and remain there forever
+  \item designate the @{text 0}-state as \"halting state\" and remain there 
+  forever, i.e.~have a @{text Nop}-action
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Register Machines}%
+
+  \begin{itemize}
+  \item instructions
+
+  \begin{center}
+  \begin{tabular}{rcl@ {\hspace{10mm}}l}
+  @{text "I"} & $::=$  & @{term "Inc R\<iota>"} & increment register @{text "R"} by one\\
+  & $\mid$ & @{term "Dec R\<iota> L\<iota>"} & if content of @{text R} is non-zero,\\
+  & & & then decrement it by one\\
+  & & & otherwise jump to instruction @{text L}\\
+  & $\mid$ & @{term "Goto L\<iota>"} & jump to instruction @{text L}
+  \end{tabular}
+  \end{center}
+
   \end{itemize}
 
   \end{frame}}
@@ -250,9 +252,9 @@
   \node [anchor=base] at (2.2,0.1) {\small$\Rightarrow$};
   \node [anchor=base] at (5.6,0.1) {\small$\Rightarrow$};
   \node [anchor=base] at (10.5,0.1) {\small$\Rightarrow$};
-  \node [anchor=base] at (2.2,-0.8) {\small$\overbrace{\text{cbegin}}^{}$};
-  \node [anchor=base] at (5.6,-0.8) {\small$\overbrace{\text{cloop}}^{}$};
-  \node [anchor=base] at (10.5,-0.8) {\small$\overbrace{\text{cend}}^{}$};
+  \node [anchor=base] at (2.2,-0.8) {\small$\overbrace{@{text cbegin}}^{}$};
+  \node [anchor=base] at (5.6,-0.8) {\small$\overbrace{@{text cloop}}^{}$};
+  \node [anchor=base] at (10.5,-0.8) {\small$\overbrace{@{text cend}}^{}$};
 
 
   \begin{scope}[shift={(0.5,0)}]
@@ -405,11 +407,13 @@
   \frametitle{Hoare Reasoning}%
 
   \begin{itemize}
-  \item reasoning is still quite difficult---invariants
+  \item reasoning is still quite demanding;\\
+  the invariants of the copy-machine:\\[-5mm]\mbox{}
 
   \footnotesize
   \begin{center}
-\begin{tabular}{@ {\hspace{-4mm}}lcl@ {\hspace{-0.9cm}}l@ {}}
+  \begin{tabular}{@ {\hspace{-5mm}}c@ {}}
+  \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {\hspace{-0.9cm}}l@ {}}
   \hline
   @{thm (lhs) inv_begin1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin1.simps} & (starting state)\\
   @{thm (lhs) inv_begin2.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin2.simps}\\
@@ -426,6 +430,7 @@
   @{thm (lhs) inv_end0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end0.simps} & (halting state)\smallskip\\
   \hline
   \end{tabular}
+  \end{tabular}
   \end{center}
 
   \end{itemize}
@@ -434,30 +439,7 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
 
-text_raw {*
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \mode<presentation>{
-  \begin{frame}[c]
-  \frametitle{Register Machines}%
 
-  \begin{itemize}
-  \item instructions
-
-  \begin{center}
-  \begin{tabular}{rcl@ {\hspace{10mm}}l}
-  @{text "I"} & $::=$  & @{term "Inc R\<iota>"} & increment register @{text "R"} by one\\
-  & $\mid$ & @{term "Dec R\<iota> L\<iota>"} & if content of @{text R} is non-zero,\\
-  & & & then decrement it by one\\
-  & & & otherwise jump to instruction @{text L}\\
-  & $\mid$ & @{term "Goto L\<iota>"} & jump to instruction @{text L}
-  \end{tabular}
-  \end{center}
-
-  \end{itemize}
-
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-*}
 
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -486,13 +468,13 @@
   \frametitle{Sizes}%
 
   \begin{itemize}
-  \item UF (size: 140843)
-  \item Register Machine (size: 2 Mio instructions)
-  \item UTM (size: 38 Mio states)
+  \item UF (size: @{text 140843})
+  \item Register Machine (size: @{text 2} Mio instructions)
+  \item UTM (size: @{text 38} Mio states)
   \end{itemize}\bigskip\bigskip
 
   \small
-  old version: RM (12 Mio) UTM (112 Mio)
+  old version: RM (@{text 12} Mio) UTM (@{text 112} Mio)
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}

Binary file Slides/document/jian.jpg has changed

Binary file slides2.pdf has changed