\documentclass{svjour3}
\usepackage{times}
\usepackage{isabelle}
\usepackage{isabellesym}
\usepackage{amsmath}
\usepackage{amssymb}
\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{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}
\newcommand\new[0]{\reflectbox{\ensuremath{\mathsf{N}}}}

\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 HOL, which the original formulation by
Pitts is not.  We achieve this by not requiring that every object in our
discourse has 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 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: