\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 thenotions of permutation and support. The engineering challenge is to smoothlyadapt this theory to a theorem prover environment, in our case Isabelle/HOL.We present a formalisation of this work that differs from our earlier approachin two important respects: First, instead of representing permutations aslists of pairs of atoms, we now use a more abstract representation based onfunctions. Second, whereas the earlier work modeled different sorts of atomsusing different types, we now introduce a unified atom type that includes allsorts of atoms. Interestingly, we allow swappings, that is permutations build fromtwo atoms, to be ill-sorted. As a result of these design changes, we can ironout inconveniences for the user, considerably simplify proofs and alsodrastically reduce the amount of custom ML-code. Furthermore we can extend thecapabilities of Nominal Isabelle to deal with variables that carry additionalinformation. We end up with a pleasing and formalised theory of permutationsand support, on which we can build an improved and more powerful version ofNominal 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: