\documentclass{svjour3}\usepackage{times}\usepackage{isabelle}\usepackage{isabellesym}\usepackage{amsmath}\usepackage{amssymb}\usepackage{mathabx}\usepackage{proof}\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{\rrh}{\mbox{\footnotesize$\rightrightharpoons$}}\newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}\newcommand\new[0]{\reflectbox{\ensuremath{\mathsf{N}}}}\changenotsign\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 andbinding based on the notions of atoms, permutations and support. Theengineering challenge is to smoothly adapt this theory to a theorem proverenvironment, in our case Isabelle/HOL. For this we have to formulate thetheory so that it is compatible with Higher-Order Logic, which the original formulation byPitts is not. We achieve this by not requiring that every construction has to have finite support. We present a formalisation that is based on aunified atom type and that represents permutations by bijective functions fromatoms to atoms. Interestingly, we allow swappings, which are permutationsbuild from two atoms, to be ill-sorted. We also describe a reasoning infrastructurethat automates properties about equivariance, and present a formalisation oftwo 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: