% $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}