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