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