\documentclass{svjour3}

\usepackage{times}

\usepackage{isabelle}

\usepackage{isabellesym}

\usepackage{amsmath}

\usepackage{amssymb}

\usepackage{mathabx}

\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

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: