
diff -r 52263ffd17b9 -r 681c36b2af27 slides/slides09.tex
--- a/slides/slides09.tex	Sun Nov 24 16:30:34 2019 +0000
+++ b/slides/slides09.tex	Thu Nov 28 08:18:57 2019 +0000
@@ -1,3 +1,4 @@
+% !TEX program = xelatex
 \documentclass[dvipsnames,14pt,t]{beamer}
 \usepackage{../slides}
 \usepackage{../langs}
@@ -6,6 +7,7 @@
 \usepackage{../grammar}
 \usepackage{soul}
 \usepackage{mathpartir}
+\usetikzlibrary{shapes,arrows,shadows}
 
 % beamer stuff
 \renewcommand{\slidecaption}{CFL 09, King's College London}
@@ -26,147 +28,456 @@
   \normalsize
   \begin{center}
   \begin{tabular}{ll}
-  Email:  & christian.urban at kcl.ac.uk\\
-  Office: & N\liningnums{7.07} (North Wing, Bush House)\\
-  Slides: & KEATS (also homework is there)\\
+    Email:  & christian.urban at kcl.ac.uk\\
+    Office Hours: & Thursdays 12 -- 14\\
+    Location: & N7.07 (North Wing, Bush House)\\
+    Slides \& Progs: & KEATS (also homework is there)\\  
   \end{tabular}
   \end{center}
 
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
- 
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[t]
-\frametitle{While Language}
-  
-\begin{center}
-\bl{\begin{tabular}{@{}lcl@{}}
-\\[-12mm]        
-\meta{Stmt} & $::=$ &  $\texttt{skip}$\\
-              & $|$ & \textit{Id}\;\texttt{:=}\;\meta{AExp}\\
-              & $|$ & \texttt{if}\; \meta{BExp} \;\texttt{then}\; \meta{Block} \;\texttt{else}\; \meta{Block}\\
-              & $|$ & \texttt{while}\; \meta{BExp} \;\texttt{do}\; \meta{Block}\\
-              & $|$ & \texttt{read}\;\textit{Id}\\
-              & $|$ & \texttt{write}\;\textit{Id}\\
-              & $|$ & \texttt{write}\;\textit{String}\medskip\\
-\meta{Stmts} & $::=$ &  \meta{Stmt} \;\texttt{;}\; \meta{Stmts} $|$  \meta{Stmt}\medskip\\
-\meta{Block} & $::=$ &  \texttt{\{}\,\meta{Stmts}\,\texttt{\}} $|$ \meta{Stmt}\medskip\\
-\meta{AExp} & $::=$ & \ldots\\
-\meta{BExp} & $::=$ & \ldots\\
-\end{tabular}}
-\end{center}
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c,fragile]
+\frametitle{Functional Programming}
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c]
-\frametitle{\begin{tabular}{c}Fibonacci Numbers\end{tabular}}
+\footnotesize
+\begin{textblock}{13}(0.9,3)
+\begin{lstlisting}[]numbers=none]
+def fib(n) = if n == 0 then 0 
+             else if n == 1 then 1 
+             else fib(n - 1) + fib(n - 2);
 
-\mbox{}\\[-18mm]\mbox{}
+def fact(n) = if n == 0 then 1 else n * fact(n - 1);
 
-{\lstset{language=While}\fontsize{10}{12}\selectfont
-\texttt{\lstinputlisting{../progs/fib.while}}}
+def ack(m, n) = if m == 0 then n + 1
+                else if n == 0 then ack(m - 1, 1)
+                else ack(m - 1, ack(m, n - 1));
+                
+def gcd(a, b) = if b == 0 then a else gcd(b, a % b);                
+\end{lstlisting}
+\end{textblock}
 
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[c,fragile]
-\frametitle{BF***}
+\frametitle{Factorial on the JVM}
 
-some big array, say \texttt{a}; 7 (8) instructions:
+\begin{textblock}{7}(1,1.8)\footnotesize
+\begin{minipage}{6cm}
+\begin{lstlisting}[language=JVMIS,basicstyle=\ttfamily, numbers=none]
+.method public static facT(II)I 
+.limit locals 2
+.limit stack 6
+  iload 0
+  ldc 0
+  if_icmpne If_else_2
+  iload 1
+  goto If_end_3
+If_else_2:
+  iload 0
+  ldc 1
+  isub
+  iload 0
+  iload 1
+  imul
+  invokestatic fact/fact/facT(II)I
+If_end_3:
+  ireturn
+.end method 
+\end{lstlisting}
+\end{minipage}
+\end{textblock}
+
+\begin{textblock}{7}(6,7)
+\begin{bubble}[7cm]\small
+\begin{lstlisting}[language=Lisp,
+                   basicstyle=\ttfamily, 
+                   numbers=none,
+                   xleftmargin=1mm,linebackgroundcolor=\color{cream}]
+def facT(n, acc) = 
+  if n == 0 then acc 
+  else facT(n - 1, n * acc);
+\end{lstlisting}
+\end{bubble}
+\end{textblock}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile,c]
+\frametitle{LLVM}
 
 \begin{itemize}
-\item \texttt{>} move \texttt{ptr++}
-\item \texttt{<} move \texttt{ptr-{}-}
-\item \texttt{+} add \texttt{a[ptr]++}
-\item \texttt{-} subtract \texttt{a[ptr]-{}-}
-\item \texttt{.} print out \texttt{a[ptr]} as ASCII
-\item \texttt{[} if \texttt{a[ptr] == 0} jump just after the corresponding \texttt{]}; otherwise \texttt{ptr++}
-\item \texttt{]} if \texttt{a[ptr] != 0} jump just after the corresponding \texttt{[}; otherwise \texttt{ptr++}
-
-\end{itemize}  
+  \item Chris Lattner, Vikram Adve (started in 2000)
+  \item Apple hired Lattner in 2006
+  \item modular architecture, LLVM-IR
+  \item \texttt{lli} and \texttt{llc} 
+\end{itemize}
 
 \end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\tikzstyle{sensor}=[draw, fill=blue!20, text width=3.8em, line width=1mm,
+    text centered, minimum height=2em,drop shadow]
+\tikzstyle{ann} = [above, text width=4em, text centered]
+\tikzstyle{sc} = [sensor, text width=7em, fill=red!20, 
+    minimum height=6em, rounded corners, drop shadow,line width=1mm]
+
+\begin{frame}[fragile,c]
+\frametitle{LLVM: Overview}
+
+\begin{tikzpicture}
+    % Validation Layer is the same except that there are a set of nodes and links which are added
+   
+    \path (0,0) node (IR) [sc] {\textbf{LLVM-IR}\\ Optimisations};
+    \path (IR.west)+(-2.2,1.7) node (sou1) [sensor] {C++};
+    \path (IR.west)+(-2.2,0.5) node (sou2)[sensor] {C};
+    \path (IR.west)+(-2.2,-1.0) node (dots)[ann] {$\vdots$}; 
+    \path (IR.west)+(-2.2,-1.8) node (sou3)[sensor] {Haskell};    
+
+    \path [draw,->,line width=1mm] (sou1.east) -- node [above] {} (IR.160);
+    \path [draw,->,line width=1mm] (sou2.east) -- node [above] {} (IR.180);
+    \path [draw,->,line width=1mm] (sou3.east) -- node [above] {} (IR.200);
+
+    \path (IR.east)+(2.2,2.0)  node (tar1)[sensor] {x86};
+    \path (IR.east)+(2.2,0.8)  node (tar2)[sensor] {ARM};
+    \path (IR.east)+(2.2,-0.4) node (tar3)[sensor] {MIPS}; 
+    \path (IR.east)+(2.2,-1.6) node (tar4)[sensor] {RISC}; 
+    \path (IR.east)+(2.2,-2.8) node (tar5)[sensor] {Power PC};
+    \path (IR.east)+(2.2,-4.2) node (dots2)[ann] {$\vdots$};
+
+    \path [draw,<-,line width=1mm] (tar1.west) -- node [above] {} (IR.10);
+    \path [draw,<-,line width=1mm] (tar2.west) -- node [above] {} (IR.5);
+    \path [draw,<-,line width=1mm] (tar3.west) -- node [above] {} (IR.0);
+    \path [draw,<-,line width=1mm] (tar4.west) -- node [above] {} (IR.-5);
+    \path [draw,<-,line width=1mm] (tar5.west) -- node [above] {} (IR.-10);
+    
+\end{tikzpicture}
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c,fragile]
-\frametitle{Arrays in While}
+\begin{frame}[fragile,t]
+\frametitle{LLVM-IR}
+\small
+
+\begin{textblock}{7.7}(8,11.4)
+\begin{bubble}[5cm]\small
+\begin{lstlisting}[language=Lisp,
+                   numbers=none,
+                   xleftmargin=1mm,linebackgroundcolor=\color{cream}]
+def fact(n) =
+  if n == 0 then 1 
+  else n * fact(n - 1)
+\end{lstlisting}
+\end{bubble}
+\end{textblock}
 
-\begin{itemize}
-\item \texttt{new arr[15000]}\medskip 
-\item \texttt{x := 3 + arr[3 + y]}\medskip 
-\item \texttt{arr[42 * n] := ...}
-\end{itemize}  
+\begin{lstlisting}[language=LLVM,xleftmargin=-7mm]
+define i32 @fact (i32 %n) {
+   %tmp_19 = icmp eq i32  %n, 0
+   br i1 %tmp_19, label %if_br_23, label %else_br_24
+
+if_br_23:
+   ret i32 1
+
+else_br_24:
+   %tmp_21 = sub i32  %n, 1
+   %tmp_22 = call i32 @fact (i32 %tmp_21)
+   %tmp_20 = mul i32  %n, %tmp_22
+   ret i32 %tmp_20
+}
+\end{lstlisting}
 
 \end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile,c]
+\frametitle{LLVM Types}
+
+\tt
+\begin{center}
+\begin{tabular}{ll}
+boolean & i1 \\
+byte    & i8 \\
+short   & i16\\
+char    & i16\\
+integer & i32\\
+long    & i64\\
+float   & float\\
+double  & double\\
+*\_      & pointer to \\
+**\_     & pointer to a pointer to\\
+\mbox{}[\_]    & arrays of\\
+\end{tabular}
+\end{center}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile,c]
+\frametitle{LLVM Instructions}
+\small
+
+\begin{lstlisting}[language=LLVM]
+br i1 %var, label %if_br, label %else_br
+
+icmp eq i32  %x, %y     ; for equal
+icmp sle i32 %x, %y     ;   signed less or equal
+icmp slt i32 %x, %y     ;   signed less than
+icmp ult i32 %x, %y     ;   unsigned less than 
+
+%var = call i32 @foo(...args...)
+\end{lstlisting}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile,c]
+\frametitle{SSA Format}
+
+\bl{$(1 + a) + (3 + (b * 5))$}\bigskip\bigskip
+
+\begin{lstlisting}[language=LLVM]
+let tmp0 = add 1 a in   
+let tmp1 = mul b 5 in 
+let tmp2 = add 3 tmp1 in 
+let tmp3 = add tmp0 tmp2 in
+  tmp3 
+\end{lstlisting}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c,fragile]
-\frametitle{New Arrays}
+\begin{frame}[fragile,c]
+\frametitle{Abstract Syntax Trees}
+\footnotesize
+
+\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-3mm]
+// Fun language (expressions)
+abstract class Exp 
+abstract class BExp 
+
+case class Call(name: String, args: List[Exp]) extends Exp
+case class If(a: BExp, e1: Exp, e2: Exp) extends Exp
+case class Write(e: Exp) extends Exp
+case class Var(s: String) extends Exp
+case class Num(i: Int) extends Exp
+case class Aop(o: String, a1: Exp, a2: Exp) extends Exp
+case class Sequence(e1: Exp, e2: Exp) extends Exp
+case class Bop(o: String, a1: Exp, a2: Exp) extends BExp  
+\end{lstlisting}
 
-\begin{lstlisting}[mathescape,numbers=none,language=While]
-  new arr[number]
-\end{lstlisting}\bigskip\bigskip
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile,c]
+\frametitle{K-(Intermediate)Language}
+\footnotesize
 
-\begin{lstlisting}[mathescape,numbers=none,language=While]
-  ldc number
-  newarray int
-  astore loc_var
+\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-3mm]
+abstract class KExp
+abstract class KVal
+
+case class KVar(s: String) extends KVal
+case class KNum(i: Int) extends KVal
+case class Kop(o: String, v1: KVal, v2: KVal) extends KVal
+case class KCall(o: String, vrs: List[KVal]) extends KVal
+case class KWrite(v: KVal) extends KVal
+
+case class KIf(x1: String, e1: KExp, e2: KExp) extends KExp
+case class KLet(x: String, v: KVal, e: KExp) extends KExp
+case class KReturn(v: KVal) extends KExp
 \end{lstlisting}
 
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile,c]
+\frametitle{CPS-Translation}
+\small
+
+\begin{lstlisting}[language=Scala,numbers=none]
+def CPS(e: Exp)(k: KVal => KExp) : KExp = 
+  e match { ... }
+\end{lstlisting}
+\bigskip\bigskip
+
+\small
+\begin{lstlisting}[language=LLVMIR,numbers=none,xleftmargin=30mm,escapeinside={(*@}{@*)}]
+let tmp0 = add 1 a in   
+let tmp1 = mul (*@$\Box$@*) 5 in 
+let tmp2 = add 3 tmp1 in 
+let tmp3 = add tmp0 tmp2 in
+  KReturn tmp3 
+\end{lstlisting}
 
 \end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile,c]
+\frametitle{CPS-Translation}
+\small
+
+\begin{lstlisting}[language=Scala,numbers=none]
+def CPS(e: Exp)(k: KVal => KExp) : KExp = 
+  e match { 
+     case Var(s) => k(KVar(s)) 
+     case Num(i) => k(KNum(i))
+     ...
+  }
+\end{lstlisting}
+\bigskip\bigskip
+
+\small
+\begin{lstlisting}[language=LLVMIR,numbers=none,xleftmargin=30mm,escapeinside={(*@}{@*)}]
+let tmp0 = add 1 a in   
+let tmp1 = mul (*@$\Box$@*) 5 in 
+let tmp2 = add 3 tmp1 in 
+let tmp3 = add tmp0 tmp2 in
+  KReturn tmp3 
+\end{lstlisting}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c,fragile]
-\frametitle{Array Update}
+\begin{frame}[fragile,c]
+\frametitle{CPS-Translation}
+\small
 
-\begin{lstlisting}[mathescape,numbers=none,language=While]
-  arr[...] := 
-\end{lstlisting}\bigskip\bigskip
-
-\begin{lstlisting}[mathescape,numbers=none,language=While]
-  aload loc_var
-  index_aexp
-  value_aexp
-  iastore
+\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-5mm]
+def CPS(e: Exp)(k: KVal => KExp) : KExp = e match { 
+  case Aop(o, e1, e2) => {
+    val z = Fresh("tmp")
+    CPS(e1)(y1 => 
+      CPS(e2)(y2 => 
+               KLet(z, Kop(o, y1, y2), k(KVar(z)))))
+  } ...
+}
 \end{lstlisting}
 
+\small
+\begin{lstlisting}[language=LLVMIR,numbers=none,xleftmargin=30mm,escapeinside={(*@}{@*)}]
+...
+let z = op (*@$\Box_{y_1}$@*) (*@$\Box_{y_2}$@*)
+let tmp0 = add 1 a in   
+let tmp1 = mul (*@$\Box\!\!\!\!\raisebox{0.6mm}{\texttt{z}}$@*) 5 in 
+let tmp2 = add 3 tmp1 in 
+let tmp3 = add tmp0 tmp2 in
+  KReturn tmp3 
+\end{lstlisting}
 
 \end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c,fragile]
-\frametitle{Array Lookup in AExp}
+\begin{frame}[fragile,c]
+\frametitle{CPS-Translation}
+\small
 
-\begin{lstlisting}[mathescape,numbers=none,language=While]
-  ...arr[...]... 
-\end{lstlisting}\bigskip\bigskip
+\begin{lstlisting}[language=Scala,numbers=none]
+def CPS(e: Exp)(k: KVal => KExp) : KExp = 
+  e match { 
+    case Sequence(e1, e2) => 
+      CPS(e1)(_ => CPS(e2)(y2 => k(y2)))
+     ...
+  }
+\end{lstlisting}
+\bigskip\bigskip
 
