\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

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: