\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 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 for dealing with general bindings, that meansterm-constructors where multiple variables are bound at once. Such bindingstructures are ubiquitous in programming language research and only verypoorly supported with single binders, such as lambda-abstractions. Ourextension includes novel definitions of alpha-equivalence and establishesautomatically the reasoning infrastructure for alpha-equated terms. Wealso provide strong induction principles that have the usual variableconvention already built in.\end{abstract}\input{session}\bibliographystyle{plain}\bibliography{root}\end{document}%%% Local Variables:%%% mode: latex%%% TeX-master: t%%% End: