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

     2 

     3 \documentclass[11pt,a4paper]{article}

     4 \usepackage{isabelle,isabellesym}

     5 

     6 % further packages required for unusual symbols (see also isabellesym.sty)

     7 % use only when needed

     8 \usepackage{amssymb}                  % for \<leadsto>, \<box>, \<diamond>,

     9                                        % \<sqsupset>, \<mho>, \<Join>, 

    10                                        % \<lhd>, \<lesssim>, \<greatersim>,

    11                                        % \<lessapprox>, \<greaterapprox>,

    12                                        % \<triangleq>, \<yen>, \<lozenge>

    13 %\usepackage[greek,english]{babel}     % greek for \<euro>,

    14                                        % english for \<guillemotleft>, 

    15                                        %             \<guillemotright>

    16                                        % default language = last

    17 %\usepackage[latin1]{inputenc}         % for \<onesuperior>, \<onequarter>,

    18                                        % \<twosuperior>, \<onehalf>,

    19                                        % \<threesuperior>, \<threequarters>,

    20                                        % \<degree>

    21 %\usepackage[only,bigsqcap]{stmaryrd}  % for \<Sqinter>

    22 %\usepackage{eufrak}                   % for \<AA> ... \<ZZ>, \<aa> ... \<zz>

    23                                        % (only needed if amssymb not used)

    24 %\usepackage{textcomp}                 % for \<cent>, \<currency>

    25 

    26 % this should be the last package used

    27 \usepackage{pdfsetup}

    28 

    29 % urls in roman style, theory text in math-similar italics

    30 \urlstyle{rm}

    31 \isabellestyle{it}

    32 

    33 

    34 \begin{document}

    35 

    36 \title{Separation Algebra}

    37 \author{Gerwin Klein and Rafal Kolanski and Andrew Boyton}

    38 \maketitle

    39 

    40 \begin{abstract}

    41 We present a generic type class implementation of separation

    42 algebra for Isabelle/HOL as well as lemmas and generic tactics which can

    43 be used directly for any instantiation of the type class.

    44 

    45 The ex directory contains example instantiations that include structures

    46 such as a heap or virtual memory.

    47 

    48 The abstract separation algebra is based upon ``Abstract Separation

    49 Logic'' by Calcagno et al. These theories are also the basis of

    50 ``Mechanised Separation Algebra'' by the authors \cite{KleinKB-ITP12}.

    51 

    52 The aim of this work is to support and significantly reduce the effort

    53 for future separation logic developments in Isabelle/HOL by factoring

    54 out the part of separation logic that can be treated abstractly once

    55 and for all. This includes developing typical default rule sets for

    56 reasoning as well as automated tactic support for separation logic.

    57 \end{abstract}

    58 

    59 \tableofcontents

    60 

    61 % include generated text of all theories

    62 \input{session}

    63 

    64 \bibliographystyle{abbrv}

    65 \bibliography{root}

    66 

    67 \end{document}