\documentclass[dvipsnames,14pt,t]{beamer}

\usepackage{langs}

%\usepackage{grammar}

\usepackage{soul}

\usepackage{data}

\usepackage{proof}

\renewcommand{\slidecaption}{Canterbury, 22.2.2016}

\newcommand\grid[1]{%

\begin{tikzpicture}[baseline=(char.base)]

  \path[use as bounding box]

    (0,0) rectangle (1em,1em);

  \draw[red!50, fill=red!20]

    (0,0) rectangle (1em,1em);

  \node[inner sep=1pt,anchor=base west]

    (char) at (0em,\gridraiseamount) {#1};

\end{tikzpicture}}

\newcommand\gridraiseamount{0.12em}

\makeatletter

\newcommand\Grid[1]{%

  \@tfor\z:=#1\do{\grid{\z}}}

\makeatother	

\newcommand\Vspace[1][.3em]{%

  \mbox{\kern.06em\vrule height.3ex}%

  \vbox{\hrule width#1}%

  \hbox{\vrule height.3ex}}

\def\VS{\Vspace[0.6em]}

  \Large POSIX Lexing with Derivatives\\[-1.5mm] 

  \Large of Regular Expressions\\[-1mm] 

  %\normalsize Or, How to Find Bugs with the\\[-5mm] 

  %\normalsize Isabelle Theorem Prover

  \begin{tabular}{c}

  \small Christian Urban\\

  \small King's College London\\

  \\

  \\

  Joint work with Fahad Ausaf and Roy Dyckhoff

  \includegraphics[scale=0.2]{isabelle.png}

  \mbox{}\\[-20mm]\mbox{}

  \begin{itemize}

  \item Isabelle interactive theorem prover; 

  some proofs are automatic -- most however need help

  \item the learning curve is steep; you often have to fight the 

  theorem prover\ldots no different in other ITPs

  \end{itemize}

\frametitle{Why Bother?}

Surely regular expressions must have been implemented and 

studied to death, no?

\begin{center}

\begin{tikzpicture}

\begin{axis}[

    xlabel={{\tt a}s},

    ylabel={time in secs},

    enlargelimits=false,

    xtick={0,5,...,30},

    xmax=30,

    ymax=35,

    ytick={0,5,...,30},

    scaled ticks=false,

    axis lines=left,

    width=8cm,

    height=6cm, 

    legend entries={Python,Ruby},  

    legend pos=north west,

    legend cell align=left  

]

\addplot[blue,mark=*, mark options={fill=white}] 

  table {re-python.data};

\addplot[brown,mark=pentagon*, mark options={fill=white}] 

  table {re-ruby.data};  

\end{axis}

\end{tikzpicture}

\end{center}

evil regular expressions: \bl{$({\tt a}?)^n \cdot {\tt a}^n$}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}[c]

\frametitle{\Large Isabelle Theorem Prover}

\begin{itemize}

\item started to use Isabelle after my PhD (in 2000)

\item the thesis included a rather complicated 

  ``pencil-and-paper'' proof for a 

  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]

  \footnotesize Henk Barendregt

  \end{tabular}

  \hspace{2mm}

  \begin{tabular}{@ {}c@ {}}

  \includegraphics[scale=0.20]{andrewpitts.jpg}\\[-2mm]

  \footnotesize Andrew Pitts

  \end{tabular}

  \end{center}

\item people were building their work on my result      

\end{itemize}

\begin{frame}[t]

\frametitle{\Large Nominal Isabelle}

\begin{itemize}

\item implemented a package for the Isabelle prover 

in order to reason conveniently about binders 

\begin{center}

\large\bl{$\lambda \alert{x}.\,M$} \hspace{10mm}

\bl{$\forall \alert{x}.\,P\,x$}

\end{center}\bigskip\bigskip\bigskip\bigskip

\bigskip\bigskip\bigskip\pause\pause

\item when finally being able to formalise the proof from my PhD, I found that the main result

      (termination) is correct, but a central lemma needed to

      be generalised

\end{itemize}

\only<2->{

\begin{textblock}{3}(13,5)

\includegraphics[scale=0.33]{skeleton.jpg}

\end{textblock}}

\begin{textblock}{3}(5.3,7)

\onslide<1->{

\begin{tikzpicture}

\node at (0,0) [single arrow, shape border rotate=90, fill=red,text=red]{\mbox{a}};

\end{tikzpicture}}

\end{textblock}

\begin{textblock}{3}(8.7,7)

\onslide<1->{

\begin{tikzpicture}

\node at (0,0) [single arrow, shape border rotate=90, fill=red,text=red]{\mbox{a}};

\end{tikzpicture}}

\end{textblock}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}[c]

