\documentclass{svjour3}
\usepackage{times}
\usepackage{isabelle}
\usepackage{isabellesym}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{mathabx}
\usepackage{proof}
\usepackage{longtable}
\usepackage{graphics}
\usepackage{pdfsetup}

\urlstyle{rm}
\isabellestyle{it}
\renewcommand{\isastyle}{\isastyleminor}
\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
\renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\cdot}$}}}
\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
\renewcommand{\isasymequiv}{$\dn$}
\renewcommand{\isasymiota}{}
\renewcommand{\isasymrightleftharpoons}{}
\renewcommand{\isasymemptyset}{$\varnothing$}
\newcommand{\isasymallatoms}{\ensuremath{\mathbb{A}}}
\newcommand{\rrh}{\mbox{\footnotesize$\rightrightharpoons$}}

\newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}
\newcommand\new[0]{\reflectbox{\ensuremath{\mathsf{N}}}}

\changenotsign

\begin{document}

\title{Implementing the Nominal Logic Work in Isabelle/HOL}
\author{Christian Urban \and Brian Huffman}
\institute{C.~Urban \at Technical University of Munich 
     \and  B.~Huffman \at Portland State University}
\date{Received: date / Accepted: date}

\maketitle

\begin{abstract}
In his nominal logic work, Pitts introduced a beautiful theory about names and
binding based on the notions of atoms, permutations and support. The
engineering challenge is to smoothly adapt this theory to a theorem prover
environment, in our case Isabelle/HOL. For this we have to formulate the
theory so that it is compatible with Higher-Order Logic, which the original formulation by
Pitts is not.  We achieve this by not requiring that every construction has 
to have finite support. We present a formalisation that is based on a
unified atom type and that represents permutations by bijective functions from
atoms to atoms. Interestingly, we allow swappings, which are permutations
build from two atoms, to be ill-sorted.  We also describe a reasoning infrastructure
that automates properties about equivariance, and present a formalisation of
two abstraction operators that bind sets of names.
\end{abstract}

% generated text of all theories
\input{session}

% optional bibliography
\bibliographystyle{abbrv}
\bibliography{root}

\end{document}

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