\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: