\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 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. For this we have to formulate the+
−
theory so that it is compatible with Higher-Order Logic, which the original formulation by+
−
Pitts is not.  We achieve this by not requiring that every construction has +
−
to have finite support. We present a formalisation that is based on a+
−
unified atom type 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.  We also describe a reasoning infrastructure+
−
that automates properties about equivariance, and present a formalisation of+
−
two 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:+
−