slides/slides05.tex
changeset 124 382aad582d8b
parent 123 2185acdb43bb
child 125 27103cafb297
equal deleted inserted replaced
123:2185acdb43bb 124:382aad582d8b
     1 \documentclass[dvipsnames,14pt,t]{beamer}
     1 \documentclass[dvipsnames,14pt,t]{beamer}
     2 \usepackage{proof}
     2 \usepackage{proof}
     3 \usepackage{beamerthemeplaincu}
     3 \usepackage{beamerthemeplaincu}
     4 %\usepackage[T1]{fontenc}
     4 \usepackage{fontenc}
     5 %\usepackage[latin1]{inputenc}
     5 \usepackage[latin1]{inputenc}
     6 \usepackage{mathpartir}
     6 \usepackage{mathpartir}
     7 \usepackage{isabelle}
     7 \usepackage{isabelle}
     8 \usepackage{isabellesym}
     8 \usepackage{isabellesym}
     9 \usepackage[absolute,overlay]{textpos}
     9 \usepackage[absolute,overlay]{textpos}
    10 \usepackage{ifthen}
    10 \usepackage{ifthen}
    13 \usepackage{listings}
    13 \usepackage{listings}
    14 \usetikzlibrary{arrows}
    14 \usetikzlibrary{arrows}
    15 \usetikzlibrary{positioning}
    15 \usetikzlibrary{positioning}
    16 \usetikzlibrary{calc}
    16 \usetikzlibrary{calc}
    17 \usepackage{graphicx} 
    17 \usepackage{graphicx} 
       
    18 \setmonofont{Consolas}
    18 
    19 
    19 \isabellestyle{rm}
    20 \isabellestyle{rm}
    20 \renewcommand{\isastyle}{\rm}%
    21 \renewcommand{\isastyle}{\rm}%
    21 \renewcommand{\isastyleminor}{\rm}%
    22 \renewcommand{\isastyleminor}{\rm}%
    22 \renewcommand{\isastylescript}{\footnotesize\rm\slshape}%
    23 \renewcommand{\isastylescript}{\footnotesize\rm\slshape}%
    33 \renewcommand{\isacharless}{$\langle$}
    34 \renewcommand{\isacharless}{$\langle$}
    34 \renewcommand{\isachargreater}{$\rangle$}
    35 \renewcommand{\isachargreater}{$\rangle$}
    35 \renewcommand{\isasymsharp}{\isamath{\#}}
    36 \renewcommand{\isasymsharp}{\isamath{\#}}
    36 \renewcommand{\isasymdots}{\isamath{...}}
    37 \renewcommand{\isasymdots}{\isamath{...}}
    37 \renewcommand{\isasymbullet}{\act}
    38 \renewcommand{\isasymbullet}{\act}
    38 
    39 \newcommand{\isaliteral}[1]{}
    39 
    40 \newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
    40 
    41 
    41 \definecolor{javared}{rgb}{0.6,0,0} % for strings
    42 \definecolor{javared}{rgb}{0.6,0,0} % for strings
    42 \definecolor{javagreen}{rgb}{0.25,0.5,0.35} % comments
    43 \definecolor{javagreen}{rgb}{0.25,0.5,0.35} % comments
    43 \definecolor{javapurple}{rgb}{0.5,0,0.35} % keywords
    44 \definecolor{javapurple}{rgb}{0.5,0,0.35} % keywords
    44 \definecolor{javadocblue}{rgb}{0.25,0.35,0.75} % javadoc
    45 \definecolor{javadocblue}{rgb}{0.25,0.35,0.75} % javadoc
    45 
    46 
    46 \lstset{language=Java,
    47 \makeatletter
    47 	basicstyle=\ttfamily,
    48 \lst@CCPutMacro\lst@ProcessOther {"2D}{\lst@ttfamily{-{}}{-{}}}
    48 	keywordstyle=\color{javapurple}\bfseries,
    49 \@empty\z@\@empty
    49 	stringstyle=\color{javagreen},
    50 \makeatother
    50 	commentstyle=\color{javagreen},
    51 
    51 	morecomment=[s][\color{javadocblue}]{/**}{*/},
       
    52 	numbers=left,
       
    53 	numberstyle=\tiny\color{black},
       
    54 	stepnumber=1,
       
    55 	numbersep=10pt,
       
    56 	tabsize=2,
       
    57 	showspaces=false,
       
    58 	showstringspaces=false}
       
    59 
    52 
    60 \lstdefinelanguage{scala}{
    53 \lstdefinelanguage{scala}{
    61   morekeywords={abstract,case,catch,class,def,%
    54   morekeywords={abstract,case,catch,class,def,%
    62     do,else,extends,false,final,finally,%
    55     do,else,extends,false,final,finally,%
    63     for,if,implicit,import,match,mixin,%
    56     for,if,implicit,import,match,mixin,%
    72   morestring=[b]",
    65   morestring=[b]",
    73   morestring=[b]',
    66   morestring=[b]',
    74   morestring=[b]"""
    67   morestring=[b]"""
    75 }
    68 }
    76 
    69 
       
    70 \lstdefinelanguage{while}{
       
    71   morekeywords={while, if, then. else, read, write},
       
    72   otherkeywords={=>,<-,<\%,<:,>:,\#,@},
       
    73   sensitive=true,
       
    74   morecomment=[l]{//},
       
    75   morecomment=[n]{/*}{*/},
       
    76   morestring=[b]",
       
    77   morestring=[b]',
       
    78   morestring=[b]"""
       
    79 }
       
    80 
       
    81 
    77 \lstset{language=Scala,
    82 \lstset{language=Scala,
    78 	basicstyle=\ttfamily,
    83 	basicstyle=\ttfamily,
    79 	keywordstyle=\color{javapurple}\bfseries,
    84 	keywordstyle=\color{javapurple}\bfseries,
    80 	stringstyle=\color{javagreen},
    85 	stringstyle=\color{javagreen},
    81 	commentstyle=\color{javagreen},
    86 	commentstyle=\color{javagreen},
    85 	stepnumber=1,
    90 	stepnumber=1,
    86 	numbersep=10pt,
    91 	numbersep=10pt,
    87 	tabsize=2,
    92 	tabsize=2,
    88 	showspaces=false,
    93 	showspaces=false,
    89 	showstringspaces=false}
    94 	showstringspaces=false}
       
    95 	
    90 
    96 
    91 % beamer stuff 
    97 % beamer stuff 
    92 \renewcommand{\slidecaption}{APP 05, King's College London, 29 October 2013}
    98 \renewcommand{\slidecaption}{APP 05, King's College London, 29 October 2013}
    93 
    99 
    94 \newcommand{\bl}[1]{\textcolor{blue}{#1}}
   100 \newcommand{\bl}[1]{\textcolor{blue}{#1}}
   548 \end{quote}
   554 \end{quote}
   549 
   555 
   550 \end{frame}}
   556 \end{frame}}
   551 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
   557 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
   552 
   558 
       
   559 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   560   \mode<presentation>{
       
   561   \begin{frame}[t]
       
   562   \frametitle{\Large\begin{tabular}{@ {}c@ {}}Logic(s)\end{tabular}}
       
   563 
       
   564   \begin{itemize}
       
   565   \item Formulas
       
   566 
       
   567   \begin{center}\color{blue}
       
   568   \begin{tabular}{rcl@ {\hspace{10mm}}l}
       
   569   \isa{F} & \isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}} & \isa{true} \\
       
   570             & \isa{{\isaliteral{7C}{\isacharbar}}}   & \isa{false} \\
       
   571             & \isa{{\isaliteral{7C}{\isacharbar}}}   & \isa{F\ {\isaliteral{5C3C616E643E}{\isasymand}}\ F} \\
       
   572             & \isa{{\isaliteral{7C}{\isacharbar}}}   & \isa{F\ {\isaliteral{5C3C6F723E}{\isasymor}}\ F} \\
       
   573             & \isa{{\isaliteral{7C}{\isacharbar}}}   & \isa{F\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F}       & \textcolor{black}{implies}\\
       
   574             & \isa{{\isaliteral{7C}{\isacharbar}}}   & \isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ F}       & \textcolor{black}{negation}\\
       
   575             & \isa{{\isaliteral{7C}{\isacharbar}}}   & \isa{p\ {\isaliteral{28}{\isacharparenleft}}t\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}t\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}} & \textcolor{black}{predicates}\\
       
   576    & \onslide<2->{\isa{{\isaliteral{7C}{\isacharbar}}}} & \onslide<2->{\isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ F}} & 
       
   577         \onslide<2->{\textcolor{black}{forall quantification}}\\
       
   578    & \onslide<2->{\isa{{\isaliteral{7C}{\isacharbar}}}} & \onslide<2->{\isa{{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ F}} & 
       
   579         \onslide<2->{\textcolor{black}{exists quantification}}\\[-7mm]
       
   580   \end{tabular}
       
   581   \end{center}
       
   582 
       
   583   \end{itemize}
       
   584 
       
   585   \begin{textblock}{12}(1,14)
       
   586   Terms \textcolor{blue}{\isa{t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{7C}{\isacharbar}}\ c\ {\isaliteral{5C3C646F74733E}{\isasymdots}}}}
       
   587   \end{textblock}
       
   588   
       
   589   \end{frame}}
       
   590   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   591 %
       
   592 
       
   593 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   594   \mode<presentation>{
       
   595   \begin{frame}[c]
       
   596 
       
   597 {\lstset{language=Scala}\fontsize{10}{12}\selectfont
       
   598 \texttt{\lstinputlisting{../programs/formulas.scala}}}
       
   599 
       
   600   \end{frame}}
       
   601   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
       
   602 
       
   603 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   604   \mode<presentation>{
       
   605   \begin{frame}[t]
       
   606   \frametitle{Judgements}
       
   607 
       
   608   \begin{center}
       
   609   \LARGE
       
   610   \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}
       
   611   \end{center}
       
   612 
       
   613   \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}}} is a collection of formulas, called the \alert{assumptions}\bigskip\pause
       
   614 
       
   615   \begin{itemize}
       
   616   \item Example\mbox{}\\[-3mm]
       
   617 
       
   618   \only<2>{\begin{center}\tiny
       
   619   \textcolor{blue}{
       
   620   \begin{tabular}{l}
       
   621   \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\
       
   622   \isa{is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\
       
   623   \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}}\\
       
   624   \end{tabular}\isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}
       
   625   \end{center}}
       
   626   \only<3>{\small
       
   627   \textcolor{blue}{
       
   628   \begin{center}
       
   629   \mbox{
       
   630   \infer{\mbox{\isa{may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}}
       
   631   {\mbox{\begin{tabular}{@ {}l@ {}}
       
   632   \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\\
       
   633   \isa{is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\\
       
   634   \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}}\\
       
   635   \end{tabular}}
       
   636   }
       
   637   }
       
   638   \end{center}
       
   639   }}
       
   640   \only<4>{\small
       
   641   \textcolor{blue}{
       
   642   \begin{center}
       
   643   \mbox{
       
   644   \infer{\mbox{\isa{may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Alice{\isaliteral{29}{\isacharparenright}}}}}
       
   645   {\mbox{\begin{tabular}{@ {}l@ {}}
       
   646   \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Alice{\isaliteral{29}{\isacharparenright}}}\\
       
   647   \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\\
       
   648   \isa{is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\\
       
   649   \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}}\\
       
   650   \end{tabular}}
       
   651   }
       
   652   }
       
   653   \end{center}
       
   654   }}
       
   655 
       
   656   \end{itemize}
       
   657 
       
   658   \end{frame}}
       
   659   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   660 
       
   661 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   662   \mode<presentation>{
       
   663   \begin{frame}[c]
       
   664 
       
   665 {\lstset{language=Scala}\fontsize{10}{12}\selectfont
       
   666 \texttt{\lstinputlisting{../programs/judgement.scala}}}
       
   667 
       
   668   \end{frame}}
       
   669   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
       
   670 
       
   671 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   672   \mode<presentation>{
       
   673   \begin{frame}[t]
       
   674   \frametitle{Inference Rules}
       
   675 
       
   676   \textcolor{blue}{
       
   677   \begin{center}
       
   678   \Large
       
   679   \mbox{
       
   680   \infer{\mbox{\isa{conclusion}}}
       
   681         {\mbox{\isa{premise\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}} & \mbox{\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}} & \mbox{\isa{premise\isaliteral{5C3C5E697375623E}{}\isactrlisub n}}}}
       
   682   \end{center}}
       
   683 
       
   684   The conlusion and premises are judgements\bigskip\pause
       
   685 
       
   686   \begin{itemize}
       
   687   \item Examples
       
   688   \textcolor{blue}{
       
   689   \begin{center}
       
   690   \mbox{
       
   691   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}
       
   692         {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}}
       
   693   \end{center}}\pause
       
   694 
       
   695   \textcolor{blue}{
       
   696   \begin{center}
       
   697   \mbox{
       
   698   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}
       
   699         {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}}}
       
   700   \hspace{10mm}
       
   701   \mbox{
       
   702   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}
       
   703         {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}}
       
   704   \end{center}}
       
   705   \end{itemize}
       
   706 
       
   707   \end{frame}}
       
   708   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   709 %
       
   710 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   711   \mode<presentation>{
       
   712   \begin{frame}[t]
       
   713   \frametitle{Implication}
       
   714   \Large
       
   715 
       
   716   \textcolor{blue}{
       
   717   \begin{center}
       
   718   \mbox{
       
   719   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}
       
   720         {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}{\isaliteral{2C}{\isacharcomma}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}}
       
   721   \end{center}}
       
   722 
       
   723   \textcolor{blue}{
       
   724   \begin{center}
       
   725   \mbox{
       
   726   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}
       
   727         {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}}}
       
   728   \end{center}}
       
   729 
       
   730   \end{frame}}
       
   731   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   732 %
       
   733 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   734   \mode<presentation>{
       
   735   \begin{frame}[t]
       
   736   \frametitle{Universal Quantification}
       
   737   \Large
       
   738 
       
   739   \textcolor{blue}{
       
   740   \begin{center}
       
   741   \mbox{
       
   742   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F{\isaliteral{5B}{$\isacharbrackleft$}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{5D}{$\isacharbrackright$}}}}}
       
   743         {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ F}}}}
       
   744   \end{center}}
       
   745 
       
   746   \end{frame}}
       
   747   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   748 %
       
   749 
       
   750 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   751   \mode<presentation>{
       
   752   \begin{frame}[t]
       
   753   \frametitle{Start Rules / Axioms}
       
   754 
       
   755   \normalsize
       
   756   \alert{if \textcolor{blue}{\isa{F\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}}}}
       
   757   
       
   758   \textcolor{blue}{\Large
       
   759   \begin{center}
       
   760   \mbox{
       
   761   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}{}}
       
   762   \end{center}}\bigskip\pause
       
   763 
       
   764   \normalsize
       
   765   Also written as:
       
   766   \textcolor{blue}{\Large
       
   767   \begin{center}
       
   768   \mbox{
       
   769   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}{\isaliteral{2C}{\isacharcomma}}\ F\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}{}}
       
   770   \end{center}}\pause
       
   771 
       
   772   \textcolor{blue}{\Large
       
   773   \begin{center}
       
   774   \mbox{
       
   775   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ true}}}{}}
       
   776   \end{center}}
       
   777 
       
   778   \end{frame}}
       
   779   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   780 %
       
   781 
       
   782 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   783   \mode<presentation>{
       
   784   \begin{frame}[t]
       
   785   \frametitle{}
       
   786  
       
   787  \begin{minipage}{1.1\textwidth}
       
   788   Let \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\footnotesize\begin{tabular}{l}
       
   789   \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\
       
   790   \isa{is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\
       
   791   \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}}\\
       
   792   \end{tabular}}
       
   793   \end{minipage}
       
   794 
       
   795   \only<2>{
       
   796   \begin{textblock}{12}(4,3)\footnotesize
       
   797   \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}\hspace{10mm}
       
   798   \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}
       
   799   \end{textblock}}
       
   800 
       
   801   \only<3->{
       
   802   \begin{textblock}{12}(4,3)\footnotesize
       
   803   \mbox{\textcolor{blue}{
       
   804   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}}
       
   805   {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}} &\hspace{10mm}
       
   806    \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}}
       
   807   }}
       
   808   \end{textblock}}
       
   809 
       
   810   \only<4>{
       
   811   \begin{textblock}{14}(0.5,6)\footnotesize
       
   812   \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}}}
       
   813   \end{textblock}}
       
   814 
       
   815   \only<5->{
       
   816   \begin{textblock}{14}(0.5,6)\footnotesize
       
   817   \textcolor{blue}{
       
   818   \infer{\mbox{\begin{tabular}{l}\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\\ 
       
   819            \hspace{40mm}\isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}\end{tabular}}}
       
   820         {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}}}}}
       
   821   \end{textblock}}
       
   822 
       
   823   \only<6->{
       
   824   \begin{textblock}{14}(5,10)\footnotesize
       
   825   \textcolor{blue}{
       
   826   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}}
       
   827         {\vdots & \hspace{30mm} \vdots}}
       
   828   \end{textblock}}
       
   829 
       
   830   \end{frame}}
       
   831   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   832 %
       
   833 
       
   834 
       
   835 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   836   \mode<presentation>{
       
   837   \begin{frame}[t]
       
   838   \frametitle{Access Control}
       
   839   \Large
       
   840 
       
   841   \textcolor{blue}{
       
   842   \begin{center}
       
   843   \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}
       
   844   \end{center}}\bigskip
       
   845 
       
   846   \normalsize
       
   847   \begin{itemize}
       
   848   \item If there is a proof \isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}} yes (granted)
       
   849   \item If there isn't \isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}} no (denied)
       
   850   \end{itemize}\bigskip\pause
       
   851 
       
   852 \begin{minipage}{1.1\textwidth}	
       
   853   \small
       
   854   \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\small\begin{tabular}{l}
       
   855   \isa{is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\
       
   856   \isa{is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}},\\
       
   857   \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ is{\isaliteral{5F}{\isacharunderscore}}at{\isaliteral{5F}{\isacharunderscore}}library\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}}\\
       
   858   \end{tabular}}\medskip
       
   859   
       
   860   \textcolor{blue}{
       
   861   \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}} $\not\vdash$ \isa{may{\isaliteral{5F}{\isacharunderscore}}obtain{\isaliteral{5F}{\isacharunderscore}}email\ {\isaliteral{28}{\isacharparenleft}}Alice{\isaliteral{29}{\isacharparenright}}}}}
       
   862 \end{minipage}
       
   863   \end{frame}}
       
   864   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   865 %
       
   866 
       
   867 
       
   868 
       
   869 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   870 \mode<presentation>{
       
   871 \begin{frame}[c]
       
   872 \frametitle{The Access Control Problem}
       
   873 
       
   874 
       
   875 \begin{center}
       
   876   \begin{tikzpicture}[scale=1]
       
   877   
       
   878   \draw[line width=1mm] (-.3, 0) rectangle (1.5,2);
       
   879   \draw (-2.7,1) node {\begin{tabular}{l}access\\request\\ (\bl{$F$})\end{tabular}};
       
   880   \draw (4.2,1) node {\begin{tabular}{l}granted/\\not granted\end{tabular}};
       
   881   \draw (0.6,1.2) node {\footnotesize \begin{tabular}{l}Access\\Control\\Checker\end{tabular}};
       
   882  
       
   883   \draw[red, ->, line width = 2mm] (1.7,1) -- (2.7,1); 
       
   884   \draw[red,<-, line width = 2mm] (-0.6,1) -- (-1.6,1);
       
   885   \draw[red, <-, line width = 3mm] (0.6,2.2) -- (0.6,3.2); 
       
   886   
       
   887   \draw (0.6,4) node {\begin{tabular}{l}\large Access Policy (\bl{$\Gamma$})\end{tabular}};
       
   888 
       
   889   \end{tikzpicture}
       
   890 \end{center}
       
   891 
       
   892 \end{frame}}
       
   893 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
   894 
       
   895 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   896   \mode<presentation>{
       
   897   \begin{frame}[c]
       
   898   \frametitle{Bad News}
       
   899   
       
   900   \begin{itemize}
       
   901   \item We introduced (roughly) first-order logic. \bigskip\pause
       
   902 
       
   903   \item Judgements
       
   904   \begin{center}
       
   905   \textcolor{blue}
       
   906   {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}
       
   907   \end{center}
       
   908 
       
   909   are in general \alert{undecidable}.\pause\medskip\\ 
       
   910  
       
   911   The problem is \alert{semi-decidable}.
       
   912  
       
   913   \end{itemize}
       
   914 
       
   915 
       
   916   \end{frame}}
       
   917   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   918 %
       
   919 
       
   920 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   921   \mode<presentation>{
       
   922   \begin{frame}[t]
       
   923   \frametitle{\Large\begin{tabular}{@ {}c@ {}}Access Control Logic\end{tabular}}
       
   924   
       
   925   \begin{itemize}
       
   926   \item[]
       
   927   
       
   928   \begin{center}\color{blue}
       
   929   \begin{tabular}[t]{rcl@ {\hspace{10mm}}l}
       
   930   \isa{F} & \isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}} & \isa{true} \\
       
   931             & \isa{{\isaliteral{7C}{\isacharbar}}} & \isa{false} \\
       
   932             & \isa{{\isaliteral{7C}{\isacharbar}}}   & \isa{F\ {\isaliteral{5C3C616E643E}{\isasymand}}\ F} \\
       
   933             & \isa{{\isaliteral{7C}{\isacharbar}}}   & \isa{F\ {\isaliteral{5C3C6F723E}{\isasymor}}\ F} \\
       
   934             & \isa{{\isaliteral{7C}{\isacharbar}}}   & \isa{F\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F}\\
       
   935             & \isa{{\isaliteral{7C}{\isacharbar}}}   & \isa{p\ {\isaliteral{28}{\isacharparenleft}}t\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}t\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}} \\  
       
   936             & \isa{{\isaliteral{7C}{\isacharbar}}}   & \alert{\isa{P\ says\ F}} & \textcolor{black}{``saying predicate''}\\ 
       
   937   \end{tabular}
       
   938   \end{center}\medskip
       
   939 
       
   940   where \textcolor{blue}{\isa{P\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ Alice{\isaliteral{2C}{\isacharcomma}}\ Bob{\isaliteral{2C}{\isacharcomma}}\ Christian{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}}} (principals)\bigskip\pause
       
   941   
       
   942   \item \textcolor{blue}{\isa{HoD\ says\ is{\isaliteral{5F}{\isacharunderscore}}staff\ {\isaliteral{28}{\isacharparenleft}}Christian{\isaliteral{29}{\isacharparenright}}}}
       
   943   \end{itemize}
       
   944   
       
   945 
       
   946   
       
   947   \end{frame}}
       
   948   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   949 %
       
   950 
       
   951 
       
   952 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   953   \mode<presentation>{
       
   954   \begin{frame}[c]
       
   955 
       
   956 {\lstset{language=Scala}\fontsize{10}{12}\selectfont
       
   957 \texttt{\lstinputlisting{../programs/formulas1.scala}}}
       
   958 
       
   959   \end{frame}}
       
   960   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
       
   961 
       
   962 
       
   963 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   964   \mode<presentation>{
       
   965   \begin{frame}[t]
       
   966   \frametitle{Rules about Says}
       
   967 
       
   968   \textcolor{blue}{
       
   969   \begin{center}
       
   970   \mbox{
       
   971   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}}
       
   972         {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}}
       
   973   \end{center}}
       
   974 
       
   975   \textcolor{blue}{
       
   976   \begin{center}
       
   977   \mbox{
       
   978   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}
       
   979         {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ {\isaliteral{28}{\isacharparenleft}}F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}} & \hspace{10mm}\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}}}
       
   980   \end{center}}
       
   981 
       
   982   \textcolor{blue}{
       
   983   \begin{center}
       
   984   \mbox{
       
   985   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}}
       
   986         {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ {\isaliteral{28}{\isacharparenleft}}P\ says\ F{\isaliteral{29}{\isacharparenright}}}}}}
       
   987   \end{center}}
       
   988 
       
   989   \end{frame}}
       
   990   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   991 %
       
   992 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   993   \mode<presentation>{
       
   994   \begin{frame}[c]
       
   995   \frametitle{}
       
   996 
       
   997   Consider the following scenario:
       
   998 
       
   999   \begin{itemize}
       
  1000   \item If \textcolor{blue}{Admin} says that \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}} 
       
  1001   should be deleted, then this file must be deleted.
       
  1002   \item \textcolor{blue}{Admin} trusts \textcolor{blue}{Bob} to decide whether 
       
  1003   \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}} should be deleted.
       
  1004   \item \textcolor{blue}{Bob} wants to delete \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}.
       
  1005   \end{itemize}\bigskip\pause
       
  1006 
       
  1007   \small
       
  1008   \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\small\begin{tabular}{l}
       
  1009   \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}},\\
       
  1010   \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}},\\
       
  1011   \isa{Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}\\
       
  1012   \end{tabular}}\medskip\pause
       
  1013 
       
  1014   \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}
       
  1015   \end{frame}}
       
  1016   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1017 %
       
  1018 
       
  1019 
       
  1020 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1021   \mode<presentation>{
       
  1022   \begin{frame}[c]
       
  1023   \frametitle{}
       
  1024 
       
  1025   \textcolor{blue}{
       
  1026   \begin{center}
       
  1027   \mbox{
       
  1028   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}}
       
  1029         {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}}\\\bigskip
       
  1030   \mbox{
       
  1031   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}}}
       
  1032         {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ {\isaliteral{28}{\isacharparenleft}}F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}} & \hspace{5mm}\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}}}
       
  1033   \end{center}}\bigskip
       
  1034 
       
  1035   \small
       
  1036   \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\small\begin{tabular}{l}
       
  1037   \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}},\\
       
  1038   \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}},\\
       
  1039   \isa{Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}\\
       
  1040   \end{tabular}}\medskip
       
  1041 
       
  1042   \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}
       
  1043   \end{frame}}
       
  1044   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1045 %
       
  1046 
       
  1047 
       
  1048 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1049   \mode<presentation>{
       
  1050   \begin{frame}[t]
       
  1051   \frametitle{}
       
  1052   \small
       
  1053 
       
  1054   \textcolor{blue}{
       
  1055   \begin{center}
       
  1056   \only<1>{$ \underbrace{
       
  1057   \mbox{\infer{\Gamma \vdash \mbox{Admin says (Bob says del\_file)}}
       
  1058   {\infer{\Gamma \vdash \mbox{Bob says del\_file}}{}}}}_{X}$}
       
  1059   \end{center}}
       
  1060 
       
  1061   \textcolor{blue}{
       
  1062   \begin{center}
       
  1063   \only<1>{
       
  1064   $ \underbrace{
       
  1065   \mbox{\infer{\Gamma \vdash \mbox{Admin says del\_file}}
       
  1066   {\infer{\Gamma \vdash \mbox{Admin says (Bob says del\_file \isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}} del\_file)}}{}
       
  1067    &
       
  1068    \deduce[$\vdots$]{X}{}
       
  1069   }}}_{Y}$}
       
  1070   \end{center}}
       
  1071 
       
  1072   \textcolor{blue}{
       
  1073   \begin{center}
       
  1074   \only<1>{\mbox{\infer{\Gamma \vdash \mbox{del\_file}}
       
  1075   {\infer{\Gamma \vdash \mbox{(Admin says del\_file) \isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}} del\_file}}{}
       
  1076    &
       
  1077    \deduce[$\vdots$]{Y}{}
       
  1078   }}}
       
  1079   \end{center}}
       
  1080 
       
  1081   \end{frame}}
       
  1082   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1083 %
       
  1084 
       
  1085 
       
  1086 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1087   \mode<presentation>{
       
  1088   \begin{frame}[c]
       
  1089   \frametitle{Controls}
       
  1090   \small
       
  1091   
       
  1092   \begin{itemize}
       
  1093   \item \bl{\isa{P\ controls\ F\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{28}{\isacharparenleft}}P\ says\ F{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F}}
       
  1094 
       
  1095   \item its meaning ``\bl{P} is entitled to do \bl{F}''
       
  1096   \item if \bl{P controls F} and \bl{P says F} then \bl{F}\pause
       
  1097 
       
  1098   \begin{center}
       
  1099   \bl{\mbox{
       
  1100   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}
       
  1101         {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ controls\ F}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}}
       
  1102   }}
       
  1103   \end{center}\pause
       
  1104 
       
  1105   \begin{center}
       
  1106   \bl{\mbox{
       
  1107   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ F}}}
       
  1108         {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{28}{\isacharparenleft}}P\ says\ F{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ F}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}}
       
  1109   }}
       
  1110   \end{center}
       
  1111   \end{itemize}
       
  1112 
       
  1113   \end{frame}}
       
  1114   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1115 %
       
  1116 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1117   \mode<presentation>{
       
  1118   \begin{frame}[c]
       
  1119   \frametitle{Speaks For}
       
  1120   \small
       
  1121   
       
  1122   \begin{itemize}
       
  1123   \item \bl{\isa{P\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ Q\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}F{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}P\ says\ F{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}Q\ says\ F{\isaliteral{29}{\isacharparenright}}}}
       
  1124 
       
  1125   \item its meaning ``\bl{P} speaks for \bl{Q}''
       
  1126   
       
  1127 
       
  1128   \begin{center}
       
  1129   \bl{\mbox{
       
  1130   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ Q\ says\ F}}}
       
  1131         {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ Q}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ says\ F}}}
       
  1132   }}
       
  1133   \end{center}\pause
       
  1134 
       
  1135   \begin{center}
       
  1136   \bl{\mbox{
       
  1137   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ controls\ F}}}
       
  1138         {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ Q}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ Q\ controls\ F}}}
       
  1139   }}
       
  1140   \end{center}
       
  1141 
       
  1142   \begin{center}
       
  1143   \bl{\mbox{
       
  1144   \infer{\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ R}}}
       
  1145         {\mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ P\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ Q}} & \mbox{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ Q\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ R}}}
       
  1146   }}
       
  1147   \end{center}
       
  1148   \end{itemize}
       
  1149 
       
  1150   \end{frame}}
       
  1151   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1152 %
       
  1153 
       
  1154 
       
  1155 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1156   \mode<presentation>{
       
  1157   \begin{frame}[c]
       
  1158   \frametitle{Security Levels}
       
  1159   \small
       
  1160 
       
  1161   \begin{itemize}
       
  1162   \item Top secret (\bl{$T\!S$})
       
  1163   \item Secret (\bl{$S$})
       
  1164   \item Public (\bl{$P$})
       
  1165   \end{itemize}
       
  1166 
       
  1167   \begin{center}
       
  1168   \bl{$slev(P) < slev(S) < slev(T\!S)$}\pause
       
  1169   \end{center}
       
  1170 
       
  1171   \begin{itemize}
       
  1172   \item Bob has a clearance for ``secret''
       
  1173   \item Bob can read documents that are public or sectret, but not top secret
       
  1174   \end{itemize}
       
  1175 
       
  1176   \end{frame}}
       
  1177   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1178 %
       
  1179 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1180   \mode<presentation>{
       
  1181   \begin{frame}[c]
       
  1182   \frametitle{Reading a File}
       
  1183 
       
  1184   \bl{\begin{center}
       
  1185   \begin{tabular}{c}
       
  1186   \begin{tabular}{@ {}l@ {}}
       
  1187   \only<2->{\textcolor{red}{$slev($File$)$ $<$ $slev($Bob$)$ $\Rightarrow$}}\\ 
       
  1188   \only<2->{\hspace{3cm}}Bob controls Permitted $($File, read$)$\\
       
  1189   Bob says Permitted $($File, read$)$\only<2->{\\}
       
  1190   \only<2>{\textcolor{red}{$slev($File$)$ $<$ $slev($Bob$)$}}%
       
  1191   \only<3>{\textcolor{red}{$slev($File$)$ $=$ $P$}\\}%
       
  1192   \only<3>{\textcolor{red}{$slev($Bob$)$ $=$ $S$}\\}%
       
  1193   \only<3>{\textcolor{red}{$slev(P)$ $<$ $slev(S)$}\\}%
       
  1194   \end{tabular}\\
       
  1195   \hline
       
  1196   Permitted $($File, read$)$
       
  1197   \end{tabular}
       
  1198   \end{center}}
       
  1199 
       
  1200   \end{frame}}
       
  1201   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1202 %
       
  1203 
       
  1204 
       
  1205 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1206   \mode<presentation>{
       
  1207   \begin{frame}[c]
       
  1208   \frametitle{Substitution Rule}
       
  1209   \small
       
  1210   
       
  1211   \bl{\begin{center}
       
  1212   \begin{tabular}{c}
       
  1213   $\Gamma \vdash slev(P) = l_1$ \hspace{4mm} $\Gamma \vdash slev(Q) = l_2$
       
  1214   \hspace{4mm} $\Gamma \vdash l_1 < l_2$\\\hline
       
  1215   $\Gamma \vdash slev(P) < slev(Q)$
       
  1216   \end{tabular}
       
  1217   \end{center}}\bigskip\pause
       
  1218 
       
  1219   \begin{itemize}
       
  1220   \item \bl{$slev($Bob$)$ $=$ $S$}
       
  1221   \item \bl{$slev($File$)$ $=$ $P$}
       
  1222   \item \bl{$slev(P) < slev(S)$}
       
  1223   \end{itemize}
       
  1224 
       
  1225   \end{frame}}
       
  1226   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1227 %
       
  1228 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1229   \mode<presentation>{
       
  1230   \begin{frame}[c]
       
  1231   \frametitle{Reading a File}
       
  1232 
       
  1233   \bl{\begin{center}
       
  1234   \begin{tabular}{c}
       
  1235   \begin{tabular}{@ {}l@ {}}
       
  1236   $slev($File$)$ $<$ $slev($Bob$)$ $\Rightarrow$\\ 
       
  1237   \hspace{3cm}Bob controls Permitted $($File, read$)$\\
       
  1238   Bob says Permitted $($File, read$)$\\
       
  1239   $slev($File$)$ $=$ $P$\\
       
  1240   $slev($Bob$)$ $=$ $T\!S$\\
       
  1241   \only<1>{\textcolor{red}{$?$}}%
       
  1242   \only<2>{\textcolor{red}{$slev(P) < slev(S)$}\\}%
       
  1243   \only<2>{\textcolor{red}{$slev(S) < slev(T\!S)$}}%
       
  1244   \end{tabular}\\
       
  1245   \hline
       
  1246   Permitted $($File, read$)$
       
  1247   \end{tabular}
       
  1248   \end{center}}
       
  1249 
       
  1250   \end{frame}}
       
  1251   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1252 %
       
  1253 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1254   \mode<presentation>{
       
  1255   \begin{frame}[c]
       
  1256   \frametitle{Transitivity Rule}
       
  1257   \small
       
  1258   
       
  1259   \bl{\begin{center}
       
  1260   \begin{tabular}{c}
       
  1261   $\Gamma \vdash l_1 < l_2$ 
       
  1262   \hspace{4mm} $\Gamma \vdash l_2 < l_3$\\\hline
       
  1263   $\Gamma \vdash l_1 < l_3$
       
  1264   \end{tabular}
       
  1265   \end{center}}\bigskip
       
  1266 
       
  1267   \begin{itemize}
       
  1268   \item \bl{$slev(P) < slev (S)$}
       
  1269   \item \bl{$slev(S) < slev (T\!S)$}
       
  1270   \item[] \bl{$slev(P) < slev (T\!S)$}
       
  1271   \end{itemize}
       
  1272 
       
  1273   \end{frame}}
       
  1274   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1275 %
       
  1276 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1277   \mode<presentation>{
       
  1278   \begin{frame}[c]
       
  1279   \frametitle{Reading Files}
       
  1280 
       
  1281   \begin{itemize}
       
  1282   \item Access policy for reading
       
  1283   \end{itemize}
       
  1284 
       
  1285   \bl{\begin{center}
       
  1286   \begin{tabular}{c}
       
  1287   \begin{tabular}{@ {}l@ {}}
       
  1288   $\forall f.\;slev(f)$ \only<1>{$<$}\only<2>{\textcolor{red}{$\le$}} $slev($Bob$)$ $\Rightarrow$\\ 
       
  1289   \hspace{3cm}Bob controls Permitted $(f$, read$)$\\
       
  1290   Bob says Permitted $($File, read$)$\\
       
  1291   $slev($File$)$ $=$ \only<1>{$P$}\only<2>{\textcolor{red}{$T\!S$}}\\
       
  1292   $slev($Bob$)$ $=$ $T\!S$\\
       
  1293   $slev(P) < slev(S)$\\
       
  1294   $slev(S) < slev(T\!S)$
       
  1295   \end{tabular}\\
       
  1296   \hline
       
  1297   Permitted $($File, read$)$
       
  1298   \end{tabular}
       
  1299   \end{center}}
       
  1300 
       
  1301   \end{frame}}
       
  1302   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1303 %
       
  1304 
       
  1305 
       
  1306 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1307   \mode<presentation>{
       
  1308   \begin{frame}[c]
       
  1309   \frametitle{Writing Files}
       
  1310 
       
  1311   \begin{itemize}
       
  1312   \item Access policy for \underline{writing}
       
  1313   \end{itemize}
       
  1314 
       
  1315   \bl{\begin{center}
       
  1316   \begin{tabular}{c}
       
  1317   \begin{tabular}{@ {}l@ {}}
       
  1318   $\forall f.\;slev($Bob$)$ $\le$ $slev(f)$ $\Rightarrow$\\ 
       
  1319   \hspace{3cm}Bob controls Permitted $(f$, write$)$\\
       
  1320   Bob says Permitted $($File, write$)$\\
       
  1321   $slev($File$)$ $=$ $T\!S$\\
       
  1322   $slev($Bob$)$ $=$ $S$\\
       
  1323   $slev(P) < slev(S)$\\
       
  1324   $slev(S) < slev(T\!S)$
       
  1325   \end{tabular}\\
       
  1326   \hline
       
  1327   Permitted $($File, write$)$
       
  1328   \end{tabular}
       
  1329   \end{center}}
       
  1330 
       
  1331   \end{frame}}
       
  1332   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1333 %
   553 
  1334 
   554 \end{document}
  1335 \end{document}
   555 
  1336 
   556 %%% Local Variables:  
  1337 %%% Local Variables:  
   557 %%% mode: latex
  1338 %%% mode: latex