\documentclass[11pt,a4paper]{article}
\usepackage[a4paper,margin=1cm,footskip=.5cm]{geometry}
\usepackage[T1]{fontenc}
\usepackage{isabelle,isabellesym}

\usepackage{amssymb}
\usepackage{wasysym}

\usepackage[english]{babel}

% lifted composition.
\newcommand{\isasymbigcirc}{\isamath{\circ}}

% Bibliography
\usepackage[authoryear,longnamesfirst,sort]{natbib}
\bibpunct();A{},

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

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}
\renewcommand{\ttdefault}{cmtt} % CM rather than courier for \tt

% for uniform font size
\renewcommand{\isastyle}{\isastyleminor}

% Abstract various things that might change.
\newcommand{\ccode}[1]{\texttt{#1}}
\newcommand{\isabelletype}[1]{\emph{#1}}
\newcommand{\isabelleterm}[1]{\emph{#1}}

\begin{document}

\title{CIMP}
\author{Peter Gammie}
\maketitle

\begin{abstract}
  CIMP extends the small imperative language IMP with control
  non-determinism and constructs for synchronous message passing.
\end{abstract}

\tableofcontents

% sane default for proof documents
\parindent 0pt\parskip 0.5ex

% generated text of all theories
\input{session}

\section{Concluding remarks}

Previously
\citet{DBLP:conf/fase/NipkowN99,Prensa-PhD,Prensa-ESOP03}\footnote{The
  theories are in \texttt{\$ISABELLE/src/HOL/Hoare\_Parallel}.} have
developed the classical Owicki/Gries and Rely-Guarantee paradigms for
the verification of shared-variable concurrent programs in
Isabelle/HOL. These have been used to show the correctness of a
garbage collector \citep{PrenEsp00}.

We instead use synchronous message passing, which is significantly
less explored.
\citet{DBLP:conf/mfcs/BoerRH99,DBLP:books/cu/RoeverBH2001} provide
compositional systems for \emph{terminating} systems. We have instead
adopted Lamport's paradigm of a single global invariant and local
proof obligations as the systems we have in mind are tightly coupled
and it is not obvious that the proofs would be easier on a decomposed
system; see \citet[\S1.6.6]{DBLP:books/cu/RoeverBH2001} for a
concurring opinion.

Unlike the generic sequential program verification framework Simpl
\citep{DBLP:conf/lpar/Schirmer04}, we do not support function calls,
or a sophisticated account of state spaces. Moreover we do no
meta-theory beyond showing the simple VCG is sound
(\S\ref{sec:cimp-vcg}).

\bibliographystyle{plainnat}
\bibliography{root}
\addcontentsline{toc}{section}{References}

\end{document}

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