% $Id: root.tex,v 1.2 2007-11-12 21:00:45 nipkow Exp $

\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym}

% further packages required for unusual symbols (see also isabellesym.sty)
% use only when needed
\usepackage{amssymb}                  % for \<leadsto>, \<box>, \<diamond>,
                                       % \<sqsupset>, \<mho>, \<Join>, 
                                       % \<lhd>, \<lesssim>, \<greatersim>,
                                       % \<lessapprox>, \<greaterapprox>,
                                       % \<triangleq>, \<yen>, \<lozenge>
%\usepackage[greek,english]{babel}     % greek for \<euro>,
                                       % english for \<guillemotleft>, 
                                       %             \<guillemotright>
                                       % default language = last
%\usepackage[latin1]{inputenc}         % for \<onesuperior>, \<onequarter>,
                                       % \<twosuperior>, \<onehalf>,
                                       % \<threesuperior>, \<threequarters>,
                                       % \<degree>
%\usepackage[only,bigsqcap]{stmaryrd}  % for \<Sqinter>
%\usepackage{eufrak}                   % for \<AA> ... \<ZZ>, \<aa> ... \<zz>
                                       % (only needed if amssymb not used)
%\usepackage{textcomp}                 % for \<cent>, \<currency>

% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}


\begin{document}

\title{Separation Algebra}
\author{Gerwin Klein and Rafal Kolanski and Andrew Boyton}
\maketitle

\begin{abstract}
We present a generic type class implementation of separation
algebra for Isabelle/HOL as well as lemmas and generic tactics which can
be used directly for any instantiation of the type class.

The ex directory contains example instantiations that include structures
such as a heap or virtual memory.

The abstract separation algebra is based upon ``Abstract Separation
Logic'' by Calcagno et al. These theories are also the basis of
``Mechanised Separation Algebra'' by the authors \cite{KleinKB-ITP12}.

The aim of this work is to support and significantly reduce the effort
for future separation logic developments in Isabelle/HOL by factoring
out the part of separation logic that can be treated abstractly once
and for all. This includes developing typical default rule sets for
reasoning as well as automated tactic support for separation logic.
\end{abstract}

\tableofcontents

% include generated text of all theories
\input{session}

\bibliographystyle{abbrv}
\bibliography{root}

\end{document}