\documentclass[preprint]{sigplanconf}
\usepackage{isabelle}
\usepackage{isabellesym}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{pdfsetup}
\usepackage{ot1patch}
\usepackage{times}
\usepackage{stmaryrd}

\urlstyle{rm}
\isabellestyle{it}
\renewcommand{\isastyleminor}{\it}%
\renewcommand{\isastyle}{\normalsize\it}%


\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
\renewcommand{\isasymequiv}{$\dn$}
\renewcommand{\isasymemptyset}{$\varnothing$}
\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}

\newcommand{\isasymcalL}{\ensuremath{\cal{L}}}
\newcommand{\isasymbigplus}{\ensuremath{\bigplus}}

\newcommand{\bigplus}{\mbox{\Large\bf$+$}}
\begin{document}

%\titlebanner{Nominal Functions}      % These are ignored unless
%\preprintfooter{Nominal Functions}   % 'preprint' option specified.

\title{Nominal Functions}
\authorinfo{?}
           {?}
           {?}

\maketitle

\begin{abstract} 
Nominal Isabelle provides an infrastructure for formal reasoning about terms
involving named bound variables. This infrastructure allows bound variables to
be analysed and manipulated directly. In this way it can mimic informal
pen-and-pencil reasoning. However, this ability makes defining functions the
most difficult aspect of the ``nominal approach''.  In this paper we present a
new way of defining recursive functions over terms with bound variables.  For
example, we are able to define without difficulties functions for CPS
translations or the evaluation of lambda-terms, which were previously not
definable in Nominal Isabelle. We also generalise the
freshness-condition-for-binders to general binders recently introduced in
Nominal Isabelle.
\end{abstract}

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

\terms
term1, term2

\keywords
keyword1, keyword2


\input{session}

%\bibliographystyle{plain}
%\bibliography{root}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: