lexing: comparison Slides/slides01.tex

equal deleted inserted replaced

-:5fa8344a5176
+:a35041d5707c
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[c]
 \begin{center}
-\includegraphics[scale=0.2]{isabelle.png}
+\includegraphics[scale=0.2]{pics/isabelle.png}
 \end{center}
 \mbox{}\\[-20mm]\mbox{}
 \begin{itemize}
 \item Isabelle interactive theorem prover;
 termination argument (sort of $\lambda$-calculus)\medskip
 \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}
 \item people were building their work on my result
 be generalised
 \end{itemize}
 \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)
 \onslide<1->{
 \begin{tikzpicture}
 \frametitle{}
 \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} &
 \begin{tabular}{p{6cm}}
 \end{tabular}\\
 \\[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} &
 \begin{tabular}{p{6cm}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[c]
 \begin{center}
-\includegraphics[scale=0.25]{p3.jpg}
+\includegraphics[scale=0.25]{pics/p3.jpg}
 \end{center}
 \begin{itemize}
 \item by Rajkumar, 1991
 \item \it ``it resumes the priority it had at the point of entry into the critical
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[c]
 \begin{center}
-\includegraphics[scale=0.25]{p2.jpg}
+\includegraphics[scale=0.25]{pics/p2.jpg}
 \end{center}
 \begin{itemize}
 \item by Jane Liu, 2000
 \item {\it ``The job $J_l$ executes at its inherited
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[c]
 \begin{center}
-\includegraphics[scale=0.15]{p1.pdf}
+\includegraphics[scale=0.15]{pics/p1.pdf}
 \end{center}
 \begin{itemize}
 \item by Laplante and Ovaska, 2011 (\$113.76)
 \item \it ``when $[$the task$]$ exits the critical section that
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[c]
 \begin{center}
-\includegraphics[scale=0.22]{p5.jpg}
+\includegraphics[scale=0.22]{pics/p5.jpg}
 \end{center}
 \begin{itemize}
 \item by Silberschatz, Galvin and Gagne (9th edition, 2013)
 \item \it ``Upon releasing the
 \end{itemize}
 \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]
 \frametitle{Lessons Learned}
 \begin{itemize}
 \item our proof-technique is adapted from security
 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
 case: no idea!
 \end{itemize}
 \item Sulzmann \& Lu came up with a beautiful
 idea for how to extend the simple regular expression
 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
 \item the idea: define an inverse operation to the derivatives
 \end{itemize}
 \only<3>{%
 \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}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}<1>[c]
 \frametitle{}
 \small
-\begin{tabular}{@{}lll@{}}
+%\begin{tabular}{@{}lll@{}}
-\bl{$POSIX(v, r)$} & \bl{$\dn$} & \bl{$\vdash v : r$}\\
+%\bl{$POSIX(v, r)$} & \bl{$\dn$} & \bl{$\vdash v : r$}\\
-& &   \bl{$\wedge \;\;(\forall v'.\;\; \vdash v' : r \,\wedge\, |v'| = |v|
+% & &   \bl{$\wedge \;\;(\forall v'.\;\; \vdash v' : r \,\wedge\, |v'| = |v|
-\Rightarrow v \succ_{\alert<2>{r}} v')$}
+%     \Rightarrow v \succ_{\alert<2>{r}} v')$}
-\end{tabular}\bigskip\bigskip\bigskip
+%\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)}
+%\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}
+%   {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)}
+%\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}}
+%   {v_1 \not= v'_1 \quad v_1 \succ_{\alert<2>{r_1}} v'_1}}
-\bigskip
+%\bigskip
-\bl{\infer{Left(v) \succ_{\alert<2>{r_1 + r_2}} Left(v')}
+%\bl{\infer{Left(v) \succ_{\alert<2>{r_1 + r_2}} Left(v')}
-{v \succ_{\alert<2>{r_1}} v'}}\hspace{15mm}
+%          {v \succ_{\alert<2>{r_1}} v'}}\hspace{15mm}
-\bl{\infer{Right(v) \succ_{\alert<2>{r_1 + r_2}} Right(v')}
+%\bl{\infer{Right(v) \succ_{\alert<2>{r_1 + r_2}} Right(v')}
-{v \succ_{\alert<2>{r_2}} v'}}\bigskip\medskip
+%          {v \succ_{\alert<2>{r_2}} v'}}\bigskip\medskip
-\bl{\infer{Left(v) \succ_{\alert<2>{r_1 + r_2}} Right(v')}
+%\bl{\infer{Left(v) \succ_{\alert<2>{r_1 + r_2}} Right(v')}
-{length |v|  \ge length |v'|}}\hspace{15mm}
+%          {length |v|  \ge length |v'|}}\hspace{15mm}
-\bl{\infer{Right(v) \succ_{\alert<2>{r_1 + r_2}} Left(v')}
+%\bl{\infer{Right(v) \succ_{\alert<2>{r_1 + r_2}} Left(v')}
-{length |v| >  length |v'|}}\bigskip
+%          {length |v| >  length |v'|}}\bigskip
-\bl{$\big\ldots$}
+%\bl{$\big\ldots$}
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \end{itemize}
 \begin{textblock}{11}(12,11)
-\includegraphics[scale=0.15]{roy.jpg}
+\includegraphics[scale=0.15]{pics/roy.jpg}
 \end{textblock}
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[c]
 \frametitle{Proofs in Math~vs.~in CS}
 \\[-10mm]\mbox{}
 \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
 ``angles'';\\\smallskip
 non-trivial proofs, but it seems
 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
 the call-graph of the seL4 microkernel OS;\\\smallskip
 easy to make mistakes\\ \mbox{}\\

changeset 197	a35041d5707c
parent 157	1fe44fb6d0a4
child 199	193a9fdcedd6