-\begin{lstlisting}[mathescape,numbers=none,language=While]
-  aload loc_var
-  index_aexp
-  iaload
+\small
+\begin{lstlisting}[language=LLVMIR,numbers=none,xleftmargin=30mm,escapeinside={(*@}{@*)}]
+let tmp0 = add 1 a in   
+let tmp1 = mul (*@$\Box$@*) 5 in 
+let tmp2 = add 3 tmp1 in 
+let tmp3 = add tmp0 tmp2 in
+  KReturn tmp3 
 \end{lstlisting}
 
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile,c]
+\frametitle{CPS-Translation}
+\small
+
+\begin{lstlisting}[language=Scala,numbers=none]
+def CPS(e: Exp)(k: KVal => KExp) : KExp = 
+  e match { 
+    ...
+    case Sequence(e1, e2) => 
+      CPS(e1)(_ => CPS(e2)(y2 => k(y2)))
+     ...
+  }
+\end{lstlisting}
+\bigskip\bigskip
+
+\small
+\begin{lstlisting}[language=LLVMIR,numbers=none,xleftmargin=30mm,escapeinside={(*@}{@*)}]
+let tmp0 = add 1 a in   
+let tmp1 = mul (*@$\Box$@*) 5 in 
+let tmp2 = add 3 tmp1 in 
+let tmp3 = add tmp0 tmp2 in
+  KReturn tmp3 
+\end{lstlisting}
 
 \end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
+\begin{frame}[fragile,c]
+\frametitle{CPS-Translation}
+\small
+
+\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-3mm]
+def CPS(e: Exp)(k: KVal => KExp) : KExp = 
+  e match { 
+    ...
+    case If(Bop(o, b1, b2), e1, e2) => {
+      val z = Fresh("tmp")
+      CPS(b1)(y1 => 
+        CPS(b2)(y2 => 
+          KLet(z, Kop(o, y1, y2), 
+                KIf(z, CPS(e1)(k), CPS(e2)(k)))))
+     }
+    ...
+  }
+\end{lstlisting}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[c]
 
 \large\bf
-Using a compiler, \\how can you mount the\\ perfect attack against a system?
+Using a compiler, \\
+how can you mount the\\ 
+perfect attack against a system?
 
-\end{frame}}
+\end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -323,6 +634,129 @@
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \begin{frame}[c]
+  \frametitle{Dijkstra on Testing}
+  
+  \begin{bubble}[10cm]
+  ``Program testing can be a very effective way to show the
+  presence of bugs, but it is hopelessly inadequate for showing
+  their absence.''
+  \end{bubble}\bigskip
+  
+  \small
+  What is good about compilers: the either seem to work,
+  or go horribly wrong (most of the time).
+  
+  \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{\Large Proving Programs to be Correct}
+
+\begin{bubble}[10cm]
+\small
+{\bf Theorem:} There are infinitely many prime 
+numbers.\medskip\\
+
+{\bf Proof} \ldots\\
+\end{bubble}\bigskip
+
+
+similarly\bigskip
+
+\begin{bubble}[10cm]
+\small
+{\bf Theorem:} The program is doing what 
+it is supposed to be doing.\medskip
+
+{\bf Long, long proof} \ldots\\
+\end{bubble}\bigskip\medskip
+
+\small This can be a gigantic proof. The only hope is to have
+help from the computer. `Program' is here to be understood to be
+quite general (compiler, OS, \ldots).
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+\begin{frame}[c]
+\frametitle{Can This Be Done?}
+
+\begin{itemize}
+\item in 2008, verification of a small C-compiler
+\begin{itemize}
+\item ``if my input program has a certain behaviour, then the compiled machine code has the same behaviour''
+\item is as good as \texttt{gcc -O1}, but much, much less buggy 
+\end{itemize}
+\end{itemize}
+
+\begin{center}
+  \includegraphics[scale=0.12]{../pics/compcert.png}
+\end{center}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+\begin{frame}[t]
+\frametitle{Fuzzy Testing C-Compilers}
+
+\begin{itemize}
+\item tested GCC, LLVM and others by randomly generating 
+C-programs
+\item found more than 300 bugs in GCC and also
+many in LLVM (some of them highest-level critical)\bigskip
+\item about CompCert:
+
+\begin{bubble}[10.7cm]\small ``The striking thing about our CompCert
+results is that the middle-end bugs we found in all other
+compilers are absent. As of early 2011, the under-development
+version of CompCert is the only compiler we have tested for
+which Csmith cannot find wrong-code errors. This is not for
+lack of trying: we have devoted about six CPU-years to the
+task.'' 
+\end{bubble} 
+\end{itemize}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+\begin{frame}[c]
+\frametitle{Next Week}
+
+\begin{itemize}
+\item Revision Lecture\medskip
+\item How many  strings are in $\bl{L(a^*)}$?\pause\medskip
+\item How many  strings are in $\bl{L((a + b)^*)}$?\\ Are there more than
+  in $\bl{L(a^*)}$?
+\end{itemize}
+
+
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+
+
+\end{document}
+
+%%% Local Variables:  
+%%% mode: latex
+%%% TeX-master: t
+%%% End: 
+
+
+
+
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \begin{frame}[c]
 
@@ -533,122 +967,3 @@
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
 
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \begin{frame}[c]
-  \frametitle{Dijkstra on Testing}
-  
-  \begin{bubble}[10cm]
-  ``Program testing can be a very effective way to show the
-  presence of bugs, but it is hopelessly inadequate for showing
-  their absence.''
-  \end{bubble}\bigskip
-  
-  \small
-  What is good about compilers: the either seem to work,
-  or go horribly wrong (most of the time).
-  
-  \end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c]
-\frametitle{\Large Proving Programs to be Correct}
-
-\begin{bubble}[10cm]
-\small
-{\bf Theorem:} There are infinitely many prime 
-numbers.\medskip\\
-
-{\bf Proof} \ldots\\
-\end{bubble}\bigskip
-
-
-similarly\bigskip
-
-\begin{bubble}[10cm]
-\small
-{\bf Theorem:} The program is doing what 
-it is supposed to be doing.\medskip
-
-{\bf Long, long proof} \ldots\\
-\end{bubble}\bigskip\medskip
-
-\small This can be a gigantic proof. The only hope is to have
-help from the computer. `Program' is here to be understood to be
-quite general (compiler, OS, \ldots).
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-
-\begin{frame}[c]
-\frametitle{Can This Be Done?}
-
-\begin{itemize}
-\item in 2008, verification of a small C-compiler
-\begin{itemize}
-\item ``if my input program has a certain behaviour, then the compiled machine code has the same behaviour''
-\item is as good as \texttt{gcc -O1}, but much, much less buggy 
-\end{itemize}
-\end{itemize}
-
-\begin{center}
-  \includegraphics[scale=0.12]{../pics/compcert.png}
-\end{center}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-\begin{frame}[t]
-\frametitle{Fuzzy Testing C-Compilers}
-
-\begin{itemize}
-\item tested GCC, LLVM and others by randomly generating 
-C-programs
-\item found more than 300 bugs in GCC and also
-many in LLVM (some of them highest-level critical)\bigskip
-\item about CompCert:
-
-\begin{bubble}[10.7cm]\small ``The striking thing about our CompCert
-results is that the middle-end bugs we found in all other
-compilers are absent. As of early 2011, the under-development
-version of CompCert is the only compiler we have tested for
-which Csmith cannot find wrong-code errors. This is not for
-lack of trying: we have devoted about six CPU-years to the
-task.'' 
-\end{bubble} 
-\end{itemize}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-
-\begin{frame}[c]
-\frametitle{Next Week}
-
-\begin{itemize}
-\item Revision Lecture\medskip
-\item How many  strings are in $\bl{L(a^*)}$?\pause\medskip
-\item How many  strings are in $\bl{L((a + b)^*)}$?\\ Are there more than
-  in $\bl{L(a^*)}$?
-\end{itemize}
-
-
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-
-
-
-\end{document}
-
-%%% Local Variables:  
-%%% mode: latex
-%%% TeX-master: t
-%%% End: 
-




