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