\documentclass{llncs}
\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{Brian Huffman\inst{1} and Christian Urban\inst{2}}
\institute{Portland State University \and Technical University of Munich}
\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 (that includes all sorts of atoms) 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 can extend the nominal logic with names that carry
additional information.
\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: