1 \documentclass{svjour3}

     2 \usepackage{times}

     3 \usepackage{isabelle}

     4 \usepackage{isabellesym}

     5 \usepackage{amsmath}

     6 \usepackage{amssymb}

     7 \usepackage{mathabx}

     8 \usepackage{proof}

     9 \usepackage{longtable}

    10 \usepackage{graphics}

    11 \usepackage{pdfsetup}

    12 

    13 \urlstyle{rm}

    14 \isabellestyle{it}

    15 \renewcommand{\isastyle}{\isastyleminor}

    16 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}

    17 \renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\cdot}$}}}

    18 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}

    19 \renewcommand{\isasymequiv}{$\dn$}

    20 \renewcommand{\isasymiota}{}

    21 \renewcommand{\isasymrightleftharpoons}{}

    22 \renewcommand{\isasymemptyset}{$\varnothing$}

    23 \newcommand{\isasymallatoms}{\ensuremath{\mathbb{A}}}

    24 \newcommand{\rrh}{\mbox{\footnotesize$\rightrightharpoons$}}

    25 

    26 \newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}

    27 \newcommand\new[0]{\reflectbox{\ensuremath{\mathsf{N}}}}

    28 

    29 \changenotsign

    30 

    31 \begin{document}

    32 

    33 \title{Implementing the Nominal Logic Work in Isabelle/HOL}

    34 \author{Christian Urban \and Brian Huffman}

    35 \institute{C.~Urban \at Technical University of Munich 

    36      \and  B.~Huffman \at Portland State University}

    37 \date{Received: date / Accepted: date}

    38 

    39 \maketitle

    40 

    41 \begin{abstract}

    42 In his nominal logic work, Pitts introduced a beautiful theory about names and

    43 binding based on the notions of atoms, permutations and support. The

    44 engineering challenge is to smoothly adapt this theory to a theorem prover

    45 environment, in our case Isabelle/HOL. For this we have to formulate the

    46 theory so that it is compatible with Higher-Order Logic, which the original formulation by

    47 Pitts is not.  We achieve this by not requiring that every construction has 

    48 to have finite support. We present a formalisation that is based on a

    49 unified atom type and that represents permutations by bijective functions from

    50 atoms to atoms. Interestingly, we allow swappings, which are permutations

    51 build from two atoms, to be ill-sorted.  We also describe a reasoning infrastructure

    52 that automates properties about equivariance, and present a formalisation of

    53 two abstraction operators that bind sets of names.

    54 \end{abstract}

    55 

    56 % generated text of all theories

    57 \input{session}

    58 

    59 % optional bibliography

    60 \bibliographystyle{abbrv}

    61 \bibliography{root}

    62 

    63 \end{document}

    64 

    65 %%% Local Variables:

    66 %%% mode: latex

    67 %%% TeX-master: t

    68 %%% End: