diff -r 5fa8344a5176 -r a35041d5707c Slides/slides01.tex --- 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