\documentclass{llncs}

\usepackage{times}

\usepackage{isabelle}

\usepackage{isabellesym}

\usepackage{amsmath}

\usepackage{amssymb}

%%\usepackage{amsthm}

\usepackage{tikz}

\usepackage{pgf}

\usepackage{pdfsetup}

\usepackage{ot1patch}

\usepackage{times}

\usepackage{boxedminipage}

\usepackage{proof}

\allowdisplaybreaks

\urlstyle{rm}

\isabellestyle{it}

\renewcommand{\isastyleminor}{\it}%

\renewcommand{\isastyle}{\normalsize\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{\isasymxi}{$..$}

\renewcommand{\isasymemptyset}{$\varnothing$}

\newcommand{\isasymnotapprox}{$\not\approx$}

\newcommand{\isasymLET}{$\mathtt{let}$}

\newcommand{\isasymAND}{$\mathtt{and}$}

\newcommand{\isasymIN}{$\mathtt{in}$}

\newcommand{\isasymEND}{$\mathtt{end}$}

\newcommand{\isasymBIND}{$\mathtt{bind}$}

\newcommand{\isasymANIL}{$\mathtt{anil}$}

\newcommand{\isasymACONS}{$\mathtt{acons}$}

\newcommand{\isasymCASE}{$\mathtt{case}$}

\newcommand{\isasymOF}{$\mathtt{of}$}

\newcommand{\isasymAL}{\makebox[0mm][l]{$^\alpha$}}

\newcommand{\isasymPRIME}{\makebox[0mm][l]{$'$}}

\newcommand{\LET}{\;\mathtt{let}\;}

\newcommand{\IN}{\;\mathtt{in}\;}

\newcommand{\END}{\;\mathtt{end}\;}

\newcommand{\AND}{\;\mathtt{and}\;}

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

\newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}

%----------------- theorem definitions ----------

%%\theoremstyle{plain}

%%\spnewtheorem{thm}[section]{Theorem}

%%\newtheorem{property}[thm]{Property}

%%\newtheorem{lemma}[thm]{Lemma}

%%\spnewtheorem{defn}[theorem]{Definition}

%%\spnewtheorem{exmple}[theorem]{Example}

%-------------------- environment definitions -----------------

\newenvironment{proof-of}[1]{{\em Proof of #1:}}{}

\begin{document}

\title{General Bindings and Alpha-Equivalence\\ in Nominal Isabelle}

\author{Christian Urban and Cezary Kaliszyk}

\institute{TU Munich, Germany}

%%%{\{urbanc, kaliszyk\}@in.tum.de}

\maketitle

\begin{abstract} 

Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem

programming language calculi involving named bound variables (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 general

bindings are ubiquitous in programming language research and only very

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

extension includes new definitions of $\alpha$-equivalence and establishes

automatically the reasoning infrastructure for $\alpha$-equated terms. We

also prove strong induction principles that have the usual variable

convention already built in.

\end{abstract}

%\category{F.4.1}{subcategory}{third-level}

%\terms

%formal reasoning, programming language calculi

%\keywords

%nominal logic work, variable convention

\input{session}

\bibliographystyle{plain}

\bibliography{root}

\end{document}

%%% Local Variables:

%%% mode: latex

%%% TeX-master: t

%%% End: