
diff -r ccec33db31d4 -r 4457185b22ef Slides/Slides2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/Slides2.thy	Wed Jul 17 10:33:19 2013 +0100
@@ -0,0 +1,524 @@
+(*<*)
+theory Slides2
+imports "../thys/UTM" "../thys/Abacus_Defs"
+begin
+declare [[show_question_marks = false]]
+
+hide_const (open) s 
+
+abbreviation
+  "update2 p a \<equiv> update a p"
+
+
+notation (latex output)
+  Cons ("_::_" [48,47] 48) and
+  Oc ("1") and
+  Bk ("0") and
+  exponent ("_\<^bsup>_\<^esup>") and
+  inv_begin0 ("I\<^isub>0") and
+  inv_begin1 ("I\<^isub>1") and
+  inv_begin2 ("I\<^isub>2") and
+  inv_begin3 ("I\<^isub>3") and
+  inv_begin4 ("I\<^isub>4") and 
+  inv_begin ("I\<^bsub>cbegin\<^esub>") and
+  inv_loop1 ("J\<^isub>1") and
+  inv_loop0 ("J\<^isub>0") and
+  inv_end1 ("K\<^isub>1") and
+  inv_end0 ("K\<^isub>0")
+
+
+ 
+lemma inv_begin_print:
+  shows "s = 0 \<Longrightarrow> inv_begin n (s, tp) = inv_begin0 n tp" and
+        "s = 1 \<Longrightarrow> inv_begin n (s, tp) = inv_begin1 n tp" and 
+        "s = 2 \<Longrightarrow> inv_begin n (s, tp) = inv_begin2 n tp" and 
+        "s = 3 \<Longrightarrow> inv_begin n (s, tp) = inv_begin3 n tp" and 
+        "s = 4 \<Longrightarrow> inv_begin n (s, tp) = inv_begin4 n tp" and
+        "s \<notin> {0,1,2,3,4} \<Longrightarrow> inv_begin n (s, l, r) = False"
+apply(case_tac [!] tp)
+by (auto)
+
+
+lemma inv1: 
+  shows "0 < (n::nat) \<Longrightarrow> Turing_Hoare.assert_imp (inv_begin0 n) (inv_loop1 n)"
+unfolding Turing_Hoare.assert_imp_def
+unfolding inv_loop1.simps inv_begin0.simps
+apply(auto)
+apply(rule_tac x="1" in exI)
+apply(auto simp add: replicate.simps)
+done
+
+lemma inv2: 
+  shows "0 < n \<Longrightarrow> inv_loop0 n = inv_end1 n"
+apply(rule ext)
+apply(case_tac x)
+apply(simp add: inv_end1.simps)
+done
+
+
+lemma measure_begin_print:
+  shows "s = 2 \<Longrightarrow> measure_begin_step (s, l, r) = length r" and
+        "s = 3 \<Longrightarrow> measure_begin_step (s, l, r) = (if r = [] \<or> r = [Bk] then 1 else 0)" and
+        "s = 4 \<Longrightarrow> measure_begin_step (s, l, r) = length l" and 
+        "s \<notin> {2,3,4} \<Longrightarrow> measure_begin_step (s, l, r) = 0"
+by (simp_all)
+
+lemma inv_begin01:
+  assumes "n > 1"
+  shows "inv_begin0 n (l, r) = (n > 1 \<and> (l, r) = (Oc \<up> (n - 2), [Oc, Oc, Bk, Oc]))"
+using assms by auto                          
+
+lemma inv_begin02:
+  assumes "n = 1"
+  shows "inv_begin0 n (l, r) = (n = 1 \<and> (l, r) = ([], [Bk, Oc, Bk, Oc]))"
+using assms by auto
+
+(*>*)
+
+
+
+text_raw {*
+  \renewcommand{\slidecaption}{ITP, 24 July 2013}
+  \newcommand{\bl}[1]{#1}                        
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}
+  \frametitle{%
+  \begin{tabular}{@ {}c@ {}}
+  \\[-3mm]
+  \Large Reasoning about Turing Machines\\[-1mm] 
+  \Large and Low-Level Code\\[-3mm] 
+  \end{tabular}}
+  
+  \begin{center}
+   Christian Urban\\[1mm]
+  %%\small King's College London
+  \end{center}\bigskip
+ 
+  \begin{center}
+  in cooperation with Jian Xu and Xingyuan Zhang
+  \end{center}
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{A Trend in Verification}%
+
+  \begin{itemize}
+  \item in the past:\\
+  \begin{quote}
+  model a problem mathematically and proof properties about the 
+  model
+  \end{quote}\bigskip
+
+  \item needs elegance, is still very hard\bigskip\pause
+
+  \item does not help with ensuring the correctness of running programs
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \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}%
+
+  \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
+  \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}
+
+  \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
+  \end{itemize}
+
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Turing Machines}%
+
+  \begin{itemize}
+  \item tapes contain 0 or 1 only
+
+  \begin{center}
+\begin{tikzpicture}[scale=1]
+  \draw[very thick] (-3.0,0)   -- ( 3.0,0);
+  \draw[very thick] (-3.0,0.5) -- ( 3.0,0.5);
+  \draw[very thick] (-0.25,0)   -- (-0.25,0.5);
+  \draw[very thick] ( 0.25,0)   -- ( 0.25,0.5);
+  \draw[very thick] (-0.75,0)   -- (-0.75,0.5);
+  \draw[very thick] ( 0.75,0)   -- ( 0.75,0.5);
+  \draw[very thick] (-1.25,0)   -- (-1.25,0.5);
+  \draw[very thick] ( 1.25,0)   -- ( 1.25,0.5);
+  \draw[very thick] (-1.75,0)   -- (-1.75,0.5);
+  \draw[very thick] ( 1.75,0)   -- ( 1.75,0.5);
+  \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
+  \draw[fill]     (1.35,0.1) rectangle (1.65,0.4);
+  \draw[fill]     (0.85,0.1) rectangle (1.15,0.4);
+  \draw[fill]     (-0.35,0.1) rectangle (-0.65,0.4);
+  \draw[fill]     (-1.65,0.1) rectangle (-1.35,0.4);
+  \draw (-0.25,0.8) -- (-0.25,-0.8);
+  \draw[<->] (-1.25,-0.7) -- (0.75,-0.7);
+  \node [anchor=base] at (-0.85,-0.5) {\small left list\;\;\;\;\mbox{}};
+  \node [anchor=base] at (0.40,-0.5) {\small \mbox{}\;\;\;\;right list};
+  \node [anchor=base] at (0.1,0.7) {\small \;\;head};
+  \node [anchor=base] at (-2.2,0.2) {\ldots};
+  \node [anchor=base] at ( 2.3,0.2) {\ldots};
+  \end{tikzpicture}
+  \end{center}
+
+  \item steps function
+
+  \begin{quote}
+  What does the tape look like after the TM has executed n steps?
+  \end{quote}\pause
+
+  designate the 0-state as halting state and remain there forever
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Copy Turing Machines}%
+
+  \begin{itemize}
+  \item TM that copies a number on the input tape
+
+
+  \begin{center}
+\begin{tikzpicture}[scale=0.7]
+  \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}}^{}$};
+
+
+  \begin{scope}[shift={(0.5,0)}]
+  \draw[very thick] (-0.25,0)   -- ( 1.25,0);
+  \draw[very thick] (-0.25,0.5) -- ( 1.25,0.5);
+  \draw[very thick] (-0.25,0)   -- (-0.25,0.5);
+  \draw[very thick] ( 0.25,0)   -- ( 0.25,0.5);
+  \draw[very thick] ( 0.75,0)   -- ( 0.75,0.5);
+  \draw[very thick] ( 1.25,0)   -- ( 1.25,0.5);
+  \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
+  \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);
+  \draw[fill]     ( 0.35,0.1) rectangle (0.65,0.4);
+  \draw[fill]     ( 0.85,0.1) rectangle (1.15,0.4);
+  \end{scope}
+
+  \begin{scope}[shift={(2.9,0)}]
+  \draw[very thick] (-0.25,0)   -- ( 2.25,0);
+  \draw[very thick] (-0.25,0.5) -- ( 2.25,0.5);
+  \draw[very thick] (-0.25,0)   -- (-0.25,0.5);
+  \draw[very thick] ( 0.25,0)   -- ( 0.25,0.5);
+  \draw[very thick] ( 0.75,0)   -- ( 0.75,0.5);
+  \draw[very thick] ( 1.25,0)   -- ( 1.25,0.5);
+  \draw[very thick] ( 1.75,0)   -- ( 1.75,0.5);
+  \draw[very thick] ( 2.25,0)   -- ( 2.25,0.5);
+  \draw[rounded corners=1mm] (0.15,-0.1) rectangle (0.85,0.6);
+  \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);
+  \draw[fill]     ( 0.35,0.1) rectangle (0.65,0.4);
+  \draw[fill]     ( 0.85,0.1) rectangle (1.15,0.4);
+  \draw[fill]     ( 1.85,0.1) rectangle (2.15,0.4);
+  \end{scope}
+
+  \begin{scope}[shift={(6.8,0)}]
+  \draw[very thick] (-0.75,0)   -- ( 3.25,0);
+  \draw[very thick] (-0.75,0.5) -- ( 3.25,0.5);
+  \draw[very thick] (-0.75,0)   -- (-0.75,0.5);
+  \draw[very thick] (-0.25,0)   -- (-0.25,0.5);
+  \draw[very thick] ( 0.25,0)   -- ( 0.25,0.5);
+  \draw[very thick] ( 0.75,0)   -- ( 0.75,0.5);
+  \draw[very thick] ( 1.25,0)   -- ( 1.25,0.5);
+  \draw[very thick] ( 1.75,0)   -- ( 1.75,0.5);
+  \draw[very thick] ( 2.25,0)   -- ( 2.25,0.5);
+  \draw[very thick] ( 2.75,0)   -- ( 2.75,0.5);
+  \draw[very thick] ( 3.25,0)   -- ( 3.25,0.5);
+  \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
+  \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);
+  \draw[fill]     ( 2.35,0.1) rectangle (2.65,0.4);
+  \draw[fill]     ( 2.85,0.1) rectangle (3.15,0.4);
+  \draw[fill]     ( 1.85,0.1) rectangle (2.15,0.4);
+  \end{scope}
+
+  \begin{scope}[shift={(11.7,0)}]
+  \draw[very thick] (-0.75,0)   -- ( 3.25,0);
+  \draw[very thick] (-0.75,0.5) -- ( 3.25,0.5);
+  \draw[very thick] (-0.75,0)   -- (-0.75,0.5);
+  \draw[very thick] (-0.25,0)   -- (-0.25,0.5);
+  \draw[very thick] ( 0.25,0)   -- ( 0.25,0.5);
+  \draw[very thick] ( 0.75,0)   -- ( 0.75,0.5);
+  \draw[very thick] ( 1.25,0)   -- ( 1.25,0.5);
+  \draw[very thick] ( 1.75,0)   -- ( 1.75,0.5);
+  \draw[very thick] ( 2.25,0)   -- ( 2.25,0.5);
+  \draw[very thick] ( 2.75,0)   -- ( 2.75,0.5);
+  \draw[very thick] ( 3.25,0)   -- ( 3.25,0.5);
+  \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
+  \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);
+  \draw[fill]     ( 2.35,0.1) rectangle (2.65,0.4);
+  \draw[fill]     ( 2.85,0.1) rectangle (3.15,0.4);
+  \draw[fill]     ( 1.85,0.1) rectangle (2.15,0.4);
+  \draw[fill]     ( 0.35,0.1) rectangle (0.65,0.4);
+  \draw[fill]     ( 0.85,0.1) rectangle (1.15,0.4);
+  \end{scope}
+  \end{tikzpicture}
+  \end{center}\bigskip
+
+  \footnotesize
+  \begin{center}
+  \begin{tabular}{@ {\hspace{-8mm}}c@ {\hspace{2mm}}c@ {\hspace{2mm}}c}
+  \begin{tabular}[t]{@ {}l@ {}}
+  @{text cbegin} @{text "\<equiv>"}\\
+  \hspace{2mm}@{text "["}@{text "(W\<^bsub>0\<^esub>, 0), (R, 2), (R, 3),"}\\
+  \hspace{2mm}\phantom{@{text "["}}@{text "(R, 2), (W\<^bsub>1\<^esub>, 3), (L, 4),"}\\
+  \hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (L, 0)"}@{text "]"} 
+  \end{tabular}
+  &
+  \begin{tabular}[t]{@ {}l@ {}}
+  @{text cloop} @{text "\<equiv>"}\\
+  \hspace{2mm}@{text "["}@{text "(R, 0), (R, 2), (R, 3),"}\\
+  \hspace{2mm}\phantom{@{text "["}}@{text "(W\<^bsub>0\<^esub>, 2), (R, 3), (R, 4),"}\\
+  \hspace{2mm}\phantom{@{text "["}}@{text "(W\<^bsub>1\<^esub>, 5), (R, 4), (L, 6),"}\\
+  \hspace{2mm}\phantom{@{text "["}}@{text "(L, 5), (L, 6), (L, 1)"}@{text "]"} 
+  \end{tabular}
+  &
+  \begin{tabular}[t]{@ {}l@ {}}
+  @{text cend} @{text "\<equiv>"}\\
+  \hspace{2mm}@{text "["}@{text "(L, 0), (R, 2), (W\<^bsub>1\<^esub>, 3),"}\\
+  \hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (R, 2), (R, 2),"}\\
+  \hspace{2mm}\phantom{@{text "["}}@{text "(L, 5), (W\<^bsub>0\<^esub>, 4), (R, 0),"}\\
+  \hspace{2mm}\phantom{@{text "["}}@{text "(L, 5)"}@{text "]"} 
+  \end{tabular}
+  \end{tabular}
+  \end{center}
+
+  \end{itemize}
+
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  \definecolor{mygrey}{rgb}{.80,.80,.80}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Hoare Logic for TMs}%
+
+  \begin{itemize}
+  \item Hoare-triples and Hoare-pairs:
+
+  \small
+  \begin{center}
+  \begin{tabular}{@ {\hspace{-6mm}}c@ {\hspace{-3mm}}c@ {}}
+  \begin{tabular}[t]{@ {}l@ {}}
+  \colorbox{mygrey}{@{thm (lhs) Hoare_halt_def}} @{text "\<equiv>"}\\[1mm]
+  \hspace{5mm}@{text "\<forall>"}@{term "tp"}.\\
+  \hspace{7mm}if @{term "P tp"} holds then\\
+  \hspace{7mm}@{text "\<exists>"}@{term n}. such that\\
+  \hspace{7mm}@{text "is_final (steps (1, tp) p n)"} \hspace{1mm}@{text "\<and>"}\\
+  \hspace{7mm}@{text "Q holds_for (steps (1, tp) p n)"}
+  \end{tabular} &
+  \begin{tabular}[t]{@ {}l@ {}}
+  \colorbox{mygrey}{@{thm (lhs) Hoare_unhalt_def}} @{text "\<equiv>"}\\[1mm]
+  \hspace{5mm}@{text "\<forall>"}@{term "tp"}.\\ 
+  \hspace{7mm}if @{term "P tp"} holds then\\
+  \hspace{7mm}@{text "\<forall>"}@{term n}. @{text "\<not> is_final (steps (1, tp) p n)"}
+  \end{tabular}
+  \end{tabular}
+  \end{center}
+
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  \definecolor{mygrey}{rgb}{.80,.80,.80}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Hoare Reasoning}%
+
+  \begin{itemize}
+  \item reasoning is still quite difficult---invariants
+
+  \footnotesize
+  \begin{center}
+\begin{tabular}{@ {\hspace{-4mm}}lcl@ {\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}\\
+  @{thm (lhs) inv_begin3.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin3.simps}\\
+  @{thm (lhs) inv_begin4.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin4.simps}\\
+  @{thm (lhs) inv_begin0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin01} @{text "\<or>"}& (halting state)\\
+                                &             & @{thm (rhs) inv_begin02}\smallskip \\
+   \hline
+  @{thm (lhs) inv_loop1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop1_loop.simps} @{text "\<or>"}\\
+                               &             & @{thm (rhs) inv_loop1_exit.simps} & (starting state)\\
+  @{thm (lhs) inv_loop0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop0.simps}& (halting state)\smallskip\\
+   \hline
+  @{thm (lhs) inv_end1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end1.simps} & (starting state)\\
+  @{thm (lhs) inv_end0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end0.simps} & (halting state)\smallskip\\
+  \hline
+  \end{tabular}
+  \end{center}
+
+  \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}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Recursive Functions}%
+
+  \begin{itemize}
+  \item addition, multiplication, \ldots
+  \item logical operations, quantifiers\ldots
+  \item coding of numbers (Cantor encoding)
+  \item UF\pause\bigskip
+
+  \item Recursive Functions $\Rightarrow$ Register Machines
+  \item Register Machines $\Rightarrow$ Turing Machines
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Sizes}%
+
+  \begin{itemize}
+  \item UF (size: 140843)
+  \item Register Machine (size: 2 Mio instructions)
+  \item UTM (size: 38 Mio states)
+  \end{itemize}\bigskip\bigskip
+
+  \small
+  old version: RM (12 Mio) UTM (112 Mio)
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Separation Algebra}%
+
+  \begin{itemize}
+  \item introduced a separation algebra framework for register machines and TMs 
+  \item we can semi-automate the reasoning for our small TMs
+  \item we can assemble bigger programs out of smaller components\bigskip
+
+  \item looks awfully like ``real'' assembly code\pause
+  \item Conclusion: we have a playing ground for reasoning about low-level 
+  code; we work on automation
+  \end{itemize}
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+
+
+(*<*)
+end
+(*>*)
\ No newline at end of file




