\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}\;}

\newcommand{\fv}{\mathit{fv}}

%----------------- 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 Bindings 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 for dealing with general bindings, that means

term-constructors where multiple variables are bound at once. Such binding

structures are ubiquitous in programming language research and only very

poorly supported with single binders, such as lambda-abstractions. Our

extension includes novel definitions of alpha-equivalence and establishes

automatically the reasoning infrastructure for alpha-equated terms. We

also provide strong induction principles that have the usual variable

convention already built in.

\end{abstract}

\input{session}

\bibliographystyle{plain}

\bibliography{root}

\end{document}

%%% Local Variables:

%%% mode: latex

%%% TeX-master: t

%%% End: