1 \documentclass[preprint]{sigplanconf}

     2 \usepackage{isabelle}

     3 \usepackage{isabellesym}

     4 \usepackage{amsmath}

     5 \usepackage{amssymb}

     6 \usepackage{pdfsetup}

     7 \usepackage{ot1patch}

     8 \usepackage{times}

     9 \usepackage{stmaryrd}

    10 

    11 \urlstyle{rm}

    12 \isabellestyle{it}

    13 \renewcommand{\isastyleminor}{\it}%

    14 \renewcommand{\isastyle}{\normalsize\it}%

    15 

    16 

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

    18 \renewcommand{\isasymequiv}{$\dn$}

    19 \renewcommand{\isasymemptyset}{$\varnothing$}

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

    21 

    22 \newcommand{\isasymcalL}{\ensuremath{\cal{L}}}

    23 \newcommand{\isasymbigplus}{\ensuremath{\bigplus}}

    24 

    25 \newcommand{\bigplus}{\mbox{\Large\bf$+$}}

    26 \begin{document}

    27 

    28 %\titlebanner{Nominal Functions}      % These are ignored unless

    29 %\preprintfooter{Nominal Functions}   % 'preprint' option specified.

    30 

    31 \title{Nominal Functions}

    32 \authorinfo{?}

    33            {?}

    34            {?}

    35 

    36 \maketitle

    37 

    38 \begin{abstract} 

    39 Nominal Isabelle provides an infrastructure for formal reasoning about terms

    40 involving named bound variables. This infrastructure allows bound variables to

    41 be analysed and manipulated directly. In this way it can mimic informal

    42 pen-and-pencil reasoning. However, this ability makes defining functions the

    43 most difficult aspect of the ``nominal approach''.  In this paper we present a

    44 new way of defining recursive functions over terms with bound variables.  For

    45 example, we are able to define without difficulties functions for CPS

    46 translations or the evaluation of lambda-terms, which were previously not

    47 definable in Nominal Isabelle. We also generalise the

    48 freshness-condition-for-binders to general binders recently introduced in

    49 Nominal Isabelle.

    50 \end{abstract}

    51 

    52 \category{CR-number}{subcategory}{third-level}

    53 

    54 \terms

    55 term1, term2

    56 

    57 \keywords

    58 keyword1, keyword2

    59 

    60 

    61 \input{session}

    62 

    63 %\bibliographystyle{plain}

    64 %\bibliography{root}

    65 

    66 \end{document}

    67 

    68 %%% Local Variables:

    69 %%% mode: latex

    70 %%% TeX-master: t

    71 %%% End: