Slides/slides01.tex
changeset 197 a35041d5707c
parent 157 1fe44fb6d0a4
child 199 193a9fdcedd6
--- a/Slides/slides01.tex	Sat Jun 11 13:28:45 2016 +0100
+++ b/Slides/slides01.tex	Tue Jun 14 11:58:20 2016 +0100
@@ -66,7 +66,7 @@
   \begin{frame}[c]
 
   \begin{center}
-  \includegraphics[scale=0.2]{isabelle.png}
+  \includegraphics[scale=0.2]{pics/isabelle.png}
   \end{center}
   \mbox{}\\[-20mm]\mbox{}
 
@@ -133,12 +133,12 @@
 \item me, my supervisor, the examiners did not find any problems\medskip 
  \begin{center}
   \begin{tabular}{@ {}c@ {}}
-  \includegraphics[scale=0.38]{barendregt.jpg}\\[-2mm]
+  \includegraphics[scale=0.38]{pics/barendregt.jpg}\\[-2mm]
   \footnotesize Henk Barendregt
   \end{tabular}
   \hspace{2mm}
   \begin{tabular}{@ {}c@ {}}
-  \includegraphics[scale=0.20]{andrewpitts.jpg}\\[-2mm]
+  \includegraphics[scale=0.20]{pics/andrewpitts.jpg}\\[-2mm]
   \footnotesize Andrew Pitts
   \end{tabular}
   \end{center}
@@ -172,7 +172,7 @@
 
 \only<2->{
 \begin{textblock}{3}(13,5)
-\includegraphics[scale=0.33]{skeleton.jpg}
+\includegraphics[scale=0.33]{pics/skeleton.jpg}
 \end{textblock}}
 
 \begin{textblock}{3}(5.3,7)
@@ -235,12 +235,12 @@
 \begin{tabular}{c@ {\hspace{2mm}}c}
 \\[6mm]
 \begin{tabular}{c}
-\includegraphics[scale=0.11]{harper.jpg}\\[-2mm]
+\includegraphics[scale=0.11]{pics/harper.jpg}\\[-2mm]
 {\footnotesize Bob Harper}\\[-2mm]
 {\footnotesize}
 \end{tabular}
 \begin{tabular}{c}
-\includegraphics[scale=0.37]{pfenning.jpg}\\[-2mm]
+\includegraphics[scale=0.37]{pics/pfenning.jpg}\\[-2mm]
 {\footnotesize Frank Pfenning}\\[-2mm]
 {\footnotesize}
 \end{tabular} &
@@ -254,7 +254,7 @@
 \\[0mm]
   
 \begin{tabular}{c}
-\includegraphics[scale=0.36]{appel.jpg}\\[-2mm] 
+\includegraphics[scale=0.36]{pics/appel.jpg}\\[-2mm] 
 {\footnotesize Andrew Appel}\\[-2.5mm]
 {\footnotesize}
 \end{tabular} &
@@ -822,7 +822,7 @@
   \begin{frame}[c]
 
   \begin{center}
-  \includegraphics[scale=0.25]{p3.jpg}
+  \includegraphics[scale=0.25]{pics/p3.jpg}
   \end{center}
 
    \begin{itemize}
@@ -838,7 +838,7 @@
   \begin{frame}[c]
 
   \begin{center}
-  \includegraphics[scale=0.25]{p2.jpg}
+  \includegraphics[scale=0.25]{pics/p2.jpg}
   \end{center}
 
    \begin{itemize}
@@ -858,7 +858,7 @@
   \begin{frame}[c]
 
   \begin{center}
-  \includegraphics[scale=0.15]{p1.pdf}
+  \includegraphics[scale=0.15]{pics/p1.pdf}
   \end{center}
 
   \begin{itemize}
@@ -875,7 +875,7 @@
   \begin{frame}[c]
 
   \begin{center}
-  \includegraphics[scale=0.22]{p5.jpg}
+  \includegraphics[scale=0.22]{pics/p5.jpg}
   \end{center}
 
   \begin{itemize}
@@ -906,24 +906,6 @@
   \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
    
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%  \begin{frame}[c]
-%  \frametitle{\Large{}Mars Pathfinder Mission 1997}
-%
-%  \begin{center}
-%  \includegraphics[scale=0.15]{marspath1.png}
-%  \includegraphics[scale=0.16]{marspath3.png}
-%  \includegraphics[scale=0.3]{marsrover.png}
-%  \end{center}
-%  
-%  \begin{itemize}
-%  \item despite NASA's famous testing procedures, the lander crashed frequently on Mars
-%  \item a scheduling algorithm was not used in the OS at the 
-%  beginning; PIP was enabled after the cause was identified
-%  \end{itemize}
-%
-%  \end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \begin{frame}[c]
@@ -934,7 +916,7 @@
   protocols\bigskip
  
   \item do not venture outside your field of expertise 
-  \includegraphics[scale=0.03]{smiley.jpg}
+  \includegraphics[scale=0.03]{pics/smiley.jpg}
   \bigskip
 
   \item we solved the single-processor case; the multi-processor 
@@ -1143,7 +1125,7 @@
 matcher to POSIX matching/lexing (FLOPS 2014)\bigskip\bigskip\bigskip
 
 \begin{tabular}{@{\hspace{4cm}}c@{}}
-  \includegraphics[scale=0.14]{sulzmann.jpg}\\[-2mm]
+  \includegraphics[scale=0.14]{pics/sulzmann.jpg}\\[-2mm]
   \hspace{0cm}\footnotesize Martin Sulzmann
 \end{tabular}\bigskip\bigskip
 
@@ -1263,7 +1245,7 @@
   \begin{textblock}{11}(1,4.4)
   \begin{center}
   \begin{bubble}[10.9cm]\small\centering
-  \includegraphics[scale=0.37]{msbug.png}
+  \includegraphics[scale=0.37]{pics/msbug.png}
   \end{bubble}
   \end{center}
   \end{textblock}}
@@ -1329,32 +1311,32 @@
 \frametitle{}
 \small
 
-\begin{tabular}{@{}lll@{}}
-\bl{$POSIX(v, r)$} & \bl{$\dn$} & \bl{$\vdash v : r$}\\ 
- & &   \bl{$\wedge \;\;(\forall v'.\;\; \vdash v' : r \,\wedge\, |v'| = |v| 
-     \Rightarrow v \succ_{\alert<2>{r}} v')$}
-\end{tabular}\bigskip\bigskip\bigskip
+%\begin{tabular}{@{}lll@{}}
+%\bl{$POSIX(v, r)$} & \bl{$\dn$} & \bl{$\vdash v : r$}\\ 
+% & &   \bl{$\wedge \;\;(\forall v'.\;\; \vdash v' : r \,\wedge\, |v'| = |v| 
+%     \Rightarrow v \succ_{\alert<2>{r}} v')$}
+%\end{tabular}\bigskip\bigskip\bigskip
 
 
 \centering
 
-\bl{\infer{Seq(v_1, v_2) \succ_{\alert<2>{r_1\cdot r_2}} Seq(v'_1, v'_2)}
-   {v_1 = v'_1 \quad v_2 \succ_{\alert<2>{r_2}} v'_2}}\hspace{3mm}
-\bl{\infer{Seq(v_1, v_2) \succ_{\alert<2>{r_1\cdot r_2}} Seq(v'_1, v'_2)}
-   {v_1 \not= v'_1 \quad v_1 \succ_{\alert<2>{r_1}} v'_1}}
-\bigskip
+%\bl{\infer{Seq(v_1, v_2) \succ_{\alert<2>{r_1\cdot r_2}} Seq(v'_1, v'_2)}
+%   {v_1 = v'_1 \quad v_2 \succ_{\alert<2>{r_2}} v'_2}}\hspace{3mm}
+%\bl{\infer{Seq(v_1, v_2) \succ_{\alert<2>{r_1\cdot r_2}} Seq(v'_1, v'_2)}
+%   {v_1 \not= v'_1 \quad v_1 \succ_{\alert<2>{r_1}} v'_1}}
+%\bigskip
 
-\bl{\infer{Left(v) \succ_{\alert<2>{r_1 + r_2}} Left(v')}
-          {v \succ_{\alert<2>{r_1}} v'}}\hspace{15mm}
-\bl{\infer{Right(v) \succ_{\alert<2>{r_1 + r_2}} Right(v')}
-          {v \succ_{\alert<2>{r_2}} v'}}\bigskip\medskip
+%\bl{\infer{Left(v) \succ_{\alert<2>{r_1 + r_2}} Left(v')}
+%          {v \succ_{\alert<2>{r_1}} v'}}\hspace{15mm}
+%\bl{\infer{Right(v) \succ_{\alert<2>{r_1 + r_2}} Right(v')}
+%          {v \succ_{\alert<2>{r_2}} v'}}\bigskip\medskip
 
-\bl{\infer{Left(v) \succ_{\alert<2>{r_1 + r_2}} Right(v')}
-          {length |v|  \ge length |v'|}}\hspace{15mm}
-\bl{\infer{Right(v) \succ_{\alert<2>{r_1 + r_2}} Left(v')}
-          {length |v| >  length |v'|}}\bigskip
+%\bl{\infer{Left(v) \succ_{\alert<2>{r_1 + r_2}} Right(v')}
+%          {length |v|  \ge length |v'|}}\hspace{15mm}
+%\bl{\infer{Right(v) \succ_{\alert<2>{r_1 + r_2}} Left(v')}
+%          {length |v| >  length |v'|}}\bigskip
 
-\bl{$\big\ldots$}
+%\bl{$\big\ldots$}
 
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
@@ -1450,7 +1432,7 @@
 
 
 \begin{textblock}{11}(12,11)
-\includegraphics[scale=0.15]{roy.jpg}
+\includegraphics[scale=0.15]{pics/roy.jpg}
 \end{textblock}
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -1463,7 +1445,7 @@
   \begin{center}
   \begin{tabular}{@{}cc@{}}
   \begin{tabular}{@{}p{5.6cm}} 
-  \includegraphics[scale=0.43]{icosahedron.png}\\[2mm] 
+  \includegraphics[scale=0.43]{pics/icosahedron.png}\\[2mm] 
   {\bf Math}: \\
   \raggedright\small
   in math, ``objects'' can be ``looked'' at from all 
@@ -1472,7 +1454,7 @@
   difficult to make mistakes
   \end{tabular} &
   \begin{tabular}{p{5cm}} 
-  \includegraphics[scale=0.2]{sel4callgraph.jpg}\\[3mm]
+  \includegraphics[scale=0.2]{pics/sel4callgraph.jpg}\\[3mm]
   \raggedright
   {\bf Code in CS}: \\
   \raggedright\small