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