\frametitle{\Large Variable Convention}

\begin{center}

\begin{bubble}[10cm]

  \color{gray}  

  \small

  {\bf\mbox{}Variable Convention:}\\[1mm] 

  If $M_1,\ldots,M_n$ occur in a certain mathematical context

  (e.g. definition, proof), then in these terms all bound variables 

  are chosen to be different from the free variables.\\[2mm]

  \footnotesize\hfill Barendregt in ``The Lambda-Calculus: Its Syntax and Semantics''

\end{bubble}

\end{center}

\mbox{}\\[-8mm]

\begin{itemize}

\item instead of proving a property for \alert{\bf all} bound

variables, you prove it only for \alert{\bf some}\ldots?

\item feels like it is used in 90\% of papers in PT and FP

(9.9\% use de-Bruijn indices)

\item this is mostly OK, but in some corner-cases you can use it

to prove \alert{\bf false}\ldots we fixed this!

\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

\begin{frame}[c]

\frametitle{}

\begin{tabular}{c@ {\hspace{2mm}}c}

\\[6mm]

\begin{tabular}{c}

\includegraphics[scale=0.11]{harper.jpg}\\[-2mm]

{\footnotesize Bob Harper}\\[-2mm]

{\footnotesize}

\end{tabular}

\begin{tabular}{c}

\includegraphics[scale=0.37]{pfenning.jpg}\\[-2mm]

{\footnotesize Frank Pfenning}\\[-2mm]

{\footnotesize}

\end{tabular} &

\begin{tabular}{p{6cm}}

\raggedright

{published a proof in\\ {\bf ACM Transactions on Computational Logic}, 2005,

$\sim$31pp}

\end{tabular}\\

\\[0mm]

\begin{tabular}{c}

\includegraphics[scale=0.36]{appel.jpg}\\[-2mm] 

{\footnotesize Andrew Appel}\\[-2.5mm]

{\footnotesize}

\end{tabular} &

\begin{tabular}{p{6cm}}

\raggedright

{relied on their proof in a\\ {\bf security} critical application}

\end{tabular}

\end{tabular}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}

\frametitle{Proof-Carrying Code}

\begin{textblock}{10}(2.5,2.2)

\begin{block}{Idea:}

\begin{center}

\begin{tikzpicture}

\draw[help lines,cream] (0,0.2) grid (8,4);

\draw[line width=1mm, red] (5.5,0.6) rectangle (7.5,4);

\node[anchor=base] at (6.5,2.8) 

     {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering  user: untrusted code\end{tabular}};

\draw[line width=1mm, red] (0.1,0.6) rectangle (2.1,4);

  \node[anchor=base] at (1.1,2.3) 

     {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering  developer ---\\ web server\end{tabular}};

\onslide<3->{

  \draw[line width=1mm, red, fill=red] (5.5,0.6) rectangle (7.5,1.8);

  \node[anchor=base,white] at (6.5,1.1) 

     {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\bf\centering proof- checker\end{tabular}};}

  \node at (3.6,3.0) [single arrow, fill=red,text=white, 

                      minimum height=3.4cm]{\bf code};

  \onslide<2->{

  \node at (3.6,1.3) [single arrow, fill=red,text=white, 

                      minimum height=3.4cm]{\bf certificate};

  \node at (3.6,1.9) {\small\color{gray}{\mbox{}\hspace{-1mm}a proof in LF}};

}

\end{tikzpicture}

\end{center}

\end{block}

\end{textblock}

\begin{textblock}{15}(2,12)

\small

\begin{itemize}

\item<3-> Appel's checker is $\sim$2700 lines of code (1865 loc of\\ LF definitions; 

803 loc in C including 2 library functions)\\[-3mm]

\item<3-> 167 loc in C implement a type-checker

\end{itemize}

\end{textblock}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \begin{frame}<2->[squeeze]

  \frametitle{} 

  \begin{columns}

  \tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex]

  \tikzstyle{node1}=[rectangle, minimum size=10mm, rounded corners=3mm, very thick, 

                     draw=black!50, top color=white, bottom color=black!20]

  \tikzstyle{node2}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick, 

                     draw=red!70, top color=white, bottom color=red!50!black!20]

  \begin{column}{0.8\textwidth}

  \begin{textblock}{0}(1,2)

  \begin{tikzpicture}

  \matrix[ampersand replacement=\&,column sep=7mm, row sep=5mm]

  { \&[-10mm] 

    \node (def1)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}}; \&

    \node (proof1) [node1] {\large Proof}; \&

    \node (alg1)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}}; \\

    \onslide<4->{\node {\begin{tabular}{c}\small 1st\\[-2.5mm] \footnotesize solution\end{tabular}};} \&

    \onslide<4->{\node (def2)   [node2] {\large Spec$^\text{+ex}$};} \&

    \onslide<4->{\node (proof2) [node1] {\large Proof};} \&

    \onslide<4->{\node (alg2)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\

    \onslide<5->{\node {\begin{tabular}{c}\small 2nd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&

    \onslide<5->{\node (def3)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&

    \onslide<5->{\node (proof3) [node1] {\large Proof};} \&

    \onslide<5->{\node (alg3)   [node2] {\large Alg$^\text{-ex}$};} \\

    \onslide<6->{\node {\begin{tabular}{c}\small 3rd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&

    \onslide<6->{\node (def4)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&

    \onslide<6->{\node (proof4) [node2] {\large\hspace{1mm}Proof\hspace{1mm}};} \&

    \onslide<6->{\node (alg4)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\

  };

  \draw[->,black!50,line width=2mm] (proof1) -- (def1);

  \draw[->,black!50,line width=2mm] (proof1) -- (alg1);

  \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (def2);}

  \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (alg2);}

  \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (def3);}

  \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (alg3);}

  \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (def4);}

  \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (alg4);}

  \onslide<3->{\draw[white,line width=1mm] (1.1,3.2) -- (0.9,2.85) -- (1.1,2.35) -- (0.9,2.0);} 

  \end{tikzpicture}

  \end{textblock}

  \end{column}

  \end{columns}

  \begin{textblock}{3}(12,3.6)

  \onslide<4->{

  \begin{tikzpicture}

  \node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{2h};

  \end{tikzpicture}}

  \end{textblock}

  \begin{textblock}{0}(0.4,12.8)

  \onslide<6->{

  \begin{bubble}[11cm]

  \small Each time one needs to check $\sim$31pp~of 

  informal paper proofs.

  You have to be able to keep definitions 

  and proofs consistent.

  \end{bubble}}

  \end{textblock}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%  \begin{frame}[c]

%  \frametitle{\Large Lessons Learned}

%

%  \begin{itemize}

%  \item using a theorem prover we were able to keep a large 

%  proof consistent with changes in the definitions\bigskip

%  \item it took us some 10 days to get to the error\ldots

%  probably the same time Harper and Pfenning needed to \LaTeX{}

%  their paper\bigskip 

%  \item once there, we ran circles around them

%  \end{itemize}

%

%  \end{frame}

  \frametitle{Real-Time Scheduling} 

   \node at (2.5,0.9) {\small locks a resource};

   \node at (2.5,0.9) {\small locks a resource};

   \node at (2.5,0.9) {\small locks a resource};

   \node at (2.5,0.9) {\small locks a resource};

   \node at (2.5,0.9) {\small locks a resource}; 

   \node at (2.5,0.9) {\small locks a resource}; 

   \node at (2.5,0.9) {\small locks a resource}; 

   \node at (2.5,0.9) {\small locks a resource};