\documentclass{acmconf}
\usepackage{isabelle}
\usepackage{isabellesym}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{tikz}
\usepackage{pgf}
\usepackage{pdfsetup}

\urlstyle{rm}
\isabellestyle{it}

\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
\renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\cdot}$}}}
\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
\renewcommand{\isasymequiv}{$\dn$}
\renewcommand{\isasymiota}{}
\renewcommand{\isasymemptyset}{$\varnothing$}
\newcommand{\LET}{\;\mathtt{let}\;}
\newcommand{\IN}{\;\mathtt{in}\;}
\newcommand{\END}{\;\mathtt{end}\;}
\newcommand{\AND}{\;\mathtt{and}\;}



%----------------- theorem definitions ----------
\newtheorem{property}{Property}[section]
\newtheorem{Theorem}{Theorem}[section]
\newtheorem{Definition}[Theorem]{Definition}
\newtheorem{Example}{\it Example}[section]

%-------------------- environment definitions -----------------
\newenvironment{example}[0]{\begin{Example} \it}{\end{Example}}
\newenvironment{proof-of}[1]{{\em Proof of #1:}}{}


\begin{document}

\title{\LARGE\bf General Binding Structures in Nominal Isabelle,\\ or How to
  Formalise Core-Haskell}
\maketitle

\maketitle
\begin{abstract} 
Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem
prover. It provides a proving infrastructure for convenient reasoning about
programming language calculi. In this paper we present an extension of Nominal
Isabelle for dealing with general binding structures. Such binding structures
are ubiquitous in programming language research and only very poorly supported
by theorem provers providing only single binding as in the lambda-calculus. We
give in this paper novel definitions for alpha-equivalence and establish
automatically the reasoning structure for alpha-equated terms. For example we
provide a strong induction principle that has the variable convention already
built in.
\end{abstract}


\input{session}

\bibliographystyle{plain}
\bibliography{root}

\end{document}

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