\documentclass{llncs}
\usepackage{times}
\usepackage{isabelle}
\usepackage{isabellesym}
\usepackage{amsmath}
\usepackage{amssymb}


\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{Proof Pearl: A New Foundation for Nominal Isabelle}
\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 permutation 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 differs from our earlier approach
in two important respects: First, instead of representing permutations as
lists of pairs of atoms, we now use a more abstract representation based on
functions.  Second, whereas the earlier work modeled different sorts of atoms
using different types, we now introduce a unified atom type that includes all
sorts of atoms. Interestingly, we allow swappings, that is permutations build from
two atoms, to be ill-sorted.  As a result of these design changes, we can iron
out inconveniences for the user, considerably simplify proofs and also
drastically reduce the amount of custom ML-code. Furthermore we can extend the
capabilities of Nominal Isabelle to deal with variables that carry additional
information. We end up with a pleasing and formalised theory of permutations
and support, on which we can build an improved and more powerful version of
Nominal Isabelle.
\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: