--- 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