\documentclass{svjour3}

\usepackage{times}

\usepackage{isabelle}

\usepackage{isabellesym}

\usepackage{amsmath}

\usepackage{amssymb}

\usepackage{longtable}

\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{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}

\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}

Pitts et al 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.  We present a formalisation of this work 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.  Furthermore we extend the nominal

logic work with names that carry additional information and with a

formalisation of abstractions that bind finite 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: