\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 theoremprover. It provides a proving infrastructure for convenient reasoning aboutprogramming language calculi involving bound variables that have names (asopposed to de-Bruijn indices). In this paper we present an extension ofNominal Isabelle in order to deal with general binding structures. Suchbinding structures are ubiquitous in programming language research and onlyvery poorly supported with single binders, such as the lambdas in thelambda-calculus. For our extension we introduce novel definitions ofalpha-equivalence and establish automatically the reasoning infrastructure foralpha-equated terms. This includes strong induction principles that have thevariable convention already built in.\end{abstract}\input{session}\bibliographystyle{plain}\bibliography{root}\end{document}%%% Local Variables:%%% mode: latex%%% TeX-master: t%%% End: