1 \documentclass{llncs}

     2 \usepackage{times}

     3 \usepackage{isabelle}

     4 \usepackage{isabellesym}

     5 \usepackage{amsmath}

     6 \usepackage{amssymb}

     7 %%\usepackage{amsthm}

     8 \usepackage{tikz}

     9 \usepackage{pgf}

    10 \usepackage{pdfsetup}

    11 \usepackage{ot1patch}

    12 \usepackage{times}

    13 \usepackage{boxedminipage}

    14 \usepackage{proof}

    15 \usepackage{setspace}

    16 

    17 \allowdisplaybreaks

    18 \urlstyle{rm}

    19 \isabellestyle{it}

    20 \renewcommand{\isastyleminor}{\it}%

    21 \renewcommand{\isastyle}{\normalsize\it}%

    22 

    23 \DeclareRobustCommand{\flqq}{\mbox{\guillemotleft}}

    24 \DeclareRobustCommand{\frqq}{\mbox{\guillemotright}}

    25 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}

    26 \renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\hspace{-0.5mm}\cdot\hspace{-0.5mm}}$}}}

    27 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}

    28 \renewcommand{\isasymequiv}{$\dn$}

    29 %%\renewcommand{\isasymiota}{}

    30 \renewcommand{\isasymxi}{$..$}

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

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

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

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

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

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

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

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

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

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

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

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

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

    44 \newcommand{\isasymFRESH}{\#}

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

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

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

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

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

    50 

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

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

    53 %%\theoremstyle{plain}

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

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

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

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

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

    59 \spnewtheorem{myproperty}{Property}{\bfseries}{\rmfamily}

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

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

    62 

    63 %\addtolength{\textwidth}{2mm}

    64 \addtolength{\parskip}{-0.33mm}

    65 \begin{document}

    66 

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

    68 \author{Christian Urban and Cezary Kaliszyk}

    69 \institute{TU Munich, Germany}

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

    71 \maketitle

    72 

    73 \begin{abstract} 

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

    75 prover. It provides a proving infrastructure for reasoning about

    76 programming language calculi involving named bound variables (as

    77 opposed to de-Bruijn indices). In this paper we present an extension of

    78 Nominal Isabelle for dealing with general bindings, that means

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

    80 bindings are ubiquitous in programming language research and only very

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

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

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

    84 also prove strong induction principles that have the usual variable

    85 convention already built in.

    86 \end{abstract}

    87 

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

    89 

    90 %\terms

    91 %formal reasoning, programming language calculi

    92 

    93 %\keywords

    94 %nominal logic work, variable convention

    95 

    96 

    97 \input{session}

    98 

    99 \begin{spacing}{0.9}

   100   \bibliographystyle{plain}

   101   \bibliography{root}

   102 \end{spacing}

   103 

   104 %\pagebreak

   105 %\input{Appendix} 

   106 

   107 \end{document}

   108 

   109 %%% Local Variables:

   110 %%% mode: latex

   111 %%% TeX-master: t

   112 %%% End: