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

\urlstyle{rm}
\isabellestyle{it}

\DeclareRobustCommand{\flqq}{\mbox{\guillemotleft}}
\DeclareRobustCommand{\frqq}{\mbox{\guillemotright}}
\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 in order to deal with general binding structures. Such binding structures
are ubiquitous in programming language research and only very poorly supported
with single binders, as for example found in the lambda-calculus. For our
extension we introduce novel definitions of alpha-equivalence and establish
automatically the reasoning infrastructure for alpha-equated terms. This
includes a strong induction principle which 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: