\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 involving bound variables that have names (as

opposed to de-Bruijn indices). 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

lambda-calculus. For our extension we introduce novel definitions of

alpha-equivalence and establish automatically the reasoning infrastructure for

alpha-equated terms. This includes strong induction principles that have the

variable convention already built in.

\end{abstract}

\input{session}

\bibliographystyle{plain}

\bibliography{root}

\end{document}

%%% Local Variables:

%%% mode: latex

%%% TeX-master: t

%%% End: