\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{isabelle,isabellesym}
\usepackage[american]{babel} % Language
\usepackage[defblank]{paralist} % for compact lists
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{stmaryrd}
\usepackage{verbatim}
\usepackage{dot2texi}
\usepackage{pdfpages}
\newtheorem{definition}{Definition}[section]
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}{Lemma}[section]
\newcommand{\definitionautorefname}{Definition}

% this should be the last package used
\usepackage{pdfsetup}
% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}

%========= DRAFT ONLY ===============
\makeatletter
\newcommand\CO[1]{%
  \@tempdima=\linewidth%
  \advance\@tempdima by -2\fboxsep%
  \advance\@tempdima by -2\fboxrule%
  \leavevmode\par\noindent%
  \fbox{\parbox{\the\@tempdima}{\small\sf #1}}%
  \smallskip\par}
\newcommand\NOTE[2][Note]{%
    \leavevmode\marginpar{\raggedright\hangindent=1ex\small\textbf{#1: }#2}}
\newcommand\OLD[1]{%
    \slshape[\textbf{old: }\ignorespaces #1\unskip]}

%======= END DRAFT ONLY =============

\title{A Dependent Security Type System for Concurrent Imperative Programs}
\author{Toby Murray, Robert Sison, Edward Pierzchalski and Christine Rizkallah}
\begin{document}
\maketitle
% sane default for proof documents
\parindent 0pt\parskip 0.5ex

\begin{abstract}
  The paper ``Compositional Verification and Refinement of Concurrent Value-Dependent 
  Noninterference'' by Murray et. al. \cite{Murray_SPR_16}
  presents a dependent security type system for compositionally verifying a value-dependent
  noninterference property, defined in \cite{Murray_15}, for concurrent programs. This development 
  formalises that security definition, the type system
  and its soundness proof, and demonstrates its application on some small examples. 
  It was derived from the \texttt{SIFUM\_Type\_Systems} AFP entry~\cite{Grewe_MS_14}, by Sylvia Grewe, Heiko Mantel and Daniel Schoepe and
  which itself formalises the work in~\cite{Mantel_SS_11}, and whose structure it
  inherits.

The formalization includes the following parts:

\begin{compactitem}
\item Notion of Dependent SIFUM-security and preliminary concepts:\\
  \texttt{Preliminaries.thy}, \texttt{Security.thy}
\item Compositionality proof: \texttt{Compositionality.thy}
\item Example language: \texttt{Language.thy}
\item Type system for ensuring Dependent SIFUM-security and soundness proof: \\
  \texttt{TypeSystem.thy}
\item Type system for ensuring sound use of modes and soundness proof:
  \texttt{LocallySoundUseOfModes.thy}
\end{compactitem}

Examples are also present in the formalisation in the \texttt{Examples/} directory.

\end{abstract}

\tableofcontents

\input{Preliminaries.tex}

\input{Security.tex}

\input{Compositionality.tex}

\input{Language.tex}

\input{TypeSystem.tex}

\input{LocallySoundModeUse.tex}

\bibliography{root}
\bibliographystyle{alpha}
\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
