1 \documentclass[runningheads]{llncs}

     2 \usepackage{times}

     3 \usepackage{isabelle}

     4 \usepackage{isabellesym}

     5 \usepackage{amsmath}

     6 \usepackage{amssymb}

     7 \usepackage{longtable}

     8 

     9 

    10 \usepackage{pdfsetup}

    11 \urlstyle{rm}

    12 \isabellestyle{it}

    13 \renewcommand{\isastyle}{\isastyleminor}

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

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

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

    17 \renewcommand{\isasymequiv}{$\dn$}

    18 \renewcommand{\isasymiota}{}

    19 \renewcommand{\isasymrightleftharpoons}{}

    20 \renewcommand{\isasymemptyset}{$\varnothing$}

    21 

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

    23 

    24 

    25 \begin{document}

    26 

    27 \title{Proof Pearl: A New Foundation for Nominal Isabelle}

    28 \author{Brian Huffman\inst{1} and Christian Urban\inst{2}}

    29 \institute{Portland State University \and Technical University of Munich}

    30 \maketitle

    31 

    32 \begin{abstract}

    33 Pitts et al introduced a beautiful theory about names and binding based on the

    34 notions of permutation and support. The engineering challenge is to smoothly

    35 adapt this theory to a theorem prover environment, in our case Isabelle/HOL.

    36 We present a formalisation of this work that differs from our earlier approach

    37 in two important respects: First, instead of representing permutations as

    38 lists of pairs of atoms, we now use a more abstract representation based on

    39 functions.  Second, whereas the earlier work modeled different sorts of atoms

    40 using different types, we now introduce a unified atom type that includes all

    41 sorts of atoms. Interestingly, we allow swappings, that is permutations build up by

    42 two atoms, to be ill-sorted.  As a result of these design changes, we can iron

    43 out inconveniences for the user, considerably simplify proofs and also

    44 drastically reduce the amount of custom ML-code. Furthermore we can extend the

    45 capabilities of Nominal Isabelle to deal with variables that carry additional

    46 information. We end up with a pleasing and formalised theory of permutations

    47 and support, on which we can build an improved and more powerful version of

    48 Nominal Isabelle.

    49 \end{abstract}

    50 

    51 % generated text of all theories

    52 \input{session}

    53 

    54 % optional bibliography

    55 \bibliographystyle{abbrv}

    56 \bibliography{root}

    57 

    58 \end{document}

    59 

    60 %%% Local Variables:

    61 %%% mode: latex

    62 %%% TeX-master: t

    63 %%% End: