--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/slides/slides10.tex Sun Sep 22 15:22:11 2013 +0100
@@ -0,0 +1,217 @@
+\documentclass[dvipsnames,14pt,t]{beamer}
+\usepackage{proof}
+\usepackage{beamerthemeplainculight}
+\usepackage[T1]{fontenc}
+\usepackage[latin1]{inputenc}
+\usepackage{mathpartir}
+\usepackage{isabelle}
+\usepackage{isabellesym}
+\usepackage[absolute,overlay]{textpos}
+\usepackage{ifthen}
+\usepackage{tikz}
+\usepackage{courier}
+\usepackage{listings}
+\usetikzlibrary{arrows}
+\usetikzlibrary{positioning}
+\usetikzlibrary{calc}
+\usepackage{graphicx}
+\usetikzlibrary{shapes}
+\usetikzlibrary{shadows}
+\usetikzlibrary{plotmarks}
+
+
+\isabellestyle{rm}
+\renewcommand{\isastyle}{\rm}%
+\renewcommand{\isastyleminor}{\rm}%
+\renewcommand{\isastylescript}{\footnotesize\rm\slshape}%
+\renewcommand{\isatagproof}{}
+\renewcommand{\endisatagproof}{}
+\renewcommand{\isamarkupcmt}[1]{#1}
+
+% Isabelle characters
+\renewcommand{\isacharunderscore}{\_}
+\renewcommand{\isacharbar}{\isamath{\mid}}
+\renewcommand{\isasymiota}{}
+\renewcommand{\isacharbraceleft}{\{}
+\renewcommand{\isacharbraceright}{\}}
+\renewcommand{\isacharless}{$\langle$}
+\renewcommand{\isachargreater}{$\rangle$}
+\renewcommand{\isasymsharp}{\isamath{\#}}
+\renewcommand{\isasymdots}{\isamath{...}}
+\renewcommand{\isasymbullet}{\act}
+
+
+
+\definecolor{javared}{rgb}{0.6,0,0} % for strings
+\definecolor{javagreen}{rgb}{0.25,0.5,0.35} % comments
+\definecolor{javapurple}{rgb}{0.5,0,0.35} % keywords
+\definecolor{javadocblue}{rgb}{0.25,0.35,0.75} % javadoc
+
+\lstset{language=Java,
+ basicstyle=\ttfamily,
+ keywordstyle=\color{javapurple}\bfseries,
+ stringstyle=\color{javagreen},
+ commentstyle=\color{javagreen},
+ morecomment=[s][\color{javadocblue}]{/**}{*/},
+ numbers=left,
+ numberstyle=\tiny\color{black},
+ stepnumber=1,
+ numbersep=10pt,
+ tabsize=2,
+ showspaces=false,
+ showstringspaces=false}
+
+\lstdefinelanguage{scala}{
+ morekeywords={abstract,case,catch,class,def,%
+ do,else,extends,false,final,finally,%
+ for,if,implicit,import,match,mixin,%
+ new,null,object,override,package,%
+ private,protected,requires,return,sealed,%
+ super,this,throw,trait,true,try,%
+ type,val,var,while,with,yield},
+ otherkeywords={=>,<-,<\%,<:,>:,\#,@},
+ sensitive=true,
+ morecomment=[l]{//},
+ morecomment=[n]{/*}{*/},
+ morestring=[b]",
+ morestring=[b]',
+ morestring=[b]"""
+}
+
+\lstset{language=Scala,
+ basicstyle=\ttfamily,
+ keywordstyle=\color{javapurple}\bfseries,
+ stringstyle=\color{javagreen},
+ commentstyle=\color{javagreen},
+ morecomment=[s][\color{javadocblue}]{/**}{*/},
+ numbers=left,
+ numberstyle=\tiny\color{black},
+ stepnumber=1,
+ numbersep=10pt,
+ tabsize=2,
+ showspaces=false,
+ showstringspaces=false}
+
+% beamer stuff
+\renewcommand{\slidecaption}{APP 09, King's College London, 27 November 2012}
+\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions
+\newcommand{\bl}[1]{\textcolor{blue}{#1}}
+
+\begin{document}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}<1>[t]
+\frametitle{%
+ \begin{tabular}{@ {}c@ {}}
+ \\
+ \LARGE Access Control and \\[-3mm]
+ \LARGE Privacy Policies (10)\\[-6mm]
+ \end{tabular}}\bigskip\bigskip\bigskip
+
+ %\begin{center}
+ %\includegraphics[scale=1.3]{pics/barrier.jpg}
+ %\end{center}
+
+\normalsize
+ \begin{center}
+ \begin{tabular}{ll}
+ Email: & christian.urban at kcl.ac.uk\\
+ Of$\!$fice: & S1.27 (1st floor Strand Building)\\
+ Slides: & KEATS (also homework is there)\\
+ \end{tabular}
+ \end{center}
+
+\end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Revision: Proofs}
+
+\begin{center}
+\includegraphics[scale=0.4]{pics/river-stones.jpg}
+\end{center}
+
+\begin{textblock}{5}(11.7,5)
+goal
+\end{textblock}
+
+\begin{textblock}{5}(11.7,14)
+start
+\end{textblock}
+
+\begin{textblock}{5}(0,7)
+\begin{center}
+\bl{\infer[\small\textcolor{black}{\text{axiom}}]{\quad\vdash\quad}{}}\\[8mm]
+\bl{\infer{\vdash}{\quad\vdash\quad}}\\[8mm]
+\bl{\infer{\vdash}{\quad\vdash\qquad\vdash\quad}}
+\end{center}
+\end{textblock}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Proof Example Proof}
+
+\begin{center}
+\bl{\infer{P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2 \wedge P\;\text{says}\;F_1}
+ {\raisebox{2mm}{\text{\LARGE $?$}}}}
+\end{center}
+
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Proof Example Proof}
+
+\begin{tabular}{@{\hspace{-6mm}}l}
+\begin{minipage}{1.1\textwidth}
+We have (by axiom)
+
+\begin{center}
+\begin{tabular}{@{}ll@{}}
+(1) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2$}
+\end{tabular}
+\end{center}
+
+From (1) we get
+
+\begin{center}
+\begin{tabular}{@{}ll@{}}
+(2) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash P\;\text{says}\;F_1$}\\
+(3) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2$}\\
+\end{tabular}
+\end{center}
+
+From (3) and (2) we get
+
+\begin{center}
+\begin{tabular}{@{}ll@{}}
+\bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2 \wedge P\;\text{says}\;F_1$}
+\end{tabular}
+\end{center}
+
+Done.
+\end{minipage}
+\end{tabular}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